X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2FWhile%2Fsemantics.ma;fp=weblib%2FWhile%2Fsemantics.ma;h=ec11cf2ec002457254c6a2094ce13bbd0a1a5155;hb=e0671ce496760cec78ec904747af76ed55fd03a2;hp=9432984443838055615e9d56aa3fdc371a709d5c;hpb=2f389dbce69245089a3b7a7a63832ac5e5773363;p=helm.git

diff --git a/weblib/While/semantics.ma b/weblib/While/semantics.ma
index 943298444..ec11cf2ec 100644
--- a/weblib/While/semantics.ma
+++ b/weblib/While/semantics.ma
@@ -1,8 +1,53 @@
 (* new script *)
 
-include "While/syntax.ma".  
+include "While/syntax.ma". 
+include "arithmetics/div_and_mod.ma. 
 
 
 (* state *)
 
-definition state ≝ \
\ No newline at end of file
+definition state ≝ a href="cic:/matita/While/syntax/Var.ind(1,0,0)"Var/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+
+(* Semantics of Arithmetic expressions *)
+
+pre class="smallmargin" style="display: inline;"let rec eval_Aexp a s ≝
+  match a with 
+  | Const n => n
+  | Aid v => s v
+  | Add a b => a+b
+  | Sub a b => a-b
+  | Mul a b => a*b
+  | Div a b => div a b
+  | Mod a b => mod a b
+ .
+
+interpretation "Aexp plus" 'plus x y = (Add x y).
+interpretation "Aexp minus" 'plus x y = (Sub x y).
+interpretation "Aexp times" 'times x y = (Mul x y).
+
+(* Boolean expressions *)
+inductive Bexp : Type[0] ≝
+  | BFalse : Bexp
+  | BTtrue : Bexp
+  | BNot : Bexp → Bexp
+  | BAnd : Bexp → Bexp → Bexp
+  | BOr : Bexp → Bexp → Bexp
+  | Eq : a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → Bexp
+  | LE : a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → Bexp
+.
+
+interpretation "Bexp not" 'not x = (BNot x).
+interpretation "Bexp and" 'and x y = (BAnd x y).
+interpretation "Bexp or" 'or x y = (BOr x y).
+interpretation "Bexp 'less or equal to'" 'leq x y = (LE x y).
+
+(* Commands *)
+inductive Cmd : Type[0] ≝
+  | Skip : Cmd
+  | Assign : Var → a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → Cmd
+  | Seq : Cmd → Cmd → Cmd
+  | If : a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"Bexp/a → Cmd → Cmd → Cmd
+  | While : a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"Bexp/a → Cmd → Cmd
+.
+
+/pre 
\ No newline at end of file