mirror of
https://github.com/smyalygames/checklist-tester.git
synced 2025-11-30 01:39:38 +01:00
feat(formal): start formal modelling
This commit is contained in:
25
formal/checklist.vdmsl
Normal file
25
formal/checklist.vdmsl
Normal file
@@ -0,0 +1,25 @@
|
||||
module Checklist
|
||||
exports all
|
||||
definitions
|
||||
|
||||
values
|
||||
|
||||
types
|
||||
|
||||
String = seq of char;
|
||||
|
||||
-- Item of a checklist, e.g. Landing gear down
|
||||
Item ::
|
||||
todo : String
|
||||
checked : bool;
|
||||
|
||||
-- A section of a checklist, e.g. Landing Checklist
|
||||
Section = seq of Item;
|
||||
|
||||
-- Full checklist, e.g. Startup, Descent, Landing Checklist
|
||||
Checklist = seq of Section;
|
||||
|
||||
functions
|
||||
|
||||
end Checklist
|
||||
|
||||
Reference in New Issue
Block a user