1 files changed, 73 insertions, 0 deletions
diff --git a/While.dcl b/While.dcl
new file mode 100644
index 0000000..1ab5ce9
--- /dev/null
+++ b/While.dcl
@@ -0,0 +1,73 @@
+definition module While
+
+from StdOverloaded import class toString
+
+:: Semantics = NS                           // Natural Semantics
+             | SOS                          // Structural Operational Semantics
+
+// evaluate @arg2 in state @arg3 according to @arg1
+class eval a b :: Semantics a State -> b
+
+instance eval Stm State
+instance eval Int Int
+instance eval Var Int
+instance eval ArithExpr Int
+instance eval Bool Bool
+instance eval BoolExpr Bool
+
+instance toString ArithExpr
+instance toString BoolExpr
+instance toString Stm
+instance toString DerivTree
+instance toString DerivSeq
+
+// Syntax
+
+:: Stm = Skip                                   // Skip
+       | (:.) infixr 1 Stm Stm                  // Composition
+       | E.a: (:=) infix 2 Var a                // Assignment
+         & eval a Int & toString a
+       | E.a: If a Stm Stm                      // If
+         & eval a Bool & toString a
+       | E.a: While a Stm                       // While
+         & eval a Bool & toString a
+
+:: Var :== Char                                 // Variable
+
+:: ArithExpr = E.a b: (+) infixl 6 a b          // Addition
+               & eval a Int & toString a & eval b Int & toString b
+             | E.a b: (-) infixl 6 a b          // Subtraction
+               & eval a Int & eval b Int & toString a & toString b
+             | E.a b: (*) infixl 7 a b          // Multiplication
+               & eval a Int & toString a & eval b Int & toString b
+
+:: BoolExpr = E.a b: (==) infix 4 a b           // Equality on ArithExpr
+               & eval a Int & toString a & eval b Int & toString b
+            | E.a b: (<=) infix 4 a b           // Ord
+               & eval a Int & toString a & eval b Int & toString b
+            | E.a: ~ a                          // Negation
+               & eval a Bool & toString a
+            | E.a b: (/\) infixr 3 a b          // Conjunction
+               & eval a Bool & toString a & eval b Bool & toString b
+
+:: State :== Var -> Int
+
+// Natural Semantics
+
+:: DerivTree = { stm :: Stm
+               , state :: State
+               , children :: [DerivTree]
+               , result :: State
+               }
+
+tree :: Stm State -> DerivTree // The derivation tree for @arg1 in state @arg2
+
+// Structural Operational Semantics
+
+:: DerivSeqNode = Done State
+                | NDone Stm State
+
+:: DerivSeq :== [DerivSeqNode]
+
+seq :: Stm State -> DerivSeq // The derivation seq. for @arg1 in state @arg2
+