Eval.thy
Back to the index of Bali_ASCII2
(* Title: isabelle/Bali/Eval.thy
ID: $Id: Eval.thy,v 1.9 1998/04/08 15:26:57 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
Operational evaluation (big-step) semantics of the
execution of Java expressions and statements
improvements over Java Specification 1.0:
* dynamic method lookup does not need to check the return type (cf. 15.11.4.4)
* 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:
* 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
+ 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
* the allocation of objects that represent system exceptions is deferred until
the end of the (if any) enclosing try block; this helps to avoid (conditional)
side effects on the heap and problems with out-of-memory conditions
* there is exacly one rule (except for Try_Catch) per syntactic construct
+ no redundancy in case distinctions
rule split for Try_Catch because of conditional execution of its catch clause,
which would require recursion in a conditional formula (not permitted by the
current implementation of the inductive package) or the alternative execution
of a Skip statement (requires several occurences of the case distinction)
* if a system exception is raised while evaluating an expression, the allocation
of a corresponding exceptions is deferred until execution of some statement
after it, but before any catch clause. This is transparent to the program.
- a kind of non-determinism
- an extra, even not syntax-driven, rule (SXcpt)
+ extra rule avoids redundany in the two Try_Catch rules
++ avoids copies of allocation code and awkward case distinctions (whether
there is enough memory to allocate the exception) in evaluation rules
*)
Eval = State + inductive2 +
consts
eval :: "prog => (state * (expr * val) * state) set"
exec :: "prog => (state * 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, (e0,v), s') : eval G"
"G|-s -s0 -> s'" == "(s, s0 , s') : exec G"
myinductive "eval G" "exec G" intrs
(* evaluation of expressions *)
(* cf. 15.5 *)
XcptE "G|-(Some xc,s) -e:>arbitrary-> (Some xc,s)"
(* cf. 15.8.1 *)
NewC "[|new_Addr (heap s) = Some (a,x)|] ==>
G|-Norm s -NewC C:>Addr a-> c_hupd[a|->init_Obj G C](x,s)"
(* cf. 15.9.1 *)
NewA "[|G|-Norm s0 -e:>i'-> (x1,s1); i = the_Intg i';
new_Addr (heap s1) = Some (a,x);
x1' = raise_if (i<$#0) NegArrSize (if x1 = None then x else x1)|] ==>
G|-Norm s0 -New T[e]:>Addr a-> c_hupd[a|->init_Arr T i](x1',s1)"
(* cf. 15.15 *)
Cast "[|G|-Norm s0 -e:>v-> (x1,s1);
x2 = raise_if (~ G,heap s1|-v fits T) ClassCast 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, 15.7.2 *)
LAcc "G|-Norm s -LAcc vn:>the (locals s vn)-> Norm s"
(* cf. 15.25.1 *)
LAss "[|G|-Norm s0 -e:>v-> (x,s1);
s1' = (if x = None then lupd[vn|->v]s1 else s1)|] ==>
G|-Norm s0 -(vn:=e):>v-> (x,s1')"
(* 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);
(c,fs) = the_Obj (heap s2 a); obj = Obj c (fs[(fn,T)|->v])|] ==>
G|-Norm s0 -(e1.{T}fn:=e2):>v-> c_hupd[a|->obj](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_Intg i');
x3 = raise_if (vo = None) IndOutBound (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_Intg i';
G|- s2 -e3:>v -> (x3,s3);
(T,cs) = the_Arr (heap s3 a); obj = Arr T (cs[i|->v]);
x3'= raise_if (~ G,heap s3|-v fits T) ArrStore
(raise_if (cs i = None) IndOutBound (np a' x3))|] ==>
G|-Norm s0 -(e1[e2]:=e3):>v-> c_hupd[a|->obj](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;
G|- s1 -p:>pv-> (x2,(h,l)); dynT = fst(the_Obj (h (the_Addr a')));
(md,(pn,rT),lvars,blk,res) = the (cmethd G dynT (mn,pT));
G|-(np a' x2,(h,init_vars lvars[This|->a'][pn|->pv])) -blk->s3;
G|- s3 -res:>v -> (x4,s4)|] ==>
G|-Norm s0 -(e..mn{pT}(p)):>v-> (x4,(heap s4,l))"
(* execution of statements *)
(* cf. 14.1 *)
XcptS "G|-(Some xc,s) -c-> (Some xc,s)"
(* allocation of exception object for system exceptions *)
SXcpt "[|G|-Norm s0 -c-> (Some (SysXcpt xn),s1);
new_Addr (heap s1) = Some (a,x);
xobj = init_Obj G (SXcpt (if x = None then xn else OutOfMemory))|] ==>
G|-Norm s0 -c-> (Some (XcptLoc a),hupd[a|->xobj]s1)"
(* 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 -c1 -> s1;
G|- s1 -c2 -> s2|] ==>
G|-Norm s0 -(c1;; c2)-> s2"
(* cf. 14.8.2 *)
Cond "[|G|-Norm s0 -e:>v-> s1;
G|- s1-(if the_Bool v then c1 else c2)-> s2|] ==>
G|-Norm s0 -(If(e) c1 Else c2)-> s2"
(* cf. 14.10, 14.10.1 *)
Loop "[|G|-Norm s0 -(If(e) (c;; While(e) c) Else Skip)-> s1|] ==>
G|-Norm s0 -(While(e) c)-> s1"
(* cf. 14.16 *)
Throw "[|G|-Norm s0 -e:>a'-> (x1,s1); x1' = np a' x1;
x1''=(if x1'=None then (Some (XcptLoc (the_Addr a'))) else x1')|] ==>
G|-Norm s0 -Throw e-> (x1'',s1)"
(* cf. 14.18.1 *)
Try1 "[|G|-Norm s0 -c1-> (Some (XcptLoc a),s1);
G|-xcpt_ty s1 (XcptLoc a)<=:Class tn;
G|-Norm(lupd[vn|->Addr a]s1) -c2-> s2|] ==>
G|-Norm s0 -(Try c1 Catch(tn vn) c2)-> s2"
Try2 "[|G|-Norm s0 -c1-> (x1,s1);
x1=None | x1=Some (XcptLoc a) & ~ G|-xcpt_ty s1 (XcptLoc a)<=:Class tn|] ==>
G|-Norm s0 -(Try c1 Catch(tn vn) c2)-> (x1,s1)"
(* cf. 14.18.2 *)
Fin "[|G|-Norm s0 -c1 -> (x1,s1);
G|-Norm s1 -c2 -> (x2,s2);
x2' = (if x1 ~= None & x2 = None then x1 else x2)|] ==>
G|-Norm s0 -(c1 Finally c2)-> (x2',s2)"
end
Theorems proved in Eval.ML:
split_eta3
(%(x,y,z). f (x, y, z)) = f
Try_intro
[|G|-Norm s0 -c1-> x1, s1;
option_case ((x1', s1') = (x1, s1))
(xcpt_case (%a. (x1', s1') = (x1, s1))
(%xn. new_Addr (fst s1) = Some (a, x) &
(x1', s1') =
(Some (XcptLoc a), hupd[a|->init_Obj G (SXcpt (if x = None then xn else OutOfMemory))] s1)))
x1;
catch = (? a. x1' = Some (XcptLoc a) & G|-xcpt_ty s1' (XcptLoc a)<=:Class tn);
G|-(if catch then None else x1',
if catch then lupd[vn|->Addr (the_XcptLoc (the x1'))] s1' else s1') -(if catch then c2 else Skip)-> s2|]
==> G|-Norm s0 -(Try c1 Catch(tn vn) c2)-> s2
eval_exec_type_sound
wf_prog G ==>
(G|-(x, h, l) -e:>v-> x', h', l' -->
(!L. (x, h, l)::<=:(G, L) -->
(!T. (G, L)|-e::T --> h<=|h' & (x', h', l')::<=:(G, L) & (x' = None --> G,h'|-v::<=:T)))) &
(G|-(x, h, l) -c-> x', h', l' --> (!L. (x, h, l)::<=:(G, L) --> (G, L)|-c::<> --> h<=|h' & (x', h', l')::<=:(G, L)))
eval_type_sound
[|E = (G, L); wf_prog G; G|-s -e:>v-> x', s'; s::<=:E; E|-e::T|]
==> (x', s')::<=:E & (x' = None --> G,fst s'|-v::<=:T)
exec_type_sound
[|E = (G, L); wf_prog G; G|-s -s0-> s'; s::<=:E; E|-s0::<>|] ==> s'::<=:E
all_methods_understood
[|E = (G, L); wf_prog G; G|-s -e:>a'-> Norm s'; a' ~= Null; s::<=:E; E|-e::RefT T; mheads G T sig ~= {}|]
==> cmethd G (fst (the_Obj (fst s' (the_Addr a')))) sig ~= None