Eval.thy
Back to the index of Bali_ASCII
(* Title: isabelle/Bali/Eval.thy
ID: $Id: Eval.thy,v 1.2 1997/10/22 12:00:07 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
Operational evaluation (big-step) semantics of the
execution of Java expressions and statements
question: does the Java specification thoroughly define
the effects of expressions/statements throwing an exception?
improvements over Java Specification 1.0 (cf. 15.11.4.4):
* dynamic method lookup does not need to check the return type
design concerns:
* evaluation vs. (one-step) transition semantics
evaluation semantics chosen, because:
++ less verbose and therefore easier to read (and to handle in proofs)
+ more abstract
+ intermediate values (appearing in recursive rules) need not be stored
explicitly, e.g. no call body construct necessary as opposed to trans. sem.
+ convenient rule induction for subject reduction theorem
- no interleaving (for parallelism) describable
- stating a property of infinite executions requires the meta-level argument
that this property holds for any finite prefixes of it (e.g. stopped using
a counter that is decremented to zero and then throwing an exception)
* the value 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
*)
Eval = State +
consts
eval_exec :: "prog => (state * (expr * val + stmt) * state) set"
syntax (symbols)
eval :: "[prog,state,expr,val,state] => bool "("_|-_ -_|>_-> _"[51,82,82,82,82]81)
exec :: "[prog,state,stmt, state] => bool "("_|-_ -_-> _" [51,82,82, 82]81)
translations
"G|-s -e0|>v-> s'" == "(s, Inl(e0,v), s') : eval_exec G"
"G|-s -s0 -> s'" == "(s, Inr s0 , s') : eval_exec G"
inductive "eval_exec G" intrs
(* evaluation of expressions *)
(* cf. 15.5 *)
XcptE "G|-(Some xc,s) -e|>arbitrary-> (Some xc,s)"
(* cf. 15.7.2 *)
This "G|-Norm s -This|>Addr (this s)-> Norm 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|-Norm s -NewC C|>Addr a-> c_hupd h' (x,s)"
(* cf. 15.9.1 *)
NewA "[|G|-Norm s0 -e|>i'-> (x1,s1); i = the_Int i';
h = heap s1; (a,x) = new_Addr h;
h'=h[a:=Arr T(%j. if $#0<=j & j<i then Some(default_val T) else None)];
x1'=raise_if (i<$#0) NegArrSizeXcpt (if x1 = None then x else x1)|] ==>
G|-Norm s0 -NewA T e|>Addr a-> c_hupd h' (x1',s1)"
(* cf. 15.15 *)
Cast "[|G|-Norm s0 -e|>v-> (x1,s1);
x2=raise_if (~ cast_ok G T (heap s1) v) ClassCastXcpt x1|] ==>
G|-Norm s0 -Cast T e|>v-> (x2,s1)"
(* cf. 15.7.1 *)
Lit "G|-Norm s -Lit v|>v-> Norm s"
(* cf. 15.13.1, 15.2 *)
LAcc "G|-Norm s -LAcc|>local s-> Norm s"
(* cf. 15.25.1 *)
LAss "[|G|-Norm s -e|>v-> (x,(h,l,t));
l' = (if x = None then v else l)|] ==>
G|-Norm s -LAss e|>v-> (x,(h,l',t))"
(* cf. 15.10.1, 15.2 *)
FAcc "[|G|-Norm s0 -e|>a'-> (x1,s1);
v = the (snd (the_Obj (heap s1 (the_Addr a'))) (fn,T))|] ==>
G|-Norm s0 -e{T}.fn|>v-> (np a' x1,s1)"
(* cf. 15.25.1 *)
FAss "[|G|- Norm s0 -e1|>a'-> (x1,s1); a = the_Addr a';
G|-(np a' x1,s1) -e2|>v -> (x2,s2);
h = heap s2; (c,fs) = the_Obj (h a);
h' = h[a:=Obj c (fs[(fn,T):=v])]|] ==>
G|-Norm s0 -(e1{T}.fn:=e2)|>v-> c_hupd h' (x2,s2)"
(* cf. 15.12.1 *)
AAcc "[|G|- Norm s0 -e1|>a'-> s1 ;
G|- s1 -e2|>i'-> (x2,s2);
vo = snd (the_Arr (heap s2 (the_Addr a'))) (the_Int i');
x3 = raise_if (vo = None) IndOutBoundXcpt (np a' x2)|] ==>
G|-Norm s0 -e1[e2]|>the vo-> (x3,s2)"
(* cf. 15.25.1 *)
AAss "[|G|- Norm s0 -e1|>a'-> s1 ; a = the_Addr a';
G|- s1 -e2|>i'-> s2 ; i = the_Int i';
G|- s2 -e3|>v -> (x3,s3);
h = heap s3; (T,cs) = the_Arr (h a);
h' = h[a:=Arr T (cs[i:=v])];
x3'= raise_if (~ cast_ok G T h v) ArrStoreXcpt
(raise_if (cs i = None) IndOutBoundXcpt (np a' x3))|] ==>
G|-Norm s0 -(e1[e2]:=e3)|>v-> c_hupd h' (x3',s3)"
(* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
Call "[|G|-Norm s0 -e|>a'-> s1 ; a = the_Addr a';
G|- s1 -p|>pv-> (x,(h,l,t)); dynT = fst (the_Obj (h a));
(md,mh,blk,res) = the (cmethd (G,dynT) (mn,T));
G|-(np a' x,(h,pv,a)) -blk->s3;
G|- s3 -res|>v -> (x4,s4)|] ==>
G|-Norm s0 -(e..mn{T}(p))|>v-> (x4,(heap s4,l,t))"
(* execution of statements *)
(* cf. 14.1 *)
XcptS "G|-(Some xc,s) -s0-> (Some xc,s)"
(* cf. 14.5 *)
Skip "G|-Norm s -Skip-> Norm s"
(* cf. 14.7 *)
Expr "[|G|-Norm s0 -e|>v-> s1|] ==>
G|-Norm s0 -Expr e-> s1"
(* cf. 14.2 *)
Comp "[|G|-Norm s0 -s -> s1;
G|- s1 -t -> s2|] ==>
G|-Norm s0 -(s;; t)-> s2"
(* cf. 14.8.2 *)
Cond "[|G|-Norm s0 -e |>v-> s1;
G|- s1 -(if the_Bool v then s else t)-> s2|] ==>
G|-Norm s0 -(If(e) s Else t)-> s2"
(* cf. 14.10, 14.10.1 *)
Loop "[|G|-Norm s0 -(If(e) (s;; While(e) s) Else Skip)-> s1|] ==>
G|-Norm s0 -(While(e) s)-> s1"
end