From 19aaeedf27c5059b5836101854a9c16f648a8957 Mon Sep 17 00:00:00 2001 From: Anthony Berg Date: Wed, 22 May 2024 15:53:33 +0100 Subject: [PATCH] refactor(dissertation): cleanup VDM model --- formal/checklist.vdmsl | 132 +----------------- .../chapters/appendix/database.tex | 1 - pub/dissertation/dissertation.pdf | Bin 984962 -> 969298 bytes pub/dissertation/dissertation.tex | 4 +- 4 files changed, 10 insertions(+), 127 deletions(-) diff --git a/formal/checklist.vdmsl b/formal/checklist.vdmsl index 6982548..ecd1414 100644 --- a/formal/checklist.vdmsl +++ b/formal/checklist.vdmsl @@ -35,7 +35,6 @@ types --@doc The state a switch can be in SwitchState = | | ; - --@LF why have a type kist as a rename? ItemState = SwitchState; --@TODO | Button | ... --@doc A switch, with the possible states it can be in, and the state that it is in @@ -93,10 +92,8 @@ types --@doc Item of a checklist, e.g. Landing gear down ChecklistItem :: - --@LF again, empty string here doesn't make sense. procedure : Dataref type : ItemType - --TODO Check is not only SwitchState check : SwitchState checked : bool; @@ -107,15 +104,12 @@ types inv i == i.item.type = i.checklistItem.type; --@doc A section of a checklist, e.g. Landing Checklist - --@LF shouldn't this be non-empty? What's the point to map a checklist name to an empty procedure? Yes. Procedure = seq1 of ChecklistItem inv p == - --@LF the "trick" for "false not in set S" is neat. It forces a full evaluation, rather than short circuited (i.e. stops at first false). - -- I presume this was intended. false not in set { let first = p(x-1).checked, second = p(x).checked in --@LF boolean values don't need equality check - second => first--((first = true) and (second = false)) + second => first | x in set {2,...,len p}}; functions @@ -123,36 +117,16 @@ functions --@doc Finds the index of the next item in the procedure that needs to be completed procedure_next_item_index: Procedure -> nat1 procedure_next_item_index(p) == - hd [ x | x in set {1,...,len p} & not p(x).checked ]--p(x).checked = false] + hd [ x | x in set {1,...,len p} & p(x).checked = false ] pre -- Checks procedure has not already been completed - not procedure_completed(p)--procedure_completed(p) = false + procedure_completed(p) = false post -- Checks that the index of the item is the next one to be completed - --@LF your def is quite confusing (to me) - --@LF how do you know that RESULT in inds p? Well, the definition above okay. - -- but you can't know whether p(RESULT-1) will! What if RESULT=1? p(RESULT-1)=p(0) which is invalid! (not p(RESULT).checked) and - (RESULT > 1 => p(RESULT-1).checked) - --p(RESULT).checked = false - --and if RESULT > 1 then - -- p(RESULT-1).checked = true - --else - -- true - ; + (RESULT > 1 => p(RESULT-1).checked); - -- --@doc Checks if all the procedures have been completed - -- check_all_proc_completed: Checklist -> bool - -- check_all_proc_completed(c) == - -- false not in set { procedure_completed(c(x)) | x in set {1,...,len c} }; - - -- --@doc Gives the index for the next procedure to complete - -- next_procedure: Checklist -> nat1 - -- next_procedure(c) == - -- hd [ x | x in set {1,...,len c} & not procedure_completed(c(x))] - -- post - -- RESULT <= len c; --@doc Checks if the procedure has been completed procedure_completed: Procedure -> bool @@ -162,19 +136,13 @@ functions --@doc Checks if the next item in the procedure has been completed check_proc_item_complete: Procedure * Aircraft -> bool check_proc_item_complete(p, a) == - --@LF here you have a nice lemma to prove: procedure_next_item_index(p) in set inds p! - -- I think that's always true let procItem = p(procedure_next_item_index(p)), - --@LF here you can't tell whether this will be true? i.e. procItem.procedure in set dom a.items? item = a.items(procItem.procedure) in - - --TODO need to be able to check for different types of Items procItem.check = item.object.position pre procedure_completed(p) = false - --@LF perhaps add - --and - --p(procedure_next_item_index(p)).procedure in set dom a.items? + and + p(procedure_next_item_index(p)).procedure in set dom a.items ; --@doc Marks next item in procedure as complete @@ -226,7 +194,6 @@ functions --@doc Moves any type of Item move_item: ItemObject * ItemState -> ItemObject move_item(i, s) == - -- if is_Switch(i) then (implement later) let switch: Switch = i.object in if check_switch_onoff(switch) and (s <> ) and switch.middlePosition then mk_ItemObject(i.type, move_switch(move_switch(switch, ), s)) @@ -235,7 +202,6 @@ functions pre wf_item_itemstate(i, s) and not check_item_in_position(i, s); - -- and wf_switch_move(i.object, s); --@doc Moves a specific switch in the aircraft move_switch: Switch * SwitchState -> Switch @@ -260,7 +226,6 @@ functions --@doc Checks if the item is already in position for the desired state for that item check_item_in_position: ItemObject * ItemState -> bool check_item_in_position(i, s) == - -- if is_Switch(i) then (implement later) i.object.position = s pre wf_item_itemstate(i,s); @@ -268,10 +233,7 @@ functions --@doc Checks if the Item.object is the same type for the ItemState wf_item_itemstate: ItemObject * ItemState -> bool wf_item_itemstate(i, s) == - (is_Switch(i.object) and is_SwitchState(s) and i.type = ) - --TODO check that the item has not already been completed before moving item - --TODO add other types of Items - ; + (is_Switch(i.object) and is_SwitchState(s) and i.type = ); --@doc Checks if the move of the Switch is a valid wf_switch_move: Switch * SwitchState -> bool @@ -290,83 +252,3 @@ functions end Checklist - -/* -//@LF always a good idea to run "qc" on your model. Here is its output. PO 21 and 22 show a problem. -//@LF silly me, this was my encoding with the cases missing one pattern :-). I can see yours has no issues. Good. - -> qc -PO #1, PROVABLE by finite types in 0.002s -PO #2, PROVABLE by finite types in 0.0s -PO #3, PROVABLE by finite types in 0.0s -PO #4, PROVABLE by finite types in 0.0s -PO #5, PROVABLE by finite types in 0.0s -PO #6, PROVABLE by finite types in 0.0s -PO #7, PROVABLE by finite types in 0.0s -PO #8, PROVABLE by finite types in 0.0s -PO #9, PROVABLE by finite types in 0.001s -PO #10, PROVABLE by finite types in 0.001s -PO #11, PROVABLE by direct (body is total) in 0.003s -PO #12, PROVABLE by witness s = mk_Switch(, true) in 0.001s -PO #13, PROVABLE by direct (body is total) in 0.001s -PO #14, PROVABLE by witness k = mk_Knob(1, [-2]) in 0.0s -PO #15, PROVABLE by direct (body is total) in 0.0s -PO #16, PROVABLE by witness t = 0 in 0.0s -PO #17, PROVABLE by direct (body is total) in 0.001s -PO #18, PROVABLE by witness t = mk_Throttle(0, 0) in 0.001s -PO #19, PROVABLE by direct (body is total) in 0.002s -PO #20, PROVABLE by witness i = mk_ItemObject(, mk_Knob(1, [-1])) in 0.002s -PO #21, FAILED in 0.002s: Counterexample: type =