From f7ec9023ff88651a6a8d02e8c0134876e3d95d0d Mon Sep 17 00:00:00 2001 From: Anthony Berg Date: Mon, 12 Feb 2024 22:54:54 +0000 Subject: [PATCH] feat(formal): start formal modelling --- .vscode/vdmignore | 2 ++ formal/checklist.vdmsl | 25 +++++++++++++++++++++++++ 2 files changed, 27 insertions(+) create mode 100644 .vscode/vdmignore create mode 100644 formal/checklist.vdmsl diff --git a/.vscode/vdmignore b/.vscode/vdmignore new file mode 100644 index 0000000..55bdc3d --- /dev/null +++ b/.vscode/vdmignore @@ -0,0 +1,2 @@ +doc/ +pub/ diff --git a/formal/checklist.vdmsl b/formal/checklist.vdmsl new file mode 100644 index 0000000..134d3e1 --- /dev/null +++ b/formal/checklist.vdmsl @@ -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 +