1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
theory Imp
use state.State
use bool.Bool
use int.Int
(* ************************ SYNTAX ************************ *)
type aexpr =
| Anum int
| Avar id
| Aadd aexpr aexpr
| Asub aexpr aexpr
| Amul aexpr aexpr
type bexpr =
| Btrue
| Bfalse
| Band bexpr bexpr
| Bnot bexpr
| Beq aexpr aexpr
| Ble aexpr aexpr
type com =
| Cskip
| Cassign id aexpr
| Cseq com com
| Cif bexpr com com
| Cwhile bexpr com
(* ************************ SEMANTICS ************************ *)
function aeval (st:state) (e:aexpr) : int =
match e with
| Anum n -> n
| Avar x -> st[x]
| Aadd e1 e2 -> aeval st e1 + aeval st e2
| Asub e1 e2 -> aeval st e1 - aeval st e2
| Amul e1 e2 -> aeval st e1 * aeval st e2
end
function beval (st:state) (b:bexpr) : bool =
match b with
| Btrue -> true
| Bfalse -> false
| Bnot b' -> notb (beval st b')
| Band b1 b2 -> andb (beval st b1) (beval st b2)
| Beq a1 a2 -> aeval st a1 = aeval st a2
| Ble a1 a2 -> aeval st a1 <= aeval st a2
end
inductive ceval state com state =
(* skip *)
| E_Skip : forall m. ceval m Cskip m
(* assignement *)
| E_Ass : forall m a x. ceval m (Cassign x a) m[x <- aeval m a]
(* sequence *)
| E_Seq : forall cmd1 cmd2 m0 m1 m2.
ceval m0 cmd1 m1 -> ceval m1 cmd2 m2 -> ceval m0 (Cseq cmd1 cmd2) m2
(* if then else *)
| E_IfTrue : forall m0 m1 cond cmd1 cmd2. beval m0 cond ->
ceval m0 cmd1 m1 -> ceval m0 (Cif cond cmd1 cmd2) m1
| E_IfFalse : forall m0 m1 cond cmd1 cmd2. not beval m0 cond ->
ceval m0 cmd2 m1 -> ceval m0 (Cif cond cmd1 cmd2) m1
(* while *)
| E_WhileEnd : forall cond m body. not beval m cond ->
ceval m (Cwhile cond body) m
| E_WhileLoop : forall mi mj mf cond body. beval mi cond ->
ceval mi body mj -> ceval mj (Cwhile cond body) mf ->
ceval mi (Cwhile cond body) mf
(* Determinstic semantics *)
lemma ceval_deterministic_aux : forall c mi mf1. ceval mi c mf1 ->
forall mf2. ([@inversion] ceval mi c mf2) -> mf1 = mf2
lemma ceval_deterministic : forall c mi mf1 mf2.
ceval mi c mf1 -> ceval mi c mf2 -> mf1 = mf2
end
|
