author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47176  568fdc70e565 
child 56073  29e308b56d23 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Trans.thy 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13384
diff
changeset

2 
Author: David von Oheimb and Norbert Schirmer 
12854  3 

4 
Operational transition (smallstep) semantics of the 

5 
execution of Java expressions and statements 

6 

7 
PRELIMINARY!!!!!!!! 

8 
*) 

9 

16417  10 
theory Trans imports Evaln begin 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

11 

37956  12 
definition 
13 
groundVar :: "var \<Rightarrow> bool" where 

14 
"groundVar v \<longleftrightarrow> (case v of 

15 
LVar ln \<Rightarrow> True 

16 
 {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a 

17 
 e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i 

18 
 InsInitV c v \<Rightarrow> False)" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

19 

47176  20 
lemma groundVar_cases: 
21 
assumes ground: "groundVar v" 

22 
obtains (LVar) ln where "v=LVar ln" 

23 
 (FVar) accC statDeclC stat a fn where "v={accC,statDeclC,stat}(Lit a)..fn" 

24 
 (AVar) a i where "v=(Lit a).[Lit i]" 

25 
using ground LVar FVar AVar 

26 
apply (cases v) 

27 
apply (simp add: groundVar_def) 

28 
apply (simp add: groundVar_def,blast) 

29 
apply (simp add: groundVar_def,blast) 

30 
apply (simp add: groundVar_def) 

31 
done 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

32 

37956  33 
definition 
34 
groundExprs :: "expr list \<Rightarrow> bool" 

35 
where "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

36 

37956  37 
primrec the_val:: "expr \<Rightarrow> val" 
38 
where "the_val (Lit v) = v" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

39 

37597  40 
primrec the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)" where 
37956  41 
"the_var G s (LVar ln) = (lvar ln (store s),s)" 
37597  42 
 the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s" 
43 
 the_var_AVar_def: "the_var G s(a.[i]) =avar G (the_val i) (the_val a) s" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

44 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

45 
lemma the_var_FVar_simp[simp]: 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

46 
"the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

47 
by (simp) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

48 
declare the_var_FVar_def [simp del] 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

49 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

50 
lemma the_var_AVar_simp: 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

51 
"the_var G s ((Lit a).[Lit i]) = avar G i a s" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

52 
by (simp) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

53 
declare the_var_AVar_def [simp del] 
12854  54 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

55 
abbreviation 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

56 
Ref :: "loc \<Rightarrow> expr" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

57 
where "Ref a == Lit (Addr a)" 
12854  58 

35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

59 
abbreviation 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

60 
SKIP :: "expr" 
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
32960
diff
changeset

61 
where "SKIP == Lit Unit" 
12854  62 

23747  63 
inductive 
21765  64 
step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81) 
65 
for G :: prog 

66 
where 

12854  67 

68 
(* evaluation of expression *) 

69 
(* cf. 15.5 *) 

21765  70 
Abrupt: "\<lbrakk>\<forall>v. t \<noteq> \<langle>Lit v\<rangle>; 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

71 
\<forall> t. t \<noteq> \<langle>l\<bullet> Skip\<rangle>; 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

72 
\<forall> C vn c. t \<noteq> \<langle>Try Skip Catch(C vn) c\<rangle>; 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

73 
\<forall> x c. t \<noteq> \<langle>Skip Finally c\<rangle> \<and> xc \<noteq> Xcpt x; 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

74 
\<forall> a c. t \<noteq> \<langle>FinA a c\<rangle>\<rbrakk> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

75 
\<Longrightarrow> 
28524  76 
G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit undefined\<rangle>,Some xc,s)" 
12854  77 

21765  78 
 InsInitE: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>, s')\<rbrakk> 
79 
\<Longrightarrow> 

80 
G\<turnstile>(\<langle>InsInitE c e\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE c' e\<rangle>, s')" 

12854  81 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

82 
(* SeqE: "G\<turnstile>(\<langle>Seq Skip e\<rangle>,Norm s) \<mapsto>1 (\<langle>e\<rangle>, Norm s)" *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

83 
(* Specialised rules to evaluate: 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

84 
InsInitE Skip (NewC C), InisInitE Skip (NewA T[e]) *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

85 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

86 
(* cf. 15.8.1 *) 
21765  87 
 NewC: "G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init C) (NewC C)\<rangle>, Norm s)" 
88 
 NewCInited: "\<lbrakk>G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk> 

89 
\<Longrightarrow> 

90 
G\<turnstile>(\<langle>InsInitE Skip (NewC C)\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')" 

12854  91 

92 

93 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

94 
(* Alternative when rule SeqE is present 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

95 
NewCInited: "\<lbrakk>inited C (globs s); 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

96 
G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

97 
\<Longrightarrow> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

98 
G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

99 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

100 
NewC: 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

101 
"\<lbrakk>\<not> inited C (globs s)\<rbrakk> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

102 
\<Longrightarrow> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

103 
G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Seq (Init C) (NewC C)\<rangle>, Norm s)" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

104 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

105 
*) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

106 
(* cf. 15.9.1 *) 
21765  107 
 NewA: 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

108 
"G\<turnstile>(\<langle>New T[e]\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (init_comp_ty T) (New T[e])\<rangle>,Norm s)" 
21765  109 
 InsInitNewAIdx: 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

110 
"\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>, s')\<rbrakk> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

111 
\<Longrightarrow> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

112 
G\<turnstile>(\<langle>InsInitE Skip (New T[e])\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE Skip (New T[e'])\<rangle>,s')" 
21765  113 
 InsInitNewA: 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

114 
"\<lbrakk>G\<turnstile>abupd (check_neg i) (Norm s) \<midarrow>halloc (Arr T (the_Intg i))\<succ>a\<rightarrow> s' \<rbrakk> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

115 
\<Longrightarrow> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

116 
G\<turnstile>(\<langle>InsInitE Skip (New T[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>,s')" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

117 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

118 
(* cf. 15.15 *) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30952
diff
changeset

119 
 CastE: 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

120 
"\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

121 
\<Longrightarrow> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

122 
G\<turnstile>(\<langle>Cast T e\<rangle>,None,s) \<mapsto>1 (\<langle>Cast T e'\<rangle>,s')" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30952
diff
changeset

123 
 Cast: 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

124 
"\<lbrakk>s' = abupd (raise_if (\<not>G,s\<turnstile>v fits T) ClassCast) (Norm s)\<rbrakk> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

125 
\<Longrightarrow> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

126 
G\<turnstile>(\<langle>Cast T (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

127 
(* can be written without abupd, since we know Norm s *) 
12854  128 

129 

21765  130 
 InstE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

131 
\<Longrightarrow> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

132 
G\<turnstile>(\<langle>e InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')" 
21765  133 
 Inst: "\<lbrakk>b = (v\<noteq>Null \<and> G,s\<turnstile>v fits RefT T)\<rbrakk> 
134 
\<Longrightarrow> 

135 
G\<turnstile>(\<langle>(Lit v) InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (Bool b)\<rangle>,s')" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

136 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

137 
(* cf. 15.7.1 *) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30952
diff
changeset

138 
(*Lit "G\<turnstile>(Lit v,None,s) \<mapsto>1 (Lit v,None,s)"*) 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

139 

21765  140 
 UnOpE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s') \<rbrakk> 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

141 
\<Longrightarrow> 
21765  142 
G\<turnstile>(\<langle>UnOp unop e\<rangle>,Norm s) \<mapsto>1 (\<langle>UnOp unop e'\<rangle>,s')" 
143 
 UnOp: "G\<turnstile>(\<langle>UnOp unop (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (eval_unop unop v)\<rangle>,Norm s)" 

144 

145 
 BinOpE1: "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s') \<rbrakk> 

146 
\<Longrightarrow> 

147 
G\<turnstile>(\<langle>BinOp binop e1 e2\<rangle>,Norm s) \<mapsto>1 (\<langle>BinOp binop e1' e2\<rangle>,s')" 

148 
 BinOpE2: "\<lbrakk>need_second_arg binop v1; G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') \<rbrakk> 

13384  149 
\<Longrightarrow> 
150 
G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 

21765  151 
\<mapsto>1 (\<langle>BinOp binop (Lit v1) e2'\<rangle>,s')" 
152 
 BinOpTerm: "\<lbrakk>\<not> need_second_arg binop v1\<rbrakk> 

153 
\<Longrightarrow> 

154 
G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 

155 
\<mapsto>1 (\<langle>Lit v1\<rangle>,Norm s)" 

156 
 BinOp: "G\<turnstile>(\<langle>BinOp binop (Lit v1) (Lit v2)\<rangle>,Norm s) 

157 
\<mapsto>1 (\<langle>Lit (eval_binop binop v1 v2)\<rangle>,Norm s)" 

13384  158 
(* Maybe its more convenient to add: need_second_arg as precondition to BinOp 
159 
to make the choice between BinOpTerm and BinOp deterministic *) 

160 

21765  161 
 Super: "G\<turnstile>(\<langle>Super\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (val_this s)\<rangle>,Norm s)" 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

162 

21765  163 
 AccVA: "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s') \<rbrakk> 
164 
\<Longrightarrow> 

165 
G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Acc va'\<rangle>,s')" 

166 
 Acc: "\<lbrakk>groundVar va; ((v,vf),s') = the_var G (Norm s) va\<rbrakk> 

167 
\<Longrightarrow> 

168 
G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

169 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

170 
(* 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

171 
AccLVar: "G\<turnstile>(\<langle>Acc (LVar vn)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (fst (lvar vn s))\<rangle>,Norm s)" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

172 
AccFVar: "\<lbrakk>((v,vf),s') = fvar statDeclC stat fn a (Norm s)\<rbrakk> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

173 
\<Longrightarrow> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

174 
G\<turnstile>(\<langle>Acc ({accC,statDeclC,stat}(Lit a)..fn)\<rangle>,Norm s) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

175 
\<mapsto>1 (\<langle>Lit v\<rangle>,s')" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

176 
AccAVar: "\<lbrakk>((v,vf),s') = avar G i a (Norm s)\<rbrakk> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

177 
\<Longrightarrow> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

178 
G\<turnstile>(\<langle>Acc ((Lit a).[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

179 
*) 
21765  180 
 AssVA: "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s')\<rbrakk> 
181 
\<Longrightarrow> 

182 
G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va':=e\<rangle>,s')" 

183 
 AssE: "\<lbrakk>groundVar va; G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 

184 
\<Longrightarrow> 

185 
G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va:=e'\<rangle>,s')" 

186 
 Ass: "\<lbrakk>groundVar va; ((w,f),s') = the_var G (Norm s) va\<rbrakk> 

187 
\<Longrightarrow> 

188 
G\<turnstile>(\<langle>va:=(Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,assign f v s')" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

189 

21765  190 
 CondC: "\<lbrakk>G\<turnstile>(\<langle>e0\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'\<rangle>,s')\<rbrakk> 
191 
\<Longrightarrow> 

192 
G\<turnstile>(\<langle>e0? e1:e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'? e1:e2\<rangle>,s')" 

193 
 Cond: "G\<turnstile>(\<langle>Lit b? e1:e2\<rangle>,Norm s) \<mapsto>1 (\<langle>if the_Bool b then e1 else e2\<rangle>,Norm s)" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

194 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

195 

21765  196 
 CallTarget: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
197 
\<Longrightarrow> 

198 
G\<turnstile>(\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>,Norm s) 

199 
\<mapsto>1 (\<langle>{accC,statT,mode}e'\<cdot>mn({pTs}args)\<rangle>,s')" 

200 
 CallArgs: "\<lbrakk>G\<turnstile>(\<langle>args\<rangle>,Norm s) \<mapsto>1 (\<langle>args'\<rangle>,s')\<rbrakk> 

201 
\<Longrightarrow> 

202 
G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s) 

203 
\<mapsto>1 (\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args')\<rangle>,s')" 

204 
 Call: "\<lbrakk>groundExprs args; vs = map the_val args; 

205 
D = invocation_declclass G mode s a statT \<lparr>name=mn,parTs=pTs\<rparr>; 

206 
s'=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs (Norm s)\<rbrakk> 

207 
\<Longrightarrow> 

208 
G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s) 

209 
\<mapsto>1 (\<langle>Callee (locals s) (Methd D \<lparr>name=mn,parTs=pTs\<rparr>)\<rangle>,s')" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

210 

21765  211 
 Callee: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 
212 
\<Longrightarrow> 

213 
G\<turnstile>(\<langle>Callee lcls_caller e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

214 

21765  215 
 CalleeRet: "G\<turnstile>(\<langle>Callee lcls_caller (Lit v)\<rangle>,Norm s) 
216 
\<mapsto>1 (\<langle>Lit v\<rangle>,(set_lvars lcls_caller (Norm s)))" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

217 

21765  218 
 Methd: "G\<turnstile>(\<langle>Methd D sig\<rangle>,Norm s) \<mapsto>1 (\<langle>body G D sig\<rangle>,Norm s)" 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

219 

21765  220 
 Body: "G\<turnstile>(\<langle>Body D c\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init D) (Body D c)\<rangle>,Norm s)" 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

221 

21765  222 
 InsInitBody: 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

223 
"\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

224 
\<Longrightarrow> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

225 
G\<turnstile>(\<langle>InsInitE Skip (Body D c)\<rangle>,Norm s) \<mapsto>1(\<langle>InsInitE Skip (Body D c')\<rangle>,s')" 
21765  226 
 InsInitBodyRet: 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

227 
"G\<turnstile>(\<langle>InsInitE Skip (Body D Skip)\<rangle>,Norm s) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

228 
\<mapsto>1 (\<langle>Lit (the ((locals s) Result))\<rangle>,abupd (absorb Ret) (Norm s))" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

229 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

230 
(* LVar: "G\<turnstile>(LVar vn,Norm s)" is already evaluated *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

231 

21765  232 
 FVar: "\<lbrakk>\<not> inited statDeclC (globs s)\<rbrakk> 
233 
\<Longrightarrow> 

234 
G\<turnstile>(\<langle>{accC,statDeclC,stat}e..fn\<rangle>,Norm s) 

235 
\<mapsto>1 (\<langle>InsInitV (Init statDeclC) ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s)" 

236 
 InsInitFVarE: 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

237 
"\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

238 
\<Longrightarrow> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

239 
G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

240 
\<mapsto>1 (\<langle>InsInitV Skip ({accC,statDeclC,stat}e'..fn)\<rangle>,s')" 
21765  241 
 InsInitFVar: 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

242 
"G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}Lit a..fn)\<rangle>,Norm s) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

243 
\<mapsto>1 (\<langle>{accC,statDeclC,stat}Lit a..fn\<rangle>,Norm s)" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

244 
 {* Notice, that we do not have literal values for @{text vars}. 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

245 
The rules for accessing variables (@{text Acc}) and assigning to variables 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

246 
(@{text Ass}), test this with the predicate @{text groundVar}. After 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

247 
initialisation is done and the @{text FVar} is evaluated, we can't just 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

248 
throw away the @{text InsInitFVar} term and return a literal value, as in the 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

249 
cases of @{text New} or @{text NewC}. Instead we just return the evaluated 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

250 
@{text FVar} and test for initialisation in the rule @{text FVar}. 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

251 
*} 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

252 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

253 

21765  254 
 AVarE1: "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s')\<rbrakk> 
255 
\<Longrightarrow> 

256 
G\<turnstile>(\<langle>e1.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'.[e2]\<rangle>,s')" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

257 

21765  258 
 AVarE2: "G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') 
259 
\<Longrightarrow> 

260 
G\<turnstile>(\<langle>Lit a.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit a.[e2']\<rangle>,s')" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

261 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

262 
(* AVar: \<langle>(Lit a).[Lit i]\<rangle> is fully evaluated *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

263 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

264 
(* evaluation of expression lists *) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

265 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

266 
 {* @{text Nil} is fully evaluated *} 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

267 

21765  268 
 ConsHd: "\<lbrakk>G\<turnstile>(\<langle>e::expr\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 
269 
\<Longrightarrow> 

270 
G\<turnstile>(\<langle>e#es\<rangle>,Norm s) \<mapsto>1 (\<langle>e'#es\<rangle>,s')" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

271 

21765  272 
 ConsTl: "\<lbrakk>G\<turnstile>(\<langle>es\<rangle>,Norm s) \<mapsto>1 (\<langle>es'\<rangle>,s')\<rbrakk> 
273 
\<Longrightarrow> 

274 
G\<turnstile>(\<langle>(Lit v)#es\<rangle>,Norm s) \<mapsto>1 (\<langle>(Lit v)#es'\<rangle>,s')" 

12854  275 

276 
(* execution of statements *) 

277 

278 
(* cf. 14.5 *) 

21765  279 
 Skip: "G\<turnstile>(\<langle>Skip\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)" 
12854  280 

21765  281 
 ExprE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
282 
\<Longrightarrow> 

283 
G\<turnstile>(\<langle>Expr e\<rangle>,Norm s) \<mapsto>1 (\<langle>Expr e'\<rangle>,s')" 

284 
 Expr: "G\<turnstile>(\<langle>Expr (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)" 

12854  285 

286 

21765  287 
 LabC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk> 
288 
\<Longrightarrow> 

289 
G\<turnstile>(\<langle>l\<bullet> c\<rangle>,Norm s) \<mapsto>1 (\<langle>l\<bullet> c'\<rangle>,s')" 

290 
 Lab: "G\<turnstile>(\<langle>l\<bullet> Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>, abupd (absorb l) s)" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

291 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

292 
(* cf. 14.2 *) 
21765  293 
 CompC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
294 
\<Longrightarrow> 

295 
G\<turnstile>(\<langle>c1;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1';; c2\<rangle>,s')" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

296 

21765  297 
 Comp: "G\<turnstile>(\<langle>Skip;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c2\<rangle>,Norm s)" 
12854  298 

299 
(* cf. 14.8.2 *) 

21765  300 
 IfE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle> ,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
301 
\<Longrightarrow> 

302 
G\<turnstile>(\<langle>If(e) s1 Else s2\<rangle>,Norm s) \<mapsto>1 (\<langle>If(e') s1 Else s2\<rangle>,s')" 

303 
 If: "G\<turnstile>(\<langle>If(Lit v) s1 Else s2\<rangle>,Norm s) 

304 
\<mapsto>1 (\<langle>if the_Bool v then s1 else s2\<rangle>,Norm s)" 

12854  305 

306 
(* cf. 14.10, 14.10.1 *) 

21765  307 
 Loop: "G\<turnstile>(\<langle>l\<bullet> While(e) c\<rangle>,Norm s) 
308 
\<mapsto>1 (\<langle>If(e) (Cont l\<bullet>c;; l\<bullet> While(e) c) Else Skip\<rangle>,Norm s)" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

309 

21765  310 
 Jmp: "G\<turnstile>(\<langle>Jmp j\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,(Some (Jump j), s))" 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

311 

21765  312 
 ThrowE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 
313 
\<Longrightarrow> 

314 
G\<turnstile>(\<langle>Throw e\<rangle>,Norm s) \<mapsto>1 (\<langle>Throw e'\<rangle>,s')" 

315 
 Throw: "G\<turnstile>(\<langle>Throw (Lit a)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (throw a) (Norm s))" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

316 

21765  317 
 TryC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
318 
\<Longrightarrow> 

319 
G\<turnstile>(\<langle>Try c1 Catch(C vn) c2\<rangle>, Norm s) \<mapsto>1 (\<langle>Try c1' Catch(C vn) c2\<rangle>,s')" 

320 
 Try: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'\<rbrakk> 

321 
\<Longrightarrow> 

322 
G\<turnstile>(\<langle>Try Skip Catch(C vn) c2\<rangle>, s) 

323 
\<mapsto>1 (if G,s'\<turnstile>catch C then (\<langle>c2\<rangle>,new_xcpt_var vn s') 

324 
else (\<langle>Skip\<rangle>,s'))" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

325 

21765  326 
 FinC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 
327 
\<Longrightarrow> 

328 
G\<turnstile>(\<langle>c1 Finally c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1' Finally c2\<rangle>,s')" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

329 

21765  330 
 Fin: "G\<turnstile>(\<langle>Skip Finally c2\<rangle>,(a,s)) \<mapsto>1 (\<langle>FinA a c2\<rangle>,Norm s)" 
13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

331 

21765  332 
 FinAC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk> 
333 
\<Longrightarrow> 

334 
G\<turnstile>(\<langle>FinA a c\<rangle>,s) \<mapsto>1 (\<langle>FinA a c'\<rangle>,s')" 

335 
 FinA: "G\<turnstile>(\<langle>FinA a Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (abrupt_if (a\<noteq>None) a) s)" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

336 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

337 

21765  338 
 Init1: "\<lbrakk>inited C (globs s)\<rbrakk> 
339 
\<Longrightarrow> 

340 
G\<turnstile>(\<langle>Init C\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)" 

341 
 Init: "\<lbrakk>the (class G C)=c; \<not> inited C (globs s)\<rbrakk> 

342 
\<Longrightarrow> 

343 
G\<turnstile>(\<langle>Init C\<rangle>,Norm s) 

344 
\<mapsto>1 (\<langle>(if C = Object then Skip else (Init (super c)));; 

345 
Expr (Callee (locals s) (InsInitE (init c) SKIP))\<rangle> 

346 
,Norm (init_class_obj G C s))" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

347 
 {* @{text InsInitE} is just used as trick to embed the statement 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

348 
@{text "init c"} into an expression*} 
21765  349 
 InsInitESKIP: 
350 
"G\<turnstile>(\<langle>InsInitE Skip SKIP\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)" 

351 

352 
abbreviation 

353 
stepn:: "[prog, term \<times> state,nat,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>_ _"[61,82,82] 81) 

30952
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
28524
diff
changeset

354 
where "G\<turnstile>p \<mapsto>n p' \<equiv> (p,p') \<in> {(x, y). step G x y}^^n" 
21765  355 

356 
abbreviation 

357 
steptr:: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>* _"[61,82,82] 81) 

358 
where "G\<turnstile>p \<mapsto>* p' \<equiv> (p,p') \<in> {(x, y). step G x y}\<^sup>*" 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

359 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

360 
(* Equivalenzen: 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

361 
Bigstep zu Smallstep komplett. 
40945  362 
Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots> 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset

363 
*) 
12854  364 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

365 
(* 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

366 
lemma imp_eval_trans: 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

367 
assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

368 
shows trans: "G\<turnstile>(t,s0) \<mapsto>* (\<langle>Lit v\<rangle>,s1)" 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

369 
*) 
40945  370 
(* Jetzt muss man bei trans natürlich wieder unterscheiden: Stmt, Expr, Var! 
371 
Sowas blödes: 

13337
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

372 
Am besten den Terminus ground auf Var,Stmt,Expr hochziehen und dann 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

373 
the_vals definieren\<dots> 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

374 
G\<turnstile>(t,s0) \<mapsto>* (t',s1) \<and> the_vals t' = v 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

375 
*) 
f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

376 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

377 

f75dfc606ac7
Added unary and binary operations like (+,,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset

378 
end 