Trans.thy
Back to the index of Bali_ASCII
(* Title: isabelle/Bali/Trans.thy
ID: $Id: Trans.thy,v 1.2 1997/10/22 12:00:12 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
Operational transition (small-step) semantics of the
execution of Java expressions and statements
improvements over Java Specification 1.0 (cf. 15.11.4.4):
* dynamic method lookup does not need to check the return type
design concerns:
* 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 this pointer needs not to be included in the state on the right side,
but is retained for 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 = State +
consts
texpr_tstmt :: "prog => (((expr * state) * (expr * state)) +
((stmt * state) * (stmt * state))) set"
syntax (symbols)
texpr :: "[prog, expr * state, expr * state] => bool "("_|-_ ->1 _"[51,82,82] 81)
tstmt :: "[prog, stmt * state, stmt * state] => bool "("_|-_ |->1 _"[51,82,82] 81)
Ref :: "loc => expr"
(*sub_expr_expr :: "(expr => expr) => prop"*)
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)"
(*
"sub_expr_expr ef" == "!!G e0 s e' s'. G|-( e0,s) ->1 ( e',s')|] ==>
G|-(ef e0,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)"
(* cf. 15.7.2 *)
This "G|-(This,None,s) ->1 (Ref (this s),None,s)"
(* cf. 15.8.1 *)
NewC "[|h = heap s; (a,x) = new_Addr h;
h'= h[a:= Obj C (table (map (%(f,ft). (f,default_val ft))
(fields (G,C))))]|] ==>
G|-(NewC C,None,s) ->1 (Ref a,c_hupd h' (x,s))"
(* cf. 15.9.1 *)
(*NewA1 "sub_expr_expr (NewA T)"*)
NewA1 "[|G|-(e,None,s) ->1 (e',s')|] ==>
G|-(NewA T e,None,s) ->1 (NewA T e',s')"
NewA "[|i = the_Int i'; h = heap s; (a,x) = new_Addr h;
h'=h[a:=Arr T(%j. if $#0<=j & j<i then Some(default_val T) else None)];
x'= raise_if (i<$#0) NegArrSizeXcpt x|] ==>
G|-(NewA T (Lit i'),None,s) ->1 (Ref a,c_hupd h' (x',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 (~ cast_ok G T h v) ClassCastXcpt 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 "G|-(LAcc,None,s) ->1 (Lit (local s),None,s)"
(* cf. 15.25.1 *)
LAss1 "[|G|-(e,None,s) ->1 (e',s')|] ==>
G|-(LAss e,None,s) ->1 (LAss e',s')"
LAss "G|-(LAss (Lit v),None,(h,l,t)) ->1 (Lit v,None,(h,v,t))"
(* cf. 15.10.1, 15.2 *)
FAcc1 "[|G|-(e,None,s) ->1 (e',s')|] ==>
G|-(e{T}.fn,None,s) ->1 (e'{T}.fn,s')"
FAcc "[|v = the (snd (the_Obj (heap s (the_Addr a'))) (fn,T))|] ==>
G|-(Lit a'{T}.fn,None,s) ->1 (Lit v,np a' None,s)"
(* cf. 15.25.1 *)
FAss1 "[|G|-(e1,None,s) ->1 (e1',s')|] ==>
G|-(e1{T}.fn:=e2,None,s) ->1 (e1'{T}.fn:=e2,s')"
FAss2 "[|G|-(e2,np a' None,s) ->1 (e2',s')|] ==>
G|-(Lit a'{T}.fn:=e2,None,s) ->1 (Lit a'{T}.fn:=e2',s')"
FAss "[|a = the_Addr a'; h = heap s; (c,fs) = the_Obj (h a);
h'= h[a:=Obj c (fs[(fn,T):=v])]|] ==>
G|-(Lit a'{T}.fn:=Lit v,None,s) ->1 (Lit v,c_hupd h' (None,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_Int i');
x' = raise_if (vo = None) IndOutBoundXcpt (np a' None)|] ==>
G|-(Lit a'[Lit i'],None,s) ->1 (Lit (the vo),x',s)"
(* cf. 15.25.1 *)
AAss1 "[|G|-(e1,None,s) ->1 (e1',s')|] ==>
G|-(e1[e2]:=e3,None,s) ->1 (e1'[e2]:=e3,s')"
AAss2 "[|G|-(e2,None,s) ->1 (e2',s')|] ==>
G|-(Lit a'[e2]:=e3,None,s) ->1 (Lit a'[e2']:=e3,s')"
AAss3 "[|G|-(e3,None,s) ->1 (e3',s')|] ==>
G|-(Lit a'[Lit i']:=e3,None,s) ->1 (Lit a'[Lit i']:=e3',s')"
AAss "[|a = the_Addr a'; i = the_Int i';
h = heap s; (T,cs) = the_Arr (h a);
h'= h[a:=Arr T (cs[i:=v])];
x'= raise_if (~ cast_ok G T h v) ArrStoreXcpt
(raise_if (cs i = None) IndOutBoundXcpt (np a' None))|] ==>
G|-(e1[e2]:=e3,None,s) ->1 (Lit v,c_hupd h' (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{T}(p),None,s) ->1 (e'..mn{T}(p),s')"
Call2 "[|G|-(p,None,s) ->1 (p',s')|] ==>
G|-(Lit a'..mn{T}(p),None,s) ->1 (Lit a'..mn{T}(p'),s')"
Call "[|a = the_Addr a';
(md,mh,blk,res) = the (cmethd (G,fst (the_Obj (h a))) (mn,T))|] ==>
G|-(Lit a'..mn{T}(Lit p),None,(h,l,t)) ->1
(Body blk res l t,np a' x,(h,p,a))"
Body1 "[|G|-(s0,None,s) |->1 (s0',s')|] ==>
G|-(Body s0 e l t,None,s) ->1 (Body s0' e l t,s')"
Body2 "[|G|-(e ,None,s) ->1 (e',s')|] ==>
G|-(Body Skip e l t,None,s) ->1 (Body Skip e' l t,s')"
Body "G|-(Body Skip (Lit v) l t,None,s) ->1 (Lit v,None,(heap s,l,t))"
(* 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 *)
Cond1 "[|G|-(e ,None,s) ->1 (e',s')|] ==>
G|-(If(e) s1 Else s2,None,s) |->1 (If(e') s1 Else s2,s')"
Cond "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)"
end