3 include "While/syntax.ma".
4 include "arithmetics/div_and_mod.ma".
8 definition state ≝ Var → nat.
10 definition eqvar ≝ λv1,v2.
12 [Id n => match v2 with [Id m => eqb n m]].
14 definition update : state → Var → nat → state ≝ λs,v,a,v1.
15 if eqvar v1 v then a else s v1.
18 (* Semantics of Arithmetic expressions *)
19 \ 5pre class="smallmargin" style="display: inline;"
\ 6
24 | Add a b => evalA a s+evalA b s
25 | Sub a b => evalA a s-evalA b s
26 | Mul a b => evalA a s*evalA b s
27 | Div a b => div (evalA a s) (evalA b s)
28 | Mod a b => mod (evalA a s) (evalA b s)
32 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.
39 | BNot b => ¬(evalB b s)
40 | BAnd b1 b2 => evalB b1 s ∧ evalB b2 s
41 | BOr b1 b2 => evalB b1 s ∨ evalB b2 s
\ 5pre class="smallmargin" style="display: inline;"
\ 6\ 5/pre
\ 6
42 | Eq a1 a2 => eqb (evalA a1 s) (evalA a2 s)
43 | LE a1 a2 => leb (evalA a1 s) (evalA a2 s)
46 inductive Cmd_sem: Cmd → state → state
\ 5pre class="smallmargin" style="display: inline;"
\ 6→ Prop
\ 5/pre
\ 6≝
47 | Skip_sem : \forall s. Cmd_sem Skip s s
48 | Assign_sem : \forall s,v,a. Cmd_sem (Assign v a) s (update s v (evalA a s))
49 | 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
50 | 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
51 | 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
52 | 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
53 | While_false : \forall b,c,s. evalB b s = false \to Cmd_sem (While b c) s s