source: LTS/Imp.ma @ 3377

Last change on this file since 3377 was 3377, checked in by sacerdot, 6 years ago
  • emit l removed

+ io l1 l2

The semantics has been changed so that one step can now emit a sequence of
labels (to implement io l1 l2).

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