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

diff --git a/weblib/While/semantics.ma b/weblib/While/semantics.ma
index 943298444..ee4362b71 100644
--- a/weblib/While/semantics.ma
+++ b/weblib/While/semantics.ma
@@ -1,8 +1,52 @@
 (* 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 ≝ Var → nat.
+
+definition eqvar ≝ λv1,v2.
+  match v1 with
+  [Id n => match v2 with [Id m => eqb n m]].
+
+definition update : state → Var → nat → state ≝ λs,v,a,v1. 
+  if eqvar v1 v then a else s v1.
+
+(* Semantics of Arithmetic expressions *)
+pre class="smallmargin" style="display: inline;"let rec evalA a s ≝
+  match a with 
+  [ Const n => n
+  | Aid v => s v
+  | Add a b => evalA a s+evalA b s
+  | Sub a b => evalA a s-evalA b s
+  | Mul a b => evalA a s*evalA b s
+  | Div a b => div (evalA a s) (evalA b s)
+  | Mod a b => mod (evalA a s) (evalA b s) 
+  ]
+ .
+
+example exA1: evalA ((Const 2)+(Const 3)*(Aid (Id 2))) (λx.span style="text-decoration: underline;"1/span) = span style="text-decoration: underline;"5/span.
+normalize // qed 
+
+let rec evalB b s ≝
+  match b with
+  [ BFalse => false
+  | BTtrue => true
+  | BNot b => ¬(evalB b s)
+  | BAnd b1 b2 => evalB b1 s ∧ evalB b2 s 
+  | BOr b1 b2 => evalB b1 s ∨ evalB b2 s pre class="smallmargin" style="display: inline;"/pre  
+  | Eq a1 a2 => eqb (evalA a1 s) (evalA a2 s)
+  | LE a1 a2 => leb (evalA a1 s) (evalA a2 s) 
+  ]. 
+
+inductive Cmd_sem: Cmd → state → statepre class="smallmargin" style="display: inline;"→ Prop/pre≝
+  | Skip_sem : \forall s. Cmd_sem Skip s s
+  | Assign_sem : \forall s,v,a. Cmd_sem (Assign v a) s (update s v (evalA a s)) 
+  | Seq_sem : \forall c1,c2,s1,s2,s3. Cmd_sem c1 s1 s2 \to  Cmd_sem c2 s2 s3 \to Cmd_sem (Seq c1 c2) s1 s3
+  | If_sem_true : \forall b,ct,cf,s,st. evalB b s = true \to  Cmd_sem ct s st \to  Cmd_sem (If b ct cf) s st
+  | If_sem_false : \forall b,ct,cf,s,sf. evalB b s = false \to  Cmd_sem cf s sf \to  Cmd_sem (If b ct cf) s sf
+  | While_true : \forall b,c,s,s1,s2. evalB b s = true \to Cmd_sem c s s1 \to Cmd_sem (While b c) s1 s2 \to Cmd_sem (While b c) s s2
+  | While_false : \forall b,c,s. evalB b s = false \to Cmd_sem (While b c) s s  
+./pre
\ No newline at end of file