src/HOL/Bali/Trans.thy
author schirmer
Fri Feb 22 11:26:44 2002 +0100 (2002-02-22)
changeset 12925 99131847fb93
parent 12858 6214f03d6d27
child 13337 f75dfc606ac7
permissions -rw-r--r--
Added check for field/method access to operational semantics and proved the acesses valid.
     1 (*  Title:      HOL/Bali/Trans.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Operational transition (small-step) semantics of the 
     7 execution of Java expressions and statements
     8 
     9 PRELIMINARY!!!!!!!!
    10 
    11 improvements over Java Specification 1.0 (cf. 15.11.4.4):
    12 * dynamic method lookup does not need to check the return type
    13 * throw raises a NullPointer exception if a null reference is given, and each
    14   throw of a system exception yield a fresh exception object (was not specified)
    15 * if there is not enough memory even to allocate an OutOfMemory exception,
    16   evaluation/execution fails, i.e. simply stops (was not specified)
    17 
    18 design issues:
    19 * Lit expressions and Skip statements are considered completely evaluated.
    20 * the expr entry in rules is redundant in case of exceptions, but its full
    21   inclusion helps to make the rule structure independent of exception occurence.
    22 * the rule format is such that the start state may contain an exception.
    23   ++ faciliates exception handling (to be added later)
    24   +  symmetry
    25 * the rules are defined carefully in order to be applicable even in not
    26   type-correct situations (yielding undefined values),
    27   e.g. the_Adr (Val (Bool b)) = arbitrary.
    28   ++ fewer rules 
    29   -  less readable because of auxiliary functions like the_Adr
    30   Alternative: "defensive" evaluation throwing some InternalError exception
    31                in case of (impossible, for correct programs) type mismatches
    32 
    33 simplifications:
    34 * just simple handling (i.e. propagation) of exceptions so far
    35 * dynamic method lookup does not check return type (should not be necessary)
    36 *)
    37 
    38 Trans = Eval +
    39 
    40 consts
    41   texpr_tstmt	:: "prog  (((expr  state)  (expr  state)) +
    42 		            ((stmt  state)  (stmt  state))) set"
    43 
    44 syntax (symbols)
    45   texpr :: "[prog, expr  state, expr  state]  bool "("__ 1 _"[61,82,82] 81)
    46   tstmt :: "[prog, stmt  state, stmt  state]  bool "("__ 1 _"[61,82,82] 81)
    47   Ref   :: "loc  expr"
    48 
    49 translations
    50 
    51   "Ge_s 1 ex_s'" == "Inl (e_s, ex_s')  texpr_tstmt G"
    52   "Gs_s 1 s'_s'" == "Inr (s_s, s'_s')  texpr_tstmt G"
    53   "Ref a" == "Lit (Addr a)"
    54 
    55 constdefs
    56   
    57   sub_expr_expr :: "(expr  expr)  prop"
    58   "sub_expr_expr ef  (G e s e' s'. G(   e,s) 1 (   e',s') 
    59 				     G(ef e,s) 1 (ef e',s'))"
    60 
    61 inductive "texpr_tstmt G" intrs 
    62 
    63 (* evaluation of expression *)
    64   (* cf. 15.5 *)
    65   XcptE	"v. e  Lit v 
    66 				  G(e,Some xc,s) 1 (Lit arbitrary,Some xc,s)"
    67 
    68  CastXX "PROP sub_expr_expr (Cast T)"
    69 
    70 (*
    71   (* cf. 15.8.1 *)
    72   NewC	"new_Addr (heap s) = Some (a,x);
    73 	  s' = assign (hupd[ainit_Obj G C]s) (x,s) 
    74 				G(NewC C,None,s) 1 (Ref a,s')"
    75 
    76   (* cf. 15.9.1 *)
    77 (*NewA1	"sub_expr_expr (NewA T)"*)
    78   NewA1	"G(e,None,s) 1 (e',s') 
    79 			      G(New T[e],None,s) 1 (New T[e'],s')"
    80   NewA	"i = the_Intg i'; new_Addr (heap s) = Some (a, x);
    81 	  s' = assign (hupd[ainit_Arr T i]s)(raise_if (i<#0) NegArrSize x,s) 
    82 			G(New T[Lit i'],None,s) 1 (Ref a,s')"
    83   (* cf. 15.15 *)
    84   Cast1	"G(e,None,s) 1 (e',s') 
    85 			      G(Cast T e,None,s) 1 (Cast T e',s')"
    86   Cast	"x'= raise_if (\<questiondown>G,sv fits T) ClassCast None 
    87 		        G(Cast T (Lit v),None,s) 1 (Lit v,x',s)"
    88 
    89   (* cf. 15.7.1 *)
    90 (*Lit				"G(Lit v,None,s) 1 (Lit v,None,s)"*)
    91 
    92   (* cf. 15.13.1, 15.2 *)
    93   LAcc	"v = the (locals s vn) 
    94 			       G(LAcc vn,None,s) 1 (Lit v,None,s)"
    95 
    96   (* cf. 15.25.1 *)
    97   LAss1	"G(e,None,s) 1 (e',s') 
    98 				 G(f vn:=e,None,s) 1 (vn:=e',s')"
    99   LAss			    "G(f vn:=Lit v,None,s) 1 (Lit v,None,lupd[vnv]s)"
   100 
   101   (* cf. 15.10.1, 15.2 *)
   102   FAcc1	"G(e,None,s) 1 (e',s') 
   103 			       G({T}e..fn,None,s) 1 ({T}e'..fn,s')"
   104   FAcc	"v = the (snd (the_Obj (heap s (the_Addr a'))) (fn,T)) 
   105 			  G({T}Lit a'..fn,None,s) 1 (Lit v,np a' None,s)"
   106 
   107   (* cf. 15.25.1 *)
   108   FAss1	"G(e1,None,s) 1 (e1',s') 
   109 			  G(f ({T}e1..fn):=e2,None,s) 1 (f({T}e1'..fn):=e2,s')"
   110   FAss2	"G(e2,np a' None,s) 1 (e2',s') 
   111 		      G(f({T}Lit a'..fn):=e2,None,s) 1 (f({T}Lit a'..fn):=e2',s')"
   112   FAss	"a = the_Addr a'; (c,fs) = the_Obj (heap s a);
   113 	  s'= assign (hupd[aObj c (fs[(fn,T)v])]s) (None,s) 
   114 		   G(f({T}Lit a'..fn):=Lit v,None,s) 1 (Lit v,s')"
   115 
   116 
   117 
   118 
   119 
   120   (* cf. 15.12.1 *)
   121   AAcc1	"G(e1,None,s) 1 (e1',s') 
   122 				G(e1[e2],None,s) 1 (e1'[e2],s')"
   123   AAcc2	"G(e2,None,s) 1 (e2',s') 
   124 			    G(Lit a'[e2],None,s) 1 (Lit a'[e2'],s')"
   125   AAcc	"vo = snd (the_Arr (heap s (the_Addr a'))) (the_Intg i');
   126 	  x' = raise_if (vo = None) IndOutBound (np a' None) 
   127 			G(Lit a'[Lit i'],None,s) 1 (Lit (the vo),x',s)"
   128 
   129 
   130   (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
   131   Call1	"G(e,None,s) 1 (e',s') 
   132 			  G(e..mn({pT}p),None,s) 1 (e'..mn({pT}p),s')"
   133   Call2	"G(p,None,s) 1 (p',s') 
   134 		     G(Lit a'..mn({pT}p),None,s) 1 (Lit a'..mn({pT}p'),s')"
   135   Call	"a = the_Addr a'; (md,(pn,rT),lvars,blk,res) = 
   136  			   the (cmethd G (fst (the_Obj (h a))) (mn,pT)) 
   137 	    G(Lit a'..mn({pT}Lit pv),None,(h,l)) 1 
   138       (Body blk res l,np a' x,(h,init_vals lvars[Thisa'][Supera'][pnpv]))"
   139   Body1	"G(s0,None,s) 1 (s0',s') 
   140 		   G(Body s0    e      l,None,s) 1 (Body s0'  e  l,s')"
   141   Body2	"G(e ,None,s) 1 (e',s') 
   142 		   G(Body Skip  e      l,None,s) 1 (Body Skip e' l,s')"
   143   Body		  "G(Body Skip (Lit v) l,None,s) 1 (Lit v,None,(heap s,l))"
   144 
   145 (* execution of statements *)
   146 
   147   (* cf. 14.1 *)
   148   XcptS	"s0  Skip 
   149 				 G(s0,Some xc,s) 1 (Skip,Some xc,s)"
   150 
   151   (* cf. 14.5 *)
   152 (*Skip	 			 "G(Skip,None,s) 1 (Skip,None,s)"*)
   153 
   154   (* cf. 14.2 *)
   155   Comp1	"G(s1,None,s) 1 (s1',s') 
   156 			       G(s1;; s2,None,s) 1 (s1';; s2,s')"
   157   Comp			    "G(Skip;; s2,None,s) 1 (s2,None,s)"
   158 
   159 
   160 
   161 
   162 
   163 
   164   (* cf. 14.7 *)
   165   Expr1	"G(e ,None,s) 1 (e',s') 
   166 				G(Expr e,None,s) 1 (Expr e',s')"
   167   Expr			 "G(Expr (Lit v),None,s) 1 (Skip,None,s)"
   168 
   169   (* cf. 14.8.2 *)
   170   If1	"G(e ,None,s) 1 (e',s') 
   171 		      G(If(e) s1 Else s2,None,s) 1 (If(e') s1 Else s2,s')"
   172   If		 "G(If(Lit v) s1 Else s2,None,s) 1 
   173 		    (if the_Bool v then s1 else s2,None,s)"
   174 
   175   (* cf. 14.10, 14.10.1 *)
   176   Loop			  "G(While(e) s0,None,s) 1 
   177 			     (If(e) (s0;; While(e) s0) Else Skip,None,s)"
   178 *)
   179   con_defs "[sub_expr_expr_def]"
   180 
   181 end