--- a/src/HOL/Bali/Trans.thy Thu Feb 21 20:11:32 2002 +0100
+++ b/src/HOL/Bali/Trans.thy Fri Feb 22 11:26:44 2002 +0100
@@ -8,118 +8,153 @@
PRELIMINARY!!!!!!!!
+improvements over Java Specification 1.0 (cf. 15.11.4.4):
+* dynamic method lookup does not need to check the return type
+* throw raises a NullPointer exception if a null reference is given, and each
+ throw of a system exception yield a fresh exception object (was not specified)
+* if there is not enough memory even to allocate an OutOfMemory exception,
+ evaluation/execution fails, i.e. simply stops (was not specified)
+
+design issues:
+* Lit expressions and Skip statements are considered completely evaluated.
+* the expr entry in rules is redundant in case of exceptions, but its full
+ inclusion helps to make the rule structure independent of exception occurence.
+* the rule format is such that the start state may contain an exception.
+ ++ faciliates exception handling (to be added later)
+ + symmetry
+* the rules are defined carefully in order to be applicable even in not
+ type-correct situations (yielding undefined values),
+ e.g. the_Adr (Val (Bool b)) = arbitrary.
+ ++ fewer rules
+ - less readable because of auxiliary functions like the_Adr
+ Alternative: "defensive" evaluation throwing some InternalError exception
+ in case of (impossible, for correct programs) type mismatches
+
+simplifications:
+* just simple handling (i.e. propagation) of exceptions so far
+* dynamic method lookup does not check return type (should not be necessary)
*)
Trans = Eval +
consts
- texpr_tstmt :: "prog \<Rightarrow> (((expr \<times> state) \<times> (expr \<times> state)) +
- ((stmt \<times> state) \<times> (stmt \<times> state))) set"
+ texpr_tstmt :: "prog ë (((expr ò state) ò (expr ò state)) +
+ ((stmt ò state) ò (stmt ò state))) set"
syntax (symbols)
- texpr :: "[prog, expr \<times> state, expr \<times> state] \<Rightarrow> bool "("_\<turnstile>_ \<rightarrow>1 _"[61,82,82] 81)
- tstmt :: "[prog, stmt \<times> state, stmt \<times> state] \<Rightarrow> bool "("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
- Ref :: "loc \<Rightarrow> expr"
+ texpr :: "[prog, expr ò state, expr ò state] ë bool "("_É_ è1 _"[61,82,82] 81)
+ tstmt :: "[prog, stmt ò state, stmt ò state] ë bool "("_É_ í1 _"[61,82,82] 81)
+ Ref :: "loc ë expr"
translations
- "G\<turnstile>e_s \<rightarrow>1 ex_s'" == "Inl (e_s, ex_s') \<in> texpr_tstmt G"
- "G\<turnstile>s_s \<mapsto>1 s'_s'" == "Inr (s_s, s'_s') \<in> texpr_tstmt G"
+ "GÉe_s è1 ex_s'" == "Inl (e_s, ex_s') Î texpr_tstmt G"
+ "GÉs_s í1 s'_s'" == "Inr (s_s, s'_s') Î texpr_tstmt G"
"Ref a" == "Lit (Addr a)"
+constdefs
+
+ sub_expr_expr :: "(expr ë expr) ë prop"
+ "sub_expr_expr ef Ú (ÄG e s e' s'. GÉ( e,s) è1 ( e',s') êë
+ GÉ(ef e,s) è1 (ef e',s'))"
+
inductive "texpr_tstmt G" intrs
(* evaluation of expression *)
(* cf. 15.5 *)
- XcptE "\<lbrakk>\<forall>v. e \<noteq> Lit v\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(e,Some xc,s) \<rightarrow>1 (Lit arbitrary,Some xc,s)"
+ XcptE "ËÂv. e Û Lit vÌ êë
+ GÉ(e,Some xc,s) è1 (Lit arbitrary,Some xc,s)"
+ CastXX "PROP sub_expr_expr (Cast T)"
+
+(*
(* cf. 15.8.1 *)
- NewC "\<lbrakk>new_Addr (heap s) = Some (a,x);
- s' = assign (hupd[a\<mapsto>init_Obj G C]s) (x,s)\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(NewC C,None,s) \<rightarrow>1 (Ref a,s')"
+ NewC "Ënew_Addr (heap s) = Some (a,x);
+ s' = assign (hupd[aíinit_Obj G C]s) (x,s)Ì êë
+ GÉ(NewC C,None,s) è1 (Ref a,s')"
(* cf. 15.9.1 *)
- NewA1 "\<lbrakk>G\<turnstile>(e,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(New T[e],None,s) \<rightarrow>1 (New T[e'],s')"
- NewA "\<lbrakk>i = the_Intg i'; new_Addr (heap s) = Some (a, x);
- s' = assign (hupd[a\<mapsto>init_Arr T i]s)(raise_if (i<#0) NegArrSize x,s)\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(New T[Lit i'],None,s) \<rightarrow>1 (Ref a,s')"
+(*NewA1 "sub_expr_expr (NewA T)"*)
+ NewA1 "ËGÉ(e,None,s) è1 (e',s')Ì êë
+ GÉ(New T[e],None,s) è1 (New T[e'],s')"
+ NewA "Ëi = the_Intg i'; new_Addr (heap s) = Some (a, x);
+ s' = assign (hupd[aíinit_Arr T i]s)(raise_if (i<#0) NegArrSize x,s)Ì êë
+ GÉ(New T[Lit i'],None,s) è1 (Ref a,s')"
(* cf. 15.15 *)
- Cast1 "\<lbrakk>G\<turnstile>(e,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(Cast T e,None,s) \<rightarrow>1 (Cast T e',s')"
- Cast "\<lbrakk>x'= raise_if (\<questiondown>G,s\<turnstile>v fits T) ClassCast None\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(Cast T (Lit v),None,s) \<rightarrow>1 (Lit v,x',s)"
+ Cast1 "ËGÉ(e,None,s) è1 (e',s')Ì êë
+ GÉ(Cast T e,None,s) è1 (Cast T e',s')"
+ Cast "Ëx'= raise_if (\<questiondown>G,sÉv fits T) ClassCast NoneÌ êë
+ GÉ(Cast T (Lit v),None,s) è1 (Lit v,x',s)"
(* cf. 15.7.1 *)
-(*Lit "G\<turnstile>(Lit v,None,s) \<rightarrow>1 (Lit v,None,s)"*)
+(*Lit "GÉ(Lit v,None,s) è1 (Lit v,None,s)"*)
(* cf. 15.13.1, 15.2 *)
- LAcc "\<lbrakk>v = the (locals s vn)\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(LAcc vn,None,s) \<rightarrow>1 (Lit v,None,s)"
+ LAcc "Ëv = the (locals s vn)Ì êë
+ GÉ(LAcc vn,None,s) è1 (Lit v,None,s)"
(* cf. 15.25.1 *)
- LAss1 "\<lbrakk>G\<turnstile>(e,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(f vn:=e,None,s) \<rightarrow>1 (vn:=e',s')"
- LAss "G\<turnstile>(f vn:=Lit v,None,s) \<rightarrow>1 (Lit v,None,lupd[vn\<mapsto>v]s)"
+ LAss1 "ËGÉ(e,None,s) è1 (e',s')Ì êë
+ GÉ(f vn:=e,None,s) è1 (vn:=e',s')"
+ LAss "GÉ(f vn:=Lit v,None,s) è1 (Lit v,None,lupd[vnív]s)"
(* cf. 15.10.1, 15.2 *)
- FAcc1 "\<lbrakk>G\<turnstile>(e,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
- G\<turnstile>({T}e..fn,None,s) \<rightarrow>1 ({T}e'..fn,s')"
- FAcc "\<lbrakk>v = the (snd (the_Obj (heap s (the_Addr a'))) (fn,T))\<rbrakk> \\<Longrightarrow>
- G\<turnstile>({T}Lit a'..fn,None,s) \<rightarrow>1 (Lit v,np a' None,s)"
+ FAcc1 "ËGÉ(e,None,s) è1 (e',s')Ì êë
+ GÉ({T}e..fn,None,s) è1 ({T}e'..fn,s')"
+ FAcc "Ëv = the (snd (the_Obj (heap s (the_Addr a'))) (fn,T))Ì êë
+ GÉ({T}Lit a'..fn,None,s) è1 (Lit v,np a' None,s)"
(* cf. 15.25.1 *)
- FAss1 "\<lbrakk>G\<turnstile>(e1,None,s) \<rightarrow>1 (e1',s')\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(f ({T}e1..fn):=e2,None,s) \<rightarrow>1 (f({T}e1'..fn):=e2,s')"
- FAss2 "\<lbrakk>G\<turnstile>(e2,np a' None,s) \<rightarrow>1 (e2',s')\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(f({T}Lit a'..fn):=e2,None,s) \<rightarrow>1 (f({T}Lit a'..fn):=e2',s')"
- FAss "\<lbrakk>a = the_Addr a'; (c,fs) = the_Obj (heap s a);
- s'= assign (hupd[a\<mapsto>Obj c (fs[(fn,T)\<mapsto>v])]s) (None,s)\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(f({T}Lit a'..fn):=Lit v,None,s) \<rightarrow>1 (Lit v,s')"
+ FAss1 "ËGÉ(e1,None,s) è1 (e1',s')Ì êë
+ GÉ(f ({T}e1..fn):=e2,None,s) è1 (f({T}e1'..fn):=e2,s')"
+ FAss2 "ËGÉ(e2,np a' None,s) è1 (e2',s')Ì êë
+ GÉ(f({T}Lit a'..fn):=e2,None,s) è1 (f({T}Lit a'..fn):=e2',s')"
+ FAss "Ëa = the_Addr a'; (c,fs) = the_Obj (heap s a);
+ s'= assign (hupd[aíObj c (fs[(fn,T)ív])]s) (None,s)Ì êë
+ GÉ(f({T}Lit a'..fn):=Lit v,None,s) è1 (Lit v,s')"
(* cf. 15.12.1 *)
- AAcc1 "\<lbrakk>G\<turnstile>(e1,None,s) \<rightarrow>1 (e1',s')\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(e1[e2],None,s) \<rightarrow>1 (e1'[e2],s')"
- AAcc2 "\<lbrakk>G\<turnstile>(e2,None,s) \<rightarrow>1 (e2',s')\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(Lit a'[e2],None,s) \<rightarrow>1 (Lit a'[e2'],s')"
- AAcc "\<lbrakk>vo = snd (the_Arr (heap s (the_Addr a'))) (the_Intg i');
- x' = raise_if (vo = None) IndOutBound (np a' None)\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(Lit a'[Lit i'],None,s) \<rightarrow>1 (Lit (the vo),x',s)"
+ AAcc1 "ËGÉ(e1,None,s) è1 (e1',s')Ì êë
+ GÉ(e1[e2],None,s) è1 (e1'[e2],s')"
+ AAcc2 "ËGÉ(e2,None,s) è1 (e2',s')Ì êë
+ GÉ(Lit a'[e2],None,s) è1 (Lit a'[e2'],s')"
+ AAcc "Ëvo = snd (the_Arr (heap s (the_Addr a'))) (the_Intg i');
+ x' = raise_if (vo = None) IndOutBound (np a' None)Ì êë
+ GÉ(Lit a'[Lit i'],None,s) è1 (Lit (the vo),x',s)"
(* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
- Call1 "\<lbrakk>G\<turnstile>(e,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(e..mn({pT}p),None,s) \<rightarrow>1 (e'..mn({pT}p),s')"
- Call2 "\<lbrakk>G\<turnstile>(p,None,s) \<rightarrow>1 (p',s')\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(Lit a'..mn({pT}p),None,s) \<rightarrow>1 (Lit a'..mn({pT}p'),s')"
- Call "\<lbrakk>a = the_Addr a'; (md,(pn,rT),lvars,blk,res) =
- the (cmethd G (fst (the_Obj (h a))) (mn,pT))\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(Lit a'..mn({pT}Lit pv),None,(h,l)) \<rightarrow>1
- (Body blk res l,np a' x,(h,init_vals lvars[This\<mapsto>a'][Super\<mapsto>a'][pn\<mapsto>pv]))"
- Body1 "\<lbrakk>G\<turnstile>(s0,None,s) \<mapsto>1 (s0',s')\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(Body s0 e l,None,s) \<rightarrow>1 (Body s0' e l,s')"
- Body2 "\<lbrakk>G\<turnstile>(e ,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(Body Skip e l,None,s) \<rightarrow>1 (Body Skip e' l,s')"
- Body "G\<turnstile>(Body Skip (Lit v) l,None,s) \<rightarrow>1 (Lit v,None,(heap s,l))"
+ Call1 "ËGÉ(e,None,s) è1 (e',s')Ì êë
+ GÉ(e..mn({pT}p),None,s) è1 (e'..mn({pT}p),s')"
+ Call2 "ËGÉ(p,None,s) è1 (p',s')Ì êë
+ GÉ(Lit a'..mn({pT}p),None,s) è1 (Lit a'..mn({pT}p'),s')"
+ Call "Ëa = the_Addr a'; (md,(pn,rT),lvars,blk,res) =
+ the (cmethd G (fst (the_Obj (h a))) (mn,pT))Ì êë
+ GÉ(Lit a'..mn({pT}Lit pv),None,(h,l)) è1
+ (Body blk res l,np a' x,(h,init_vals lvars[Thisía'][Supería'][pnípv]))"
+ Body1 "ËGÉ(s0,None,s) í1 (s0',s')Ì êë
+ GÉ(Body s0 e l,None,s) è1 (Body s0' e l,s')"
+ Body2 "ËGÉ(e ,None,s) è1 (e',s')Ì êë
+ GÉ(Body Skip e l,None,s) è1 (Body Skip e' l,s')"
+ Body "GÉ(Body Skip (Lit v) l,None,s) è1 (Lit v,None,(heap s,l))"
(* execution of statements *)
(* cf. 14.1 *)
- XcptS "\<lbrakk>s0 \<noteq> Skip\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(s0,Some xc,s) \<mapsto>1 (Skip,Some xc,s)"
+ XcptS "Ës0 Û SkipÌ êë
+ GÉ(s0,Some xc,s) í1 (Skip,Some xc,s)"
(* cf. 14.5 *)
-(*Skip "G\<turnstile>(Skip,None,s) \<mapsto>1 (Skip,None,s)"*)
+(*Skip "GÉ(Skip,None,s) í1 (Skip,None,s)"*)
(* cf. 14.2 *)
- Comp1 "\<lbrakk>G\<turnstile>(s1,None,s) \<mapsto>1 (s1',s')\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(s1;; s2,None,s) \<mapsto>1 (s1';; s2,s')"
- Comp "G\<turnstile>(Skip;; s2,None,s) \<mapsto>1 (s2,None,s)"
+ Comp1 "ËGÉ(s1,None,s) í1 (s1',s')Ì êë
+ GÉ(s1;; s2,None,s) í1 (s1';; s2,s')"
+ Comp "GÉ(Skip;; s2,None,s) í1 (s2,None,s)"
@@ -127,18 +162,20 @@
(* cf. 14.7 *)
- Expr1 "\<lbrakk>G\<turnstile>(e ,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(Expr e,None,s) \<mapsto>1 (Expr e',s')"
- Expr "G\<turnstile>(Expr (Lit v),None,s) \<mapsto>1 (Skip,None,s)"
+ Expr1 "ËGÉ(e ,None,s) è1 (e',s')Ì êë
+ GÉ(Expr e,None,s) í1 (Expr e',s')"
+ Expr "GÉ(Expr (Lit v),None,s) í1 (Skip,None,s)"
(* cf. 14.8.2 *)
- If1 "\<lbrakk>G\<turnstile>(e ,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
- G\<turnstile>(If(e) s1 Else s2,None,s) \<mapsto>1 (If(e') s1 Else s2,s')"
- If "G\<turnstile>(If(Lit v) s1 Else s2,None,s) \<mapsto>1
+ If1 "ËGÉ(e ,None,s) è1 (e',s')Ì êë
+ GÉ(If(e) s1 Else s2,None,s) í1 (If(e') s1 Else s2,s')"
+ If "GÉ(If(Lit v) s1 Else s2,None,s) í1
(if the_Bool v then s1 else s2,None,s)"
(* cf. 14.10, 14.10.1 *)
- Loop "G\<turnstile>(While(e) s0,None,s) \<mapsto>1
+ Loop "GÉ(While(e) s0,None,s) í1
(If(e) (s0;; While(e) s0) Else Skip,None,s)"
+*)
+ con_defs "[sub_expr_expr_def]"
end