src/HOL/Bali/Trans.thy
changeset 12925 99131847fb93
parent 12858 6214f03d6d27
child 13337 f75dfc606ac7
     1.1 --- a/src/HOL/Bali/Trans.thy	Thu Feb 21 20:11:32 2002 +0100
     1.2 +++ b/src/HOL/Bali/Trans.thy	Fri Feb 22 11:26:44 2002 +0100
     1.3 @@ -8,118 +8,153 @@
     1.4  
     1.5  PRELIMINARY!!!!!!!!
     1.6  
     1.7 +improvements over Java Specification 1.0 (cf. 15.11.4.4):
     1.8 +* dynamic method lookup does not need to check the return type
     1.9 +* throw raises a NullPointer exception if a null reference is given, and each
    1.10 +  throw of a system exception yield a fresh exception object (was not specified)
    1.11 +* if there is not enough memory even to allocate an OutOfMemory exception,
    1.12 +  evaluation/execution fails, i.e. simply stops (was not specified)
    1.13 +
    1.14 +design issues:
    1.15 +* Lit expressions and Skip statements are considered completely evaluated.
    1.16 +* the expr entry in rules is redundant in case of exceptions, but its full
    1.17 +  inclusion helps to make the rule structure independent of exception occurence.
    1.18 +* the rule format is such that the start state may contain an exception.
    1.19 +  ++ faciliates exception handling (to be added later)
    1.20 +  +  symmetry
    1.21 +* the rules are defined carefully in order to be applicable even in not
    1.22 +  type-correct situations (yielding undefined values),
    1.23 +  e.g. the_Adr (Val (Bool b)) = arbitrary.
    1.24 +  ++ fewer rules 
    1.25 +  -  less readable because of auxiliary functions like the_Adr
    1.26 +  Alternative: "defensive" evaluation throwing some InternalError exception
    1.27 +               in case of (impossible, for correct programs) type mismatches
    1.28 +
    1.29 +simplifications:
    1.30 +* just simple handling (i.e. propagation) of exceptions so far
    1.31 +* dynamic method lookup does not check return type (should not be necessary)
    1.32  *)
    1.33  
    1.34  Trans = Eval +
    1.35  
    1.36  consts
    1.37 -  texpr_tstmt	:: "prog \<Rightarrow> (((expr \<times> state) \<times> (expr \<times> state)) +
    1.38 -		            ((stmt \<times> state) \<times> (stmt \<times> state))) set"
    1.39 +  texpr_tstmt	:: "prog  (((expr  state)  (expr  state)) +
    1.40 +		            ((stmt  state)  (stmt  state))) set"
    1.41  
    1.42  syntax (symbols)
    1.43 -  texpr :: "[prog, expr \<times> state, expr \<times> state] \<Rightarrow> bool "("_\<turnstile>_ \<rightarrow>1 _"[61,82,82] 81)
    1.44 -  tstmt :: "[prog, stmt \<times> state, stmt \<times> state] \<Rightarrow> bool "("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)
    1.45 -  Ref   :: "loc \<Rightarrow> expr"
    1.46 +  texpr :: "[prog, expr  state, expr  state]  bool "("__ 1 _"[61,82,82] 81)
    1.47 +  tstmt :: "[prog, stmt  state, stmt  state]  bool "("__ 1 _"[61,82,82] 81)
    1.48 +  Ref   :: "loc  expr"
    1.49  
    1.50  translations
    1.51  
    1.52 -  "G\<turnstile>e_s \<rightarrow>1 ex_s'" == "Inl (e_s, ex_s') \<in> texpr_tstmt G"
    1.53 -  "G\<turnstile>s_s \<mapsto>1 s'_s'" == "Inr (s_s, s'_s') \<in> texpr_tstmt G"
    1.54 +  "Ge_s 1 ex_s'" == "Inl (e_s, ex_s')  texpr_tstmt G"
    1.55 +  "Gs_s 1 s'_s'" == "Inr (s_s, s'_s')  texpr_tstmt G"
    1.56    "Ref a" == "Lit (Addr a)"
    1.57  
    1.58 +constdefs
    1.59 +  
    1.60 +  sub_expr_expr :: "(expr  expr)  prop"
    1.61 +  "sub_expr_expr ef  (G e s e' s'. G(   e,s) 1 (   e',s') 
    1.62 +				     G(ef e,s) 1 (ef e',s'))"
    1.63 +
    1.64  inductive "texpr_tstmt G" intrs 
    1.65  
    1.66  (* evaluation of expression *)
    1.67    (* cf. 15.5 *)
    1.68 -  XcptE	"\<lbrakk>\<forall>v. e \<noteq> Lit v\<rbrakk> \\<Longrightarrow>
    1.69 -				  G\<turnstile>(e,Some xc,s) \<rightarrow>1 (Lit arbitrary,Some xc,s)"
    1.70 +  XcptE	"v. e  Lit v 
    1.71 +				  G(e,Some xc,s) 1 (Lit arbitrary,Some xc,s)"
    1.72  
    1.73 + CastXX "PROP sub_expr_expr (Cast T)"
    1.74 +
    1.75 +(*
    1.76    (* cf. 15.8.1 *)
    1.77 -  NewC	"\<lbrakk>new_Addr (heap s) = Some (a,x);
    1.78 -	  s' = assign (hupd[a\<mapsto>init_Obj G C]s) (x,s)\<rbrakk> \\<Longrightarrow>
    1.79 -				G\<turnstile>(NewC C,None,s) \<rightarrow>1 (Ref a,s')"
    1.80 +  NewC	"new_Addr (heap s) = Some (a,x);
    1.81 +	  s' = assign (hupd[ainit_Obj G C]s) (x,s) 
    1.82 +				G(NewC C,None,s) 1 (Ref a,s')"
    1.83  
    1.84    (* cf. 15.9.1 *)
    1.85 -  NewA1	"\<lbrakk>G\<turnstile>(e,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
    1.86 -			      G\<turnstile>(New T[e],None,s) \<rightarrow>1 (New T[e'],s')"
    1.87 -  NewA	"\<lbrakk>i = the_Intg i'; new_Addr (heap s) = Some (a, x);
    1.88 -	  s' = assign (hupd[a\<mapsto>init_Arr T i]s)(raise_if (i<#0) NegArrSize x,s)\<rbrakk> \\<Longrightarrow>
    1.89 -			G\<turnstile>(New T[Lit i'],None,s) \<rightarrow>1 (Ref a,s')"
    1.90 +(*NewA1	"sub_expr_expr (NewA T)"*)
    1.91 +  NewA1	"G(e,None,s) 1 (e',s') 
    1.92 +			      G(New T[e],None,s) 1 (New T[e'],s')"
    1.93 +  NewA	"i = the_Intg i'; new_Addr (heap s) = Some (a, x);
    1.94 +	  s' = assign (hupd[ainit_Arr T i]s)(raise_if (i<#0) NegArrSize x,s) 
    1.95 +			G(New T[Lit i'],None,s) 1 (Ref a,s')"
    1.96    (* cf. 15.15 *)
    1.97 -  Cast1	"\<lbrakk>G\<turnstile>(e,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
    1.98 -			      G\<turnstile>(Cast T e,None,s) \<rightarrow>1 (Cast T e',s')"
    1.99 -  Cast	"\<lbrakk>x'= raise_if (\<questiondown>G,s\<turnstile>v fits T) ClassCast None\<rbrakk> \\<Longrightarrow>
   1.100 -		        G\<turnstile>(Cast T (Lit v),None,s) \<rightarrow>1 (Lit v,x',s)"
   1.101 +  Cast1	"G(e,None,s) 1 (e',s') 
   1.102 +			      G(Cast T e,None,s) 1 (Cast T e',s')"
   1.103 +  Cast	"x'= raise_if (\<questiondown>G,sv fits T) ClassCast None 
   1.104 +		        G(Cast T (Lit v),None,s) 1 (Lit v,x',s)"
   1.105  
   1.106    (* cf. 15.7.1 *)
   1.107 -(*Lit				"G\<turnstile>(Lit v,None,s) \<rightarrow>1 (Lit v,None,s)"*)
   1.108 +(*Lit				"G(Lit v,None,s) 1 (Lit v,None,s)"*)
   1.109  
   1.110    (* cf. 15.13.1, 15.2 *)
   1.111 -  LAcc	"\<lbrakk>v = the (locals s vn)\<rbrakk> \\<Longrightarrow>
   1.112 -			       G\<turnstile>(LAcc vn,None,s) \<rightarrow>1 (Lit v,None,s)"
   1.113 +  LAcc	"v = the (locals s vn) 
   1.114 +			       G(LAcc vn,None,s) 1 (Lit v,None,s)"
   1.115  
   1.116    (* cf. 15.25.1 *)
   1.117 -  LAss1	"\<lbrakk>G\<turnstile>(e,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
   1.118 -				 G\<turnstile>(f vn:=e,None,s) \<rightarrow>1 (vn:=e',s')"
   1.119 -  LAss			    "G\<turnstile>(f vn:=Lit v,None,s) \<rightarrow>1 (Lit v,None,lupd[vn\<mapsto>v]s)"
   1.120 +  LAss1	"G(e,None,s) 1 (e',s') 
   1.121 +				 G(f vn:=e,None,s) 1 (vn:=e',s')"
   1.122 +  LAss			    "G(f vn:=Lit v,None,s) 1 (Lit v,None,lupd[vnv]s)"
   1.123  
   1.124    (* cf. 15.10.1, 15.2 *)
   1.125 -  FAcc1	"\<lbrakk>G\<turnstile>(e,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
   1.126 -			       G\<turnstile>({T}e..fn,None,s) \<rightarrow>1 ({T}e'..fn,s')"
   1.127 -  FAcc	"\<lbrakk>v = the (snd (the_Obj (heap s (the_Addr a'))) (fn,T))\<rbrakk> \\<Longrightarrow>
   1.128 -			  G\<turnstile>({T}Lit a'..fn,None,s) \<rightarrow>1 (Lit v,np a' None,s)"
   1.129 +  FAcc1	"G(e,None,s) 1 (e',s') 
   1.130 +			       G({T}e..fn,None,s) 1 ({T}e'..fn,s')"
   1.131 +  FAcc	"v = the (snd (the_Obj (heap s (the_Addr a'))) (fn,T)) 
   1.132 +			  G({T}Lit a'..fn,None,s) 1 (Lit v,np a' None,s)"
   1.133  
   1.134    (* cf. 15.25.1 *)
   1.135 -  FAss1	"\<lbrakk>G\<turnstile>(e1,None,s) \<rightarrow>1 (e1',s')\<rbrakk> \\<Longrightarrow>
   1.136 -			  G\<turnstile>(f ({T}e1..fn):=e2,None,s) \<rightarrow>1 (f({T}e1'..fn):=e2,s')"
   1.137 -  FAss2	"\<lbrakk>G\<turnstile>(e2,np a' None,s) \<rightarrow>1 (e2',s')\<rbrakk> \\<Longrightarrow>
   1.138 -		      G\<turnstile>(f({T}Lit a'..fn):=e2,None,s) \<rightarrow>1 (f({T}Lit a'..fn):=e2',s')"
   1.139 -  FAss	"\<lbrakk>a = the_Addr a'; (c,fs) = the_Obj (heap s a);
   1.140 -	  s'= assign (hupd[a\<mapsto>Obj c (fs[(fn,T)\<mapsto>v])]s) (None,s)\<rbrakk> \\<Longrightarrow>
   1.141 -		   G\<turnstile>(f({T}Lit a'..fn):=Lit v,None,s) \<rightarrow>1 (Lit v,s')"
   1.142 +  FAss1	"G(e1,None,s) 1 (e1',s') 
   1.143 +			  G(f ({T}e1..fn):=e2,None,s) 1 (f({T}e1'..fn):=e2,s')"
   1.144 +  FAss2	"G(e2,np a' None,s) 1 (e2',s') 
   1.145 +		      G(f({T}Lit a'..fn):=e2,None,s) 1 (f({T}Lit a'..fn):=e2',s')"
   1.146 +  FAss	"a = the_Addr a'; (c,fs) = the_Obj (heap s a);
   1.147 +	  s'= assign (hupd[aObj c (fs[(fn,T)v])]s) (None,s) 
   1.148 +		   G(f({T}Lit a'..fn):=Lit v,None,s) 1 (Lit v,s')"
   1.149  
   1.150  
   1.151  
   1.152  
   1.153  
   1.154    (* cf. 15.12.1 *)
   1.155 -  AAcc1	"\<lbrakk>G\<turnstile>(e1,None,s) \<rightarrow>1 (e1',s')\<rbrakk> \\<Longrightarrow>
   1.156 -				G\<turnstile>(e1[e2],None,s) \<rightarrow>1 (e1'[e2],s')"
   1.157 -  AAcc2	"\<lbrakk>G\<turnstile>(e2,None,s) \<rightarrow>1 (e2',s')\<rbrakk> \\<Longrightarrow>
   1.158 -			    G\<turnstile>(Lit a'[e2],None,s) \<rightarrow>1 (Lit a'[e2'],s')"
   1.159 -  AAcc	"\<lbrakk>vo = snd (the_Arr (heap s (the_Addr a'))) (the_Intg i');
   1.160 -	  x' = raise_if (vo = None) IndOutBound (np a' None)\<rbrakk> \\<Longrightarrow>
   1.161 -			G\<turnstile>(Lit a'[Lit i'],None,s) \<rightarrow>1 (Lit (the vo),x',s)"
   1.162 +  AAcc1	"G(e1,None,s) 1 (e1',s') 
   1.163 +				G(e1[e2],None,s) 1 (e1'[e2],s')"
   1.164 +  AAcc2	"G(e2,None,s) 1 (e2',s') 
   1.165 +			    G(Lit a'[e2],None,s) 1 (Lit a'[e2'],s')"
   1.166 +  AAcc	"vo = snd (the_Arr (heap s (the_Addr a'))) (the_Intg i');
   1.167 +	  x' = raise_if (vo = None) IndOutBound (np a' None) 
   1.168 +			G(Lit a'[Lit i'],None,s) 1 (Lit (the vo),x',s)"
   1.169  
   1.170  
   1.171    (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
   1.172 -  Call1	"\<lbrakk>G\<turnstile>(e,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
   1.173 -			  G\<turnstile>(e..mn({pT}p),None,s) \<rightarrow>1 (e'..mn({pT}p),s')"
   1.174 -  Call2	"\<lbrakk>G\<turnstile>(p,None,s) \<rightarrow>1 (p',s')\<rbrakk> \\<Longrightarrow>
   1.175 -		     G\<turnstile>(Lit a'..mn({pT}p),None,s) \<rightarrow>1 (Lit a'..mn({pT}p'),s')"
   1.176 -  Call	"\<lbrakk>a = the_Addr a'; (md,(pn,rT),lvars,blk,res) = 
   1.177 - 			   the (cmethd G (fst (the_Obj (h a))) (mn,pT))\<rbrakk> \\<Longrightarrow>
   1.178 -	    G\<turnstile>(Lit a'..mn({pT}Lit pv),None,(h,l)) \<rightarrow>1 
   1.179 -      (Body blk res l,np a' x,(h,init_vals lvars[This\<mapsto>a'][Super\<mapsto>a'][pn\<mapsto>pv]))"
   1.180 -  Body1	"\<lbrakk>G\<turnstile>(s0,None,s) \<mapsto>1 (s0',s')\<rbrakk> \\<Longrightarrow>
   1.181 -		   G\<turnstile>(Body s0    e      l,None,s) \<rightarrow>1 (Body s0'  e  l,s')"
   1.182 -  Body2	"\<lbrakk>G\<turnstile>(e ,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
   1.183 -		   G\<turnstile>(Body Skip  e      l,None,s) \<rightarrow>1 (Body Skip e' l,s')"
   1.184 -  Body		  "G\<turnstile>(Body Skip (Lit v) l,None,s) \<rightarrow>1 (Lit v,None,(heap s,l))"
   1.185 +  Call1	"G(e,None,s) 1 (e',s') 
   1.186 +			  G(e..mn({pT}p),None,s) 1 (e'..mn({pT}p),s')"
   1.187 +  Call2	"G(p,None,s) 1 (p',s') 
   1.188 +		     G(Lit a'..mn({pT}p),None,s) 1 (Lit a'..mn({pT}p'),s')"
   1.189 +  Call	"a = the_Addr a'; (md,(pn,rT),lvars,blk,res) = 
   1.190 + 			   the (cmethd G (fst (the_Obj (h a))) (mn,pT)) 
   1.191 +	    G(Lit a'..mn({pT}Lit pv),None,(h,l)) 1 
   1.192 +      (Body blk res l,np a' x,(h,init_vals lvars[Thisa'][Supera'][pnpv]))"
   1.193 +  Body1	"G(s0,None,s) 1 (s0',s') 
   1.194 +		   G(Body s0    e      l,None,s) 1 (Body s0'  e  l,s')"
   1.195 +  Body2	"G(e ,None,s) 1 (e',s') 
   1.196 +		   G(Body Skip  e      l,None,s) 1 (Body Skip e' l,s')"
   1.197 +  Body		  "G(Body Skip (Lit v) l,None,s) 1 (Lit v,None,(heap s,l))"
   1.198  
   1.199  (* execution of statements *)
   1.200  
   1.201    (* cf. 14.1 *)
   1.202 -  XcptS	"\<lbrakk>s0 \<noteq> Skip\<rbrakk> \\<Longrightarrow>
   1.203 -				 G\<turnstile>(s0,Some xc,s) \<mapsto>1 (Skip,Some xc,s)"
   1.204 +  XcptS	"s0  Skip 
   1.205 +				 G(s0,Some xc,s) 1 (Skip,Some xc,s)"
   1.206  
   1.207    (* cf. 14.5 *)
   1.208 -(*Skip	 			 "G\<turnstile>(Skip,None,s) \<mapsto>1 (Skip,None,s)"*)
   1.209 +(*Skip	 			 "G(Skip,None,s) 1 (Skip,None,s)"*)
   1.210  
   1.211    (* cf. 14.2 *)
   1.212 -  Comp1	"\<lbrakk>G\<turnstile>(s1,None,s) \<mapsto>1 (s1',s')\<rbrakk> \\<Longrightarrow>
   1.213 -			       G\<turnstile>(s1;; s2,None,s) \<mapsto>1 (s1';; s2,s')"
   1.214 -  Comp			    "G\<turnstile>(Skip;; s2,None,s) \<mapsto>1 (s2,None,s)"
   1.215 +  Comp1	"G(s1,None,s) 1 (s1',s') 
   1.216 +			       G(s1;; s2,None,s) 1 (s1';; s2,s')"
   1.217 +  Comp			    "G(Skip;; s2,None,s) 1 (s2,None,s)"
   1.218  
   1.219  
   1.220  
   1.221 @@ -127,18 +162,20 @@
   1.222  
   1.223  
   1.224    (* cf. 14.7 *)
   1.225 -  Expr1	"\<lbrakk>G\<turnstile>(e ,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
   1.226 -				G\<turnstile>(Expr e,None,s) \<mapsto>1 (Expr e',s')"
   1.227 -  Expr			 "G\<turnstile>(Expr (Lit v),None,s) \<mapsto>1 (Skip,None,s)"
   1.228 +  Expr1	"G(e ,None,s) 1 (e',s') 
   1.229 +				G(Expr e,None,s) 1 (Expr e',s')"
   1.230 +  Expr			 "G(Expr (Lit v),None,s) 1 (Skip,None,s)"
   1.231  
   1.232    (* cf. 14.8.2 *)
   1.233 -  If1	"\<lbrakk>G\<turnstile>(e ,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>
   1.234 -		      G\<turnstile>(If(e) s1 Else s2,None,s) \<mapsto>1 (If(e') s1 Else s2,s')"
   1.235 -  If		 "G\<turnstile>(If(Lit v) s1 Else s2,None,s) \<mapsto>1 
   1.236 +  If1	"G(e ,None,s) 1 (e',s') 
   1.237 +		      G(If(e) s1 Else s2,None,s) 1 (If(e') s1 Else s2,s')"
   1.238 +  If		 "G(If(Lit v) s1 Else s2,None,s) 1 
   1.239  		    (if the_Bool v then s1 else s2,None,s)"
   1.240  
   1.241    (* cf. 14.10, 14.10.1 *)
   1.242 -  Loop			  "G\<turnstile>(While(e) s0,None,s) \<mapsto>1 
   1.243 +  Loop			  "G(While(e) s0,None,s) 1 
   1.244  			     (If(e) (s0;; While(e) s0) Else Skip,None,s)"
   1.245 +*)
   1.246 +  con_defs "[sub_expr_expr_def]"
   1.247  
   1.248  end