src/HOL/Bali/Trans.thy

Added check for field/method access to operational semantics and proved the acesses valid.

(*  Title:      HOL/Bali/Trans.thy
    ID:         $Id$
    Author:     David von Oheimb
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

Operational transition (small-step) semantics of the 
execution of Java expressions and statements

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 ë (((expr ò state) ò (expr ò state)) +
		            ((stmt ò state) ò (stmt ò state))) set"

syntax (symbols)
  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É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	"ËÂ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	"Ë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	"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	"Ë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É(Lit v,None,s) è1 (Lit v,None,s)"*)

  (* cf. 15.13.1, 15.2 *)
  LAcc	"Ëv = the (locals s vn)Ì êë
			       GÉ(LAcc vn,None,s) è1 (Lit v,None,s)"

  (* cf. 15.25.1 *)
  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	"Ë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	"Ë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	"Ë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	"Ë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	"Ës0 Û SkipÌ êë
				 GÉ(s0,Some xc,s) í1 (Skip,Some xc,s)"

  (* cf. 14.5 *)
(*Skip	 			 "GÉ(Skip,None,s) í1 (Skip,None,s)"*)

  (* cf. 14.2 *)
  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)"






  (* cf. 14.7 *)
  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	"Ë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É(While(e) s0,None,s) í1 
			     (If(e) (s0;; While(e) s0) Else Skip,None,s)"
*)
  con_defs "[sub_expr_expr_def]"

end