State.thy

(*  Title:      isabelle/Bali/State.thy
    ID:         $Id: State.thy,v 1.8 1998/04/08 15:27:03 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen

State for evaluation of Java expressions and statements

design issues:
* new_Addr fails iff there is no free heap address. At the latest when there is
  only one free heap address left, it returns an OutOfMemory exception.
  In this way it is guaranteed that when an OutOfMemory exception is thrown for
  the first time, there is a free location on the heap to allocate it.
* unfortunately new_Addr is not directly executable because of Hilbert operator.

simplifications:
* lconf is designed to allow for (arbitrary) inaccessible values
* the stack of invocation frames containing local variables and return addresses
  for method calls is not explicitly modeled, nor finiteness constrains on it.
* garbage collection not considered
*)

State = WellForm +

types	fields_ (** clash with TypeRel.fields **)
	= "(ename * ref_ty, val) table" (* field name, defining class, value *)

	components
	= "(int           , val) table"	(* array elements *)

datatype obj		(* object *)
	= Obj tname fields_	(* class instance with class name and fields *)
	| Arr ty    components	(* array with component type and components *)

consts

  the_Obj	:: "obj option => tname * fields_"
  the_Arr	:: "obj option => ty * components"
  obj_ty	:: "obj => ty"

defs

 the_Obj_def	"the_Obj obj == @(C,fs). obj = Some (Obj C fs)"
 the_Arr_def	"the_Arr obj == @(T,cs). obj = Some (Arr T cs)"

primrec obj_ty obj

 "obj_ty (Obj C fs) = Class C"
 "obj_ty (Arr T cs) = T[.]"


datatype xcpt		(* exception *)
	= XcptLoc loc	(* location of allocated execption object *)
	| SysXcpt xname	(* intermediate system exception, see Eval.thy *)



consts

  the_XcptLoc	:: "xcpt => loc"
  the_SysXcpt	:: "xcpt => xname"

defs

  the_XcptLoc_def	"the_XcptLoc xc == @a. xc = XcptLoc a"
  the_SysXcpt_def	"the_SysXcpt xc == @x. xc = SysXcpt x"

types	aheap		(* heap *)
	= "(loc, obj) table"

	locals		(* local variables *)
	= "(ename, val) table"

	st		(* pure state, i.e. contents of all variables *)
	= "aheap * locals"
	(* heap, locals including This *)

	state		(* state including exception information *)
	 = "xcpt option * st"

syntax
  heap		:: "st => aheap"
  locals	:: "st => locals"
  Norm		:: "st => state"

translations
  "heap"	=> "fst"
  "locals"	=> "snd"
  "Norm s"      == "(None,s)"  

consts
  xcpt_ty	:: "st => xcpt => ty"

primrec xcpt_ty xcpt
       "xcpt_ty st (XcptLoc a ) = obj_ty (the (heap st a))"
       "xcpt_ty st (SysXcpt xn) = Class (SXcpt xn)"

constdefs

  new_Addr	:: "aheap => (loc * xcpt option) option"
 "new_Addr h	== @y.        y = None &   (!a. h a ~= None) | 
		       (? a x. y = Some (a,x) &  h a = None &  
		             (x = None |  x = Some (SysXcpt OutOfMemory)))"

  init_vars	:: "('a * ty) list => ('a, val) table"
 "init_vars	== table_of  o  map (%(n,T). (n,default_val T))"

  init_Obj	:: "prog => tname => obj"
 "init_Obj G C	== Obj C (init_vars (fields G C))"

  init_Arr	:: "ty => int => obj"
 "init_Arr T i  ==Arr T (%j. if $#0<=j &  j<i then Some (default_val T) else None)"

  raise_if	:: "bool => xname => xcpt option => xcpt option"
 "raise_if c xn xo == if c &  (xo = None) then Some (SysXcpt xn) else xo"

    lupd	:: "ename => val => st => st"        ("lupd[_|->_] _" [900,0,99] 900)
 "  lupd vn v	== %(h,l). (h,l[vn|->v])"

    hupd	:: "loc => obj => st => st"          ("hupd[_|->_] _" [900,0,99] 900)
 "  hupd a obj	== %(h,l). (h[a|->obj],l)"

  c_hupd	:: "loc => obj => state => state" ("c'_hupd[_|->_] _" [900,0,99] 900)
 "c_hupd a obj	== %(x,s). (x, if x = None then hupd[a|->obj] s else s)"

syntax

  np		:: "val => xcpt option => xcpt option"

translations

 "np v" == "raise_if (v = Null) NullPointer"

constdefs

  hext	:: "aheap => aheap => bool"               (     "_<=|_"     [51,51]       50)
	   "h<=|h' == !a obj.  h  a = Some obj --> 
	               (? obj'. h' a = Some obj' &  obj_ty obj' = obj_ty obj)"

  fits	:: "prog => aheap => val => ty => bool"   ("_,_|-_ fits _"  [51,51,51,51] 50)
 "G,h|-v fits T == ((? pt. T=PrimT pt) |  v=Null |  G|-obj_ty (the(h(the_Addr v)))<=:T)"

  conf	:: "prog => aheap => val => ty => bool"   ("_,_|-_::<=:_"     [51,51,51,51] 50)
	   "G,h|-v::<=:T == ? T'. typeof (option_map obj_ty  o  h) v = Some T' &  G|-T'<=:T"

  lconf	:: "prog => aheap => ('a, val) table => ('a, ty) table => bool"
					          ("_,_|-_[::<=:]_"   [51,51,51,51] 50)
	   "G,h|-vs[::<=:]Ts== !n T. Ts n = Some T --> (? v. vs n = Some v &  G,h|-v::<=:T)"

consts

  oconf	:: "prog => aheap => obj => bool"         ("_,_|-_::<=:<>"     [51,51,51]    50)

primrec oconf obj

 "G,h|-Obj C fs::<=:<> = (G,h|-fs[::<=:]table_of   (fields G C))"
 "G,h|-Arr T cs::<=:<> = (G,h|-cs[::<=:]option_map (%i. T)  o  cs)"

constdefs

  conforms :: "state => env => bool"              (     "_::<=:_"      [51,51]       50)
	      "xs::<=:E == let G = prg E; s = snd xs; h = heap s; l = locals s in
           (!a obj. h a = Some obj        --> G,h|-obj    ::<=:<>     ) & 
                                              G,h|-     l[::<=:](lcl E) & 
           (!a. fst xs = Some (XcptLoc a) --> G,h|-Addr a ::<=: Class(SXcpt Throwable))"

end

Theorems proved in State.ML:

obj

xcpt

new_Addr

raise_if

upd

hext

conf

fits

lconf

oconf

conforms

NewC

NewA

Cast

LAcc

LAss

FAcc

FAss

AAcc

AAss

Call

SXcpt

Throw