fix(formal): stack underflow for index_of_item

2025-05-18 14:34:12 +02:00 · 2024-03-07 16:35:49 +00:00 · 2024-03-07 16:35:49 +00:00 · 546aac34d0
commit 546aac34d0
parent 60a788ce83
1 changed files with 2 additions and 0 deletions
--- a/formal/checklist.vdmsl
+++ b/formal/checklist.vdmsl
@ -122,6 +122,8 @@ functions
            index_of_item(i, tl a) + 1
        pre
            len a > 0
+            -- Checks if the last item in the aircraft is the item that is being searched for
+            and (len a = 1 and a(1).name = i)
        post
            -- Checks that the index is correct
            --TODO this does not check if it is the first item in the list