Changeset 3377
 Timestamp:
 Jul 2, 2013, 11:37:46 AM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Imp.ma
r3376 r3377 1 include "arithmetics/nat.ma". 2 include "basics/types.ma". 3 include "basics/lists/list.ma". 4 5 (*************************) 6 7 axiom ltb: nat → nat → bool. 8 9 (*************************) 10 11 record label: Type[0] ≝ {label_name: nat}. 12 13 record ident: Type[0] ≝ {ident_name: nat}. 14 15 record fname: Type[0] ≝ {function_name: nat}. 16 17 definition label_of_fname: fname → label ≝ 18 λf. mk_label (function_name f). 19 20 coercion label_of_fname. 21 22 record 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 }. 1 include "Common.ma". 29 2 30 3 inductive expr : Type[0] := … … 44 17  Cifthenelse: bool_expr → label → cmd → label → cmd → cmd 45 18  Cwhile: bool_expr → label → cmd → label → cmd 46  C label: label → cmd→ cmd19  Cio: label → label → cmd 47 20  Ccall: ident → fname → expr → option label → cmd 48 21  Cret: expr → cmd. … … 70 43 definition fetchT ≝ fname → cmd. 71 44 72 inductive step (S: storeT) (fetch: fetchT) : state S → state S → optionlabel → Prop :=45 inductive step (S: storeT) (fetch: fetchT) : state S → state S → list label → Prop := 73 46  step_assign: ∀x,e,k,K,s. 74 47 step … 75 48 〈Cassign x e, k, K, s〉 76 49 〈Cskip, k, K, set … s (Some … x) (eval_expr … s e)〉 77 (None …)50 [] 78 51  step_skip: ∀c,k,K,s. 79 52 step … 80 53 〈Cskip, c::k, K, s〉 81 〈c, k, K, s〉82 (None …)54 〈c, k, K, s〉 55 [] 83 56  step_seq: ∀c,c',k,K,s. 84 57 step … 85 〈Cseq c c', k, K, s〉86 〈 c, c'::k, K, s〉87 (None …)58 〈Cseq c c', k, K, s〉 59 〈 c, c'::k, K, s〉 60 [] 88 61  step_if_true: 89 62 ∀b,l1,c1,l2,c2,k,K,s. eval_bool_expr ? s b = true → 90 63 step … 91 64 〈Cifthenelse b l1 c1 l2 c2, k, K, s〉 92 〈 c1, k, K, s〉93 (Some … l1)65 〈 c1, k, K, s〉 66 [l1] 94 67  step_if_false: 95 68 ∀b,l1,c1,l2,c2,k,K,s. eval_bool_expr ? s b = false → 96 69 step … 97 70 〈Cifthenelse b l1 c1 l2 c2, k, K, s〉 98 〈 c2, k, K, s〉99 (Some … l2)71 〈 c2, k, K, s〉 72 [l2] 100 73  step_while_true: ∀b,l1,c,l2,k,K,s. eval_bool_expr ? s b = true → 101 74 step … 102 〈Cwhile b l1 c l2, k, K,s〉103 〈 c, (Cwhile b l1 c l2)::k, K, s〉104 (Some … l1)75 〈Cwhile b l1 c l2, k, K,s〉 76 〈 c, (Cwhile b l1 c l2)::k, K, s〉 77 [l1] 105 78  step_while_false: ∀b,l1,c,l2,k,K,s. eval_bool_expr ? s b = false → 106 79 step … 107 80 〈Cwhile b l1 c l2, k, K, s〉 108 〈 Cskip, k, K, s〉109 (Some … l2)110  step_label: ∀ c,l,k,K,s.81 〈 Cskip, k, K, s〉 82 [l2] 83  step_label: ∀l1,l2,k,K,s. 111 84 step … 112 〈C label l c,k,K,s〉113 〈 c,k,K,s〉114 (Some … l)85 〈Cio l1 l2, k, K, s〉 86 〈 Cskip, k, K, s〉 87 [l1;l2] 115 88  step_call: ∀x,f,e,l,c,k,K,s. fetch f = c → 116 89 step … 117 〈Ccall x f e l, k, K,s〉118 〈 c, [], 〈get ? s (None …),x,l,k〉::K, set ? s (None …) (eval_expr ? s e)〉119 (Some … f)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] 120 93  step_return: ∀e,k1,v,x,l,k2,K,s. 121 94 step … 122 〈Cret e, k1, 〈v,x,l,k2〉::K, s〉123 〈 Cskip, k2,K, set ? (set ? s (Some … x) (eval_expr ? s e)) (None …) v〉124 l.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]]). 125 98 126 99 (*
Note: See TracChangeset
for help on using the changeset viewer.