(* Title: HOL/Bali/Trans.thy
Author: David von Oheimb and Norbert Schirmer
Operational transition (small-step) semantics of the
execution of Java expressions and statements
PRELIMINARY!!!!!!!!
*)
theory Trans imports Evaln begin
definition
groundVar :: "var \ bool" where
"groundVar v \ (case v of
LVar ln \<Rightarrow> True
| {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
| e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
| InsInitV c v \<Rightarrow> False)"
lemma groundVar_cases:
assumes ground: "groundVar v"
obtains (LVar) ln where "v=LVar ln"
| (FVar) accC statDeclC stat a fn where "v={accC,statDeclC,stat}(Lit a)..fn"
| (AVar) a i where "v=(Lit a).[Lit i]"
using ground LVar FVar AVar
by (cases v) (auto simp add: groundVar_def)
definition
groundExprs :: "expr list \ bool"
where "groundExprs es \ (\e \ set es. \v. e = Lit v)"
primrec the_val:: "expr \ val"
where "the_val (Lit v) = v"
primrec the_var:: "prog \ state \ var \ (vvar \ state)" where
"the_var G s (LVar ln) = (lvar ln (store s),s)"
| the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
| the_var_AVar_def: "the_var G s(a.[i]) =avar G (the_val i) (the_val a) s"
lemma the_var_FVar_simp[simp]:
"the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s"
by (simp)
declare the_var_FVar_def [simp del]
lemma the_var_AVar_simp:
"the_var G s ((Lit a).[Lit i]) = avar G i a s"
by (simp)
declare the_var_AVar_def [simp del]
abbreviation
Ref :: "loc \ expr"
where "Ref a == Lit (Addr a)"
abbreviation
SKIP :: "expr"
where "SKIP == Lit Unit"
inductive
step :: "[prog,term \ state,term \ state] \ bool" ("_\_ \1 _"[61,82,82] 81)
for G :: prog
where
(* evaluation of expression *)
(* cf. 15.5 *)
Abrupt: "\\v. t \ \Lit v\;
\<forall> t. t \<noteq> \<langle>l\<bullet> Skip\<rangle>;
\<forall> C vn c. t \<noteq> \<langle>Try Skip Catch(C vn) c\<rangle>;
\<forall> x c. t \<noteq> \<langle>Skip Finally c\<rangle> \<and> xc \<noteq> Xcpt x;
\<forall> a c. t \<noteq> \<langle>FinA a c\<rangle>\<rbrakk>
\<Longrightarrow>
G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit undefined\<rangle>,Some xc,s)"
| InsInitE: "\G\(\c\,Norm s) \1 (\c'\, s')\
\<Longrightarrow>
G\<turnstile>(\<langle>InsInitE c e\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE c' e\<rangle>, s')"
(* SeqE: "G\<turnstile>(\<langle>Seq Skip e\<rangle>,Norm s) \<mapsto>1 (\<langle>e\<rangle>, Norm s)" *)
(* Specialised rules to evaluate:
InsInitE Skip (NewC C), InisInitE Skip (NewA T[e]) *)
(* cf. 15.8.1 *)
| NewC: "G\(\NewC C\,Norm s) \1 (\InsInitE (Init C) (NewC C)\, Norm s)"
| NewCInited: "\G\ Norm s \halloc (CInst C)\a\ s'\
\<Longrightarrow>
G\<turnstile>(\<langle>InsInitE Skip (NewC C)\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')"
(* Alternative when rule SeqE is present
NewCInited: "\<lbrakk>inited C (globs s);
G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')"
NewC:
"\<lbrakk>\<not> inited C (globs s)\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Seq (Init C) (NewC C)\<rangle>, Norm s)"
*)
(* cf. 15.9.1 *)
| NewA:
"G\(\New T[e]\,Norm s) \1 (\InsInitE (init_comp_ty T) (New T[e])\,Norm s)"
| InsInitNewAIdx:
"\G\(\e\,Norm s) \1 (\e'\, s')\
\<Longrightarrow>
G\<turnstile>(\<langle>InsInitE Skip (New T[e])\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE Skip (New T[e'])\<rangle>,s')"
| InsInitNewA:
"\G\abupd (check_neg i) (Norm s) \halloc (Arr T (the_Intg i))\a\ s' \
\<Longrightarrow>
G\<turnstile>(\<langle>InsInitE Skip (New T[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>,s')"
(* cf. 15.15 *)
| CastE:
"\G\(\e\,Norm s) \1 (\e'\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>Cast T e\<rangle>,None,s) \<mapsto>1 (\<langle>Cast T e'\<rangle>,s')"
| Cast:
"\s' = abupd (raise_if (\G,s\v fits T) ClassCast) (Norm s)\
\<Longrightarrow>
G\<turnstile>(\<langle>Cast T (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
(* can be written without abupd, since we know Norm s *)
| InstE: "\G\(\e\,Norm s) \1 (\e'::expr\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>e InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')"
| Inst: "\b = (v\Null \ G,s\v fits RefT T)\
\<Longrightarrow>
G\<turnstile>(\<langle>(Lit v) InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (Bool b)\<rangle>,s')"
(* cf. 15.7.1 *)
(*Lit "G\<turnstile>(Lit v,None,s) \<mapsto>1 (Lit v,None,s)"*)
| UnOpE: "\G\(\e\,Norm s) \1 (\e'\,s') \
\<Longrightarrow>
G\<turnstile>(\<langle>UnOp unop e\<rangle>,Norm s) \<mapsto>1 (\<langle>UnOp unop e'\<rangle>,s')"
| UnOp: "G\(\UnOp unop (Lit v)\,Norm s) \1 (\Lit (eval_unop unop v)\,Norm s)"
| BinOpE1: "\G\(\e1\,Norm s) \1 (\e1'\,s') \
\<Longrightarrow>
G\<turnstile>(\<langle>BinOp binop e1 e2\<rangle>,Norm s) \<mapsto>1 (\<langle>BinOp binop e1' e2\<rangle>,s')"
| BinOpE2: "\need_second_arg binop v1; G\(\e2\,Norm s) \1 (\e2'\,s') \
\<Longrightarrow>
G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s)
\<mapsto>1 (\<langle>BinOp binop (Lit v1) e2'\<rangle>,s')"
| BinOpTerm: "\\ need_second_arg binop v1\
\<Longrightarrow>
G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s)
\<mapsto>1 (\<langle>Lit v1\<rangle>,Norm s)"
| BinOp: "G\(\BinOp binop (Lit v1) (Lit v2)\,Norm s)
\<mapsto>1 (\<langle>Lit (eval_binop binop v1 v2)\<rangle>,Norm s)"
(* Maybe its more convenient to add: need_second_arg as precondition to BinOp
to make the choice between BinOpTerm and BinOp deterministic *)
| Super: "G\(\Super\,Norm s) \1 (\Lit (val_this s)\,Norm s)"
| AccVA: "\G\(\va\,Norm s) \1 (\va'\,s') \
\<Longrightarrow>
G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Acc va'\<rangle>,s')"
| Acc: "\groundVar va; ((v,vf),s') = the_var G (Norm s) va\
\<Longrightarrow>
G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
(*
AccLVar: "G\<turnstile>(\<langle>Acc (LVar vn)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (fst (lvar vn s))\<rangle>,Norm s)"
AccFVar: "\<lbrakk>((v,vf),s') = fvar statDeclC stat fn a (Norm s)\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>Acc ({accC,statDeclC,stat}(Lit a)..fn)\<rangle>,Norm s)
\<mapsto>1 (\<langle>Lit v\<rangle>,s')"
AccAVar: "\<lbrakk>((v,vf),s') = avar G i a (Norm s)\<rbrakk>
\<Longrightarrow>
G\<turnstile>(\<langle>Acc ((Lit a).[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')"
*)
| AssVA: "\G\(\va\,Norm s) \1 (\va'\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va':=e\<rangle>,s')"
| AssE: "\groundVar va; G\(\e\,Norm s) \1 (\e'\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va:=e'\<rangle>,s')"
| Ass: "\groundVar va; ((w,f),s') = the_var G (Norm s) va\
\<Longrightarrow>
G\<turnstile>(\<langle>va:=(Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,assign f v s')"
| CondC: "\G\(\e0\,Norm s) \1 (\e0'\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>e0? e1:e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'? e1:e2\<rangle>,s')"
| Cond: "G\(\Lit b? e1:e2\,Norm s) \1 (\if the_Bool b then e1 else e2\,Norm s)"
| CallTarget: "\G\(\e\,Norm s) \1 (\e'\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>,Norm s)
\<mapsto>1 (\<langle>{accC,statT,mode}e'\<cdot>mn({pTs}args)\<rangle>,s')"
| CallArgs: "\G\(\args\,Norm s) \1 (\args'\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s)
\<mapsto>1 (\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args')\<rangle>,s')"
| Call: "\groundExprs args; vs = map the_val args;
D = invocation_declclass G mode s a statT \<lparr>name=mn,parTs=pTs\<rparr>;
s'=init_lvars G D \name=mn,parTs=pTs\ mode a' vs (Norm s)\
\<Longrightarrow>
G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s)
\<mapsto>1 (\<langle>Callee (locals s) (Methd D \<lparr>name=mn,parTs=pTs\<rparr>)\<rangle>,s')"
| Callee: "\G\(\e\,Norm s) \1 (\e'::expr\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>Callee lcls_caller e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')"
| CalleeRet: "G\(\Callee lcls_caller (Lit v)\,Norm s)
\<mapsto>1 (\<langle>Lit v\<rangle>,(set_lvars lcls_caller (Norm s)))"
| Methd: "G\(\Methd D sig\,Norm s) \1 (\body G D sig\,Norm s)"
| Body: "G\(\Body D c\,Norm s) \1 (\InsInitE (Init D) (Body D c)\,Norm s)"
| InsInitBody:
"\G\(\c\,Norm s) \1 (\c'\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>InsInitE Skip (Body D c)\<rangle>,Norm s) \<mapsto>1(\<langle>InsInitE Skip (Body D c')\<rangle>,s')"
| InsInitBodyRet:
"G\(\InsInitE Skip (Body D Skip)\,Norm s)
\<mapsto>1 (\<langle>Lit (the ((locals s) Result))\<rangle>,abupd (absorb Ret) (Norm s))"
(* LVar: "G\<turnstile>(LVar vn,Norm s)" is already evaluated *)
| FVar: "\\ inited statDeclC (globs s)\
\<Longrightarrow>
G\<turnstile>(\<langle>{accC,statDeclC,stat}e..fn\<rangle>,Norm s)
\<mapsto>1 (\<langle>InsInitV (Init statDeclC) ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s)"
| InsInitFVarE:
"\G\(\e\,Norm s) \1 (\e'\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s)
\<mapsto>1 (\<langle>InsInitV Skip ({accC,statDeclC,stat}e'..fn)\<rangle>,s')"
| InsInitFVar:
"G\(\InsInitV Skip ({accC,statDeclC,stat}Lit a..fn)\,Norm s)
\<mapsto>1 (\<langle>{accC,statDeclC,stat}Lit a..fn\<rangle>,Norm s)"
\<comment> \<open>Notice, that we do not have literal values for \<open>vars\<close>.
The rules for accessing variables (\<open>Acc\<close>) and assigning to variables
(\<open>Ass\<close>), test this with the predicate \<open>groundVar\<close>. After
initialisation is done and the \<open>FVar\<close> is evaluated, we can't just
throw away the \<open>InsInitFVar\<close> term and return a literal value, as in the
cases of \<open>New\<close> or \<open>NewC\<close>. Instead we just return the evaluated
\<open>FVar\<close> and test for initialisation in the rule \<open>FVar\<close>.\<close>
| AVarE1: "\G\(\e1\,Norm s) \1 (\e1'\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>e1.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'.[e2]\<rangle>,s')"
| AVarE2: "G\(\e2\,Norm s) \1 (\e2'\,s')
\<Longrightarrow>
G\<turnstile>(\<langle>Lit a.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit a.[e2']\<rangle>,s')"
(* AVar: \<langle>(Lit a).[Lit i]\<rangle> is fully evaluated *)
(* evaluation of expression lists *)
\<comment> \<open>\<open>Nil\<close> is fully evaluated\<close>
| ConsHd: "\G\(\e::expr\,Norm s) \1 (\e'::expr\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>e#es\<rangle>,Norm s) \<mapsto>1 (\<langle>e'#es\<rangle>,s')"
| ConsTl: "\G\(\es\,Norm s) \1 (\es'\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>(Lit v)#es\<rangle>,Norm s) \<mapsto>1 (\<langle>(Lit v)#es'\<rangle>,s')"
(* execution of statements *)
(* cf. 14.5 *)
| Skip: "G\(\Skip\,Norm s) \1 (\SKIP\,Norm s)"
| ExprE: "\G\(\e\,Norm s) \1 (\e'\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>Expr e\<rangle>,Norm s) \<mapsto>1 (\<langle>Expr e'\<rangle>,s')"
| Expr: "G\(\Expr (Lit v)\,Norm s) \1 (\Skip\,Norm s)"
| LabC: "\G\(\c\,Norm s) \1 (\c'\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>l\<bullet> c\<rangle>,Norm s) \<mapsto>1 (\<langle>l\<bullet> c'\<rangle>,s')"
| Lab: "G\(\l\ Skip\,s) \1 (\Skip\, abupd (absorb l) s)"
(* cf. 14.2 *)
| CompC1: "\G\(\c1\,Norm s) \1 (\c1'\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>c1;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1';; c2\<rangle>,s')"
| Comp: "G\(\Skip;; c2\,Norm s) \1 (\c2\,Norm s)"
(* cf. 14.8.2 *)
| IfE: "\G\(\e\ ,Norm s) \1 (\e'\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>If(e) s1 Else s2\<rangle>,Norm s) \<mapsto>1 (\<langle>If(e') s1 Else s2\<rangle>,s')"
| If: "G\(\If(Lit v) s1 Else s2\,Norm s)
\<mapsto>1 (\<langle>if the_Bool v then s1 else s2\<rangle>,Norm s)"
(* cf. 14.10, 14.10.1 *)
| Loop: "G\(\l\ While(e) c\,Norm s)
\<mapsto>1 (\<langle>If(e) (Cont l\<bullet>c;; l\<bullet> While(e) c) Else Skip\<rangle>,Norm s)"
| Jmp: "G\(\Jmp j\,Norm s) \1 (\Skip\,(Some (Jump j), s))"
| ThrowE: "\G\(\e\,Norm s) \1 (\e'\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>Throw e\<rangle>,Norm s) \<mapsto>1 (\<langle>Throw e'\<rangle>,s')"
| Throw: "G\(\Throw (Lit a)\,Norm s) \1 (\Skip\,abupd (throw a) (Norm s))"
| TryC1: "\G\(\c1\,Norm s) \1 (\c1'\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>Try c1 Catch(C vn) c2\<rangle>, Norm s) \<mapsto>1 (\<langle>Try c1' Catch(C vn) c2\<rangle>,s')"
| Try: "\G\s \sxalloc\ s'\
\<Longrightarrow>
G\<turnstile>(\<langle>Try Skip Catch(C vn) c2\<rangle>, s)
\<mapsto>1 (if G,s'\<turnstile>catch C then (\<langle>c2\<rangle>,new_xcpt_var vn s')
else (\<langle>Skip\<rangle>,s'))"
| FinC1: "\G\(\c1\,Norm s) \1 (\c1'\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>c1 Finally c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1' Finally c2\<rangle>,s')"
| Fin: "G\(\Skip Finally c2\,(a,s)) \1 (\FinA a c2\,Norm s)"
| FinAC: "\G\(\c\,s) \1 (\c'\,s')\
\<Longrightarrow>
G\<turnstile>(\<langle>FinA a c\<rangle>,s) \<mapsto>1 (\<langle>FinA a c'\<rangle>,s')"
| FinA: "G\(\FinA a Skip\,s) \1 (\Skip\,abupd (abrupt_if (a\None) a) s)"
| Init1: "\inited C (globs s)\
\<Longrightarrow>
G\<turnstile>(\<langle>Init C\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)"
| Init: "\the (class G C)=c; \ inited C (globs s)\
\<Longrightarrow>
G\<turnstile>(\<langle>Init C\<rangle>,Norm s)
\<mapsto>1 (\<langle>(if C = Object then Skip else (Init (super c)));;
Expr (Callee (locals s) (InsInitE (init c) SKIP))\<rangle>
,Norm (init_class_obj G C s))"
\<comment> \<open>\<open>InsInitE\<close> is just used as trick to embed the statement
\<open>init c\<close> into an expression\<close>
| InsInitESKIP:
"G\(\InsInitE Skip SKIP\,Norm s) \1 (\SKIP\,Norm s)"
abbreviation
stepn:: "[prog, term \ state,nat,term \ state] \ bool" ("_\_ \_ _"[61,82,82] 81)
where "G\p \n p' \ (p,p') \ {(x, y). step G x y}^^n"
abbreviation
steptr:: "[prog,term \ state,term \ state] \ bool" ("_\_ \* _"[61,82,82] 81)
where "G\p \* p' \ (p,p') \ {(x, y). step G x y}\<^sup>*"
(* Equivalenzen:
Bigstep zu Smallstep komplett.
Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots>
*)
(*
lemma imp_eval_trans:
assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
shows trans: "G\<turnstile>(t,s0) \<mapsto>* (\<langle>Lit v\<rangle>,s1)"
*)
(* Jetzt muss man bei trans natürlich wieder unterscheiden: Stmt, Expr, Var!
Sowas blödes:
Am besten den Terminus ground auf Var,Stmt,Expr hochziehen und dann
the_vals definieren\<dots>
G\<turnstile>(t,s0) \<mapsto>* (t',s1) \<and> the_vals t' = v
*)
end
¤ Dauer der Verarbeitung: 0.4 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
