smyalygames/checklist-tester
1
0
Fork 0
mirror of https://github.com/smyalygames/checklist-tester.git synced 2025-05-18 14:34:12 +02:00
Code Issues Actions Packages Projects Releases Wiki Activity

feat(formal): add search for index of item in aircraft

Browse Source
This commit is contained in:
Anthony Berg 2024-03-07 15:52:03 +00:00
parent e904ecb8df
commit 5cc785b9e2
1 changed files with 18 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
formal/checklist.vdmsl
View File

@ -93,7 +93,7 @@ types
Checklist = seq of Procedure; Checklist = seq of Procedure;
functions functions
--@doc Finds the index of the next item in the checklist that needs to be completed --@doc Finds the index of the next item in the procedure that needs to be completed
procedure_next_index: Procedure -> nat1 procedure_next_index: Procedure -> nat1
procedure_next_index(p) == procedure_next_index(p) ==
hd [ x | x in set {1,...,len p} & p(x).checked = false] hd [ x | x in set {1,...,len p} & p(x).checked = false]
@ -114,4 +114,21 @@ functions
procedure_completed(p) == procedure_completed(p) ==
false not in set { p(x).checked | x in set {1,...,len p} }; false not in set { p(x).checked | x in set {1,...,len p} };
--@doc Find index of an item in Aircraft
index_of_item: String * Aircraft -> nat1
index_of_item(i, a) ==
if (hd a).name = i then 1
else
index_of_item(i, tl a) + 1
pre
len a > 0
post
-- Checks that the index is correct
--TODO this does not check if it is the first item in the list
if RESULT > 1 then
a(RESULT).name = i
else
true
measure len a;
end Checklist end Checklist