State.thy

(*  Title:      isabelle/Bali/State.thy
    ID:         $Id: State.thy,v 1.2 1997/10/22 12:00:09 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen

State for evaluation of Java expressions and statements

simplifications:
* just primitive exceptions so far

*)

State = WellForm +

constdefs

  the_Bool	:: "val => bool"
 "the_Bool v  == @b. v = Bool b"

  the_Int	:: "val => int"
 "the_Int  v  == @i. v = Intg i"

  the_Addr	:: "val => loc"
 "the_Addr  v  == @a. v = Addr a"

consts

  defpval	:: "prim_ty => val"	(* default value for primitive types *)
  default_val	:: "ty => val"		(* default value for all types *)

primrec  defpval Type.prim_ty
	"defpval Void    = Unit"
	"defpval Boolean = Bool False"
	"defpval IntDefer = Intg ($# 0)"

primrec  default_val Type.ty
	"default_val (PrimT pt) = defpval pt"
	"default_val (RefT  r ) = Null"

types	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 *)

constdefs

  the_Obj	:: "obj option => tname * fields_"
 "the_Obj obj == case the obj of Obj C fs => (C, fs)   | Arr T cs => arbitrary"

  the_Arr	:: "obj option => ty * components"
 "the_Arr obj == case the obj of Obj C fs => arbitrary | Arr T cs => (T, cs)"

  obj_ty	:: "obj => ty"
 "obj_ty obj  == case obj of Obj C fs => Class C | Arr T cs => T[.]"

datatype xcpt		(* exceptions *)
	= NullPointerXcpt
	| NegArrSizeXcpt
	| IndOutBoundXcpt
	| ArrStoreXcpt
	| ClassCastXcpt
	| OutOfMemoryXcpt

types	aheap
	= "(loc, obj) table"

	st		(* simple state, i.e. variable contents *)
	= "aheap * val * loc"
	(* heap, local parameter, this *)

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

syntax
  heap		:: "st => (loc, obj) table"
 "local"	:: "st => val"
  this		:: "st => loc"
  Norm		:: "st => state"

translations
  "heap"	=> "first"
  "local"	=> "secnd"
  "this"	=> "third"
  "Norm s"      == "(None,s)"  

constdefs

  new_Addr	:: "aheap => loc * xcpt option"
 "new_Addr h == @(a,x). (h a = None &  x = None) |  x = Some OutOfMemoryXcpt"

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

  np		:: "val => xcpt option => xcpt option"
 "np v == raise_if (v = Null) NullPointerXcpt"

  c_hupd	:: "aheap => state => state"
 "c_hupd h'== %(xo,(h,l,t)). if xo = None then (None,(h',l,t)) else (xo,(h,l,t))"

  cast_ok	:: "prog => ty => aheap => val => bool"
 "cast_ok G T h v == ((? pt. T = PrimT pt) |  G|-obj_ty (the (h (the_Addr v)))<=:T)"

constdefs

  hconf :: "aheap => aheap => bool"		(  "_<=|_"   [51,51]       50)
	   "h<=|h' == !a obj. h a = Some obj --> (? fs' cs'. h' a = Some (
	 	            case obj of Obj C fs => Obj C fs'
			              | Arr T cs => Arr T cs'))"

  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"

(*###primrec?*)
  oconf :: "prog => aheap => obj => bool"		("_,_|-_@::<=:<>" [51,51,51]    50)
	   "G,h|-obj@::<=:<> == case obj of 
  Obj C fs => (!T f. table(fields(G,C))f=Some T --> (? v. fs f=Some v &  G,h|-v@::<=:T))
| Arr T cs => (!i v. cs i               =Some v -->                    G,h|-v@::<=:T)"

  conforms :: "st => env => bool"			(  "_@::<=:_"   [51,51]       50)
	  "s@::<=:E == (!a obj. heap s a = Some obj --> prg E,heap s|-obj@::<=:<>) & 
	            prg E,heap s|-     local s  @::<=:    localT E  & 
	            prg E,heap s|-Addr (this s) @::<=: Class (thisT E)"

end