]> matita.cs.unibo.it Git - helm.git/blob - weblib/While/semantics.ma
lablgladecc => lablgladecc3
[helm.git] / weblib / While / semantics.ma
1 (* new script *)
2
3 include "While/syntax.ma". 
4 include "arithmetics/div_and_mod.ma". 
5
6 (* state *)
7
8 definition state ≝ Var → nat.
9
10 definition eqvar ≝ λv1,v2.
11   match v1 with
12   [Id n => match v2 with [Id m => eqb n m]].
13
14 definition update : state → Var → nat → state ≝ λs,v,a,v1. 
15   if eqvar v1 v then a else s v1.
16
17 (* Semantics of Arithmetic expressions *)
18 \ 5pre class="smallmargin" style="display: inline;"\ 6let rec evalA a s ≝
19   match a with 
20   [ Const n => n
21   | Aid v => s v
22   | Add a b => evalA a s+evalA b s
23   | Sub a b => evalA a s-evalA b s
24   | Mul a b => evalA a s*evalA b s
25   | Div a b => div (evalA a s) (evalA b s)
26   | Mod a b => mod (evalA a s) (evalA b s) 
27   ]
28  .
29
30 example exA1: evalA ((Const 2)+(Const 3)*(Aid (Id 2))) (λx.\ 5span style="text-decoration: underline;"\ 61\ 5/span\ 6) = \ 5span style="text-decoration: underline;"\ 65\ 5/span\ 6.
31 normalize // qed 
32
33 let rec evalB b s ≝
34   match b with
35   [ BFalse => false
36   | BTtrue => true
37   | BNot b => ¬(evalB b s)
38   | BAnd b1 b2 => evalB b1 s ∧ evalB b2 s 
39   | BOr b1 b2 => evalB b1 s ∨ evalB b2 s \ 5pre class="smallmargin" style="display: inline;"\ 6\ 5/pre\ 6  
40   | Eq a1 a2 => eqb (evalA a1 s) (evalA a2 s)
41   | LE a1 a2 => leb (evalA a1 s) (evalA a2 s) 
42   ]. 
43
44 inductive Cmd_sem: Cmd → state → state\ 5pre class="smallmargin" style="display: inline;"\ 6→ Prop\ 5/pre\ 6
45   | Skip_sem : \forall s. Cmd_sem Skip s s
46   | Assign_sem : \forall s,v,a. Cmd_sem (Assign v a) s (update s v (evalA a s)) 
47   | 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
48   | 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
49   | 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
50   | 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
51   | While_false : \forall b,c,s. evalB b s = false \to Cmd_sem (While b c) s s  
52 .\ 5/pre\ 6