source: LTS/Imp.ma @ 3375

Last change on this file since 3375 was 3375, checked in by sacerdot, 6 years ago

Imp language and its labelled-SOS.

  • The language has function calls restricted to the following shape

x := f(E):l

where l is a post-label to be emitted _after_ f returns

  • All function declarations are of the form

nat f(nat None)

The anonimous variable None is the only one to be local.

  • All named variables are global
File size: 4.1 KB
Line 
1include "arithmetics/nat.ma".
2include "basics/types.ma".
3include "basics/lists/list.ma".
4
5(*************************)
6
7axiom ltb: nat → nat → bool.
8
9(*************************)
10
11record label: Type[0] ≝ {label_name: nat}.
12
13record ident: Type[0] ≝ {ident_name: nat}.
14
15record fname: Type[0] ≝ {function_name: nat}.
16
17definition label_of_fname: fname → label ≝
18 λf. mk_label (function_name f).
19 
20coercion label_of_fname.
21
22record storeT: Type[1] ≝
23 { store:> Type[0]
24 ; get: store → option ident → nat
25 ; set: store → option ident → nat → store
26 ; get_set_hit: ∀s,x,v. get (set s x v) x = v
27 ; get_set_miss: ∀s,x,y,v. get (set s x v) y = get s y
28 }.
29
30inductive expr : Type[0] :=
31| Evar: option ident → expr
32| Econst: nat → expr
33| Eadd: expr → expr → expr
34| Esub: expr → expr → expr.
35
36inductive bool_expr : Type[0] :=
37| Bequal: expr → expr → bool_expr
38| Bless: expr → expr → bool_expr.
39
40inductive cmd : Type[0] :=
41| Cskip: cmd
42| Cassign: ident → expr → cmd
43| Cseq: cmd → cmd → cmd
44| Cifthenelse: bool_expr → label → cmd → label → cmd → cmd
45| Cwhile: bool_expr → label → cmd → label → cmd
46| Clabel: label → cmd → cmd
47| Ccall: ident → fname → expr → option label → cmd
48| Cret: expr → cmd.
49
50let rec eval_expr (S: storeT) (s: S) (e: expr) on e : nat :=
51 match e with
52 [ Evar x ⇒ get S s x
53 | Econst n ⇒ n
54 | Eadd e1 e2 ⇒ eval_expr S s e1 + eval_expr S s e2
55 | Esub e1 e2 ⇒ eval_expr S s e1 - eval_expr S s e2
56 ].
57
58definition eval_bool_expr: ∀S:storeT. ∀s:S. ∀b:bool_expr. bool ≝
59 λS,s,b.
60  match b with
61  [ Bequal e1 e2 => eqb (eval_expr S s e1) (eval_expr S s e2)
62  | Bless e1 e2 => ltb (eval_expr S s e1) (eval_expr S s e2)
63  ].
64 
65definition continuation: Type[0] ≝ list cmd.
66
67definition state: storeT → Type[0] ≝ λS.
68 cmd × continuation × ((list (ident × (option label) × continuation)) × S).
69
70definition fetchT ≝ fname → cmd.
71
72inductive step (S: storeT) (fetch: fetchT) : state S → state S → option label → Prop :=
73| step_assign: ∀x,e,k,K,s.
74   step …
75    〈Cassign x e, k, K, s〉
76    〈Cskip, k, K, set … s (Some … x) (eval_expr … s e)〉
77    (None …)
78| step_skip: ∀c,k,K,s.
79   step …
80    〈Cskip, c::k, K, s〉
81    〈c, k, K, s〉
82    (None …)
83| step_seq: ∀c,c',k,K,s.
84   step …
85    〈Cseq c c', k, K, s〉
86    〈c, c'::k, K, s〉
87    (None …)
88| step_if_true:
89   ∀b,l1,c1,l2,c2,k,K,s. eval_bool_expr ? s b = true →
90    step …
91     〈Cifthenelse b l1 c1 l2 c2, k, K, s〉
92     〈c1, k, K, s〉
93     (Some … l1)
94| step_if_false:
95   ∀b,l1,c1,l2,c2,k,K,s. eval_bool_expr ? s b = false →
96    step …
97     〈Cifthenelse b l1 c1 l2 c2, k, K, s〉
98     〈c2, k, K, s〉
99     (Some … l2)
100| step_while_true: ∀b,l1,c,l2,k,K,s. eval_bool_expr ? s b = true →
101   step …
102    〈Cwhile b l1 c l2, k, K,s〉
103    〈c, (Cwhile b l1 c l2)::k, K, s〉
104    (Some … l1)
105| step_while_false: ∀b,l1,c,l2,k,K,s. eval_bool_expr ? s b = false →
106   step …
107    〈Cwhile b l1 c l2, k, K, s〉
108    〈Cskip, k, K, s〉
109    (Some … l2)
110| step_label: ∀c,l,k,K,s.
111   step …
112    〈Clabel l c,k,K,s〉
113    〈c,k,K,s〉
114    (Some … l)
115| step_call: ∀x,f,e,l,c,k,K,s. fetch f = c →
116   step …
117    〈Ccall x f e l, k, K, s〉
118    〈c, [], 〈x,l,k〉::K, set ? s (None …) (eval_expr ? s e)〉
119    (Some … f)
120| step_return: ∀e,k1,x,l,k2,K,s.
121   step …
122    〈Cret e, k1, 〈x,l,k2〉::K, s〉
123    〈Cskip, k2, K, set ? s (Some … x) (eval_expr ? s e)〉
124    l.
125
126(*
127definition steps: ∀S: storeT) : state S → state S → option label → Prop := star (trans_imp lbl).
128
129Definition term_imp_lbl (lbl: Type) (c: cmd lbl) (s s': store) (trace: list lbl): Prop :=
130        star_imp lbl (c, Chalt lbl, s) (Cskip lbl, Chalt lbl, s') trace.
131
132Lemma induction_on_code_imp:
133forall (P : code_imp -> Prop),
134  P (Cskip False) ->
135  (forall x e, P (Cassign False x e)) ->
136  (forall S1 S2, P S1 -> P S2 -> P (Cseq False S1 S2)) ->
137  (forall S1 S2 b, P S1 -> P S2 -> P (Cifthenelse False b S1 S2)) ->
138  (forall S b, P S -> P (Cwhile False b S)) ->
139  forall S : code_imp, P S.
140Proof.
141 unfold code_imp; intros.
142 induction S as [ | | | | | Hfalse ]; auto.
143 destruct Hfalse.
144Qed.
145*)
Note: See TracBrowser for help on using the repository browser.