From e904ecb8dfc56e8339113ac4cec13c31b32a3ea9 Mon Sep 17 00:00:00 2001
From: Anthony <smyalygames@gmail.com>
Date: Tue, 27 Feb 2024 17:25:22 +0000
Subject: [PATCH] feat(formal): add checking functions for procedures

---
 formal/checklist.vdmsl | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/formal/checklist.vdmsl b/formal/checklist.vdmsl
index e399784..af0a175 100644
--- a/formal/checklist.vdmsl
+++ b/formal/checklist.vdmsl
@@ -93,6 +93,25 @@ types
     Checklist = seq of Procedure;
 
 functions
+    --@doc Finds the index of the next item in the checklist that needs to be completed
+    procedure_next_index: Procedure -> nat1
+    procedure_next_index(p) ==
+        hd [ x | x in set {1,...,len p} & p(x).checked = false]
+    pre
+        -- Checks to prevent getting the head of an empty sequence
+        len p > 0
+        and procedure_completed(p) = false
+    post
+        -- Checks that the index of the item is the next one to be completed
+        p(RESULT).checked = false
+        and if RESULT > 1 then 
+            p(RESULT-1).checked = true
+        else 
+            true;
 
+    --@doc Checks if the procedure has been completed
+    procedure_completed: Procedure -> bool
+    procedure_completed(p) ==
+        false not in set { p(x).checked | x in set {1,...,len p} };
 
 end Checklist