Term.thy

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

Java expressions and statements

design issues:
* all variables may alternatively be handled in a very uniform way, by 
  representing arrays as special sort of class instances, and by 
  representing the current invocation frame as an instance of a special pseudo
  class (one per method definition) and identifying a special location called
  StackTop (as opposed to Heap) pointing to it. 
  Instead, we use a different approach for each kind of variable because: 
  +  it is closer to the language and therefore easier to read
  +  there is no extra handling (e.g. invariants) for special constructs 
     like StackTop needed
  -  there is more redundancy in the syntax and some semantic aspects 
     of variable access and assignment
* for the transition semantics, the method call produces an intermediate method
  body construct that enables the restoration of the previous 'stack' contents.
simplifications:
* expression statement allowed for any expression
* no super yet
* no unary, binary, ..., operators
* The This pointer is modeled as a special non-assignable local variable
* access to field x in current class via This.x
* NewA creates just one-dimensional arrays;
  initialization of further subarrays may be simulated with nested NewAs
* no constructors, initializers and finalizers yet
* for simplicity, the 'Lit' constructor is allowed to contain a reference value.
  But this is assumed to be prohibited in the input language, which is enforced
  by the type-checking rules.
* no synchronized
* result expression instead of return statement (see Decl.thy)
* no secondary forms of if, while (e.g. no for) (may be easily simulated)
* no switch, break, continue, no labels (may be simulated with while)
* the try_catch_finally statement is divided into the try_catch statement and
  a finally statement, which may be considered as try..finally with empty catch
* the try_catch statement has exactly one catch clause
* the compiler is supposed to add the annotations {_} during type-checking. This
  transformation is left out as its result is checked by the type rules anyway
*)
Term = Type + 

types   loc		(* locations, i.e. abstract references on objects *)
arities loc :: term

datatype val_ (** name not 'val' because of clash with ML token **)
	= Unit		(* dummy result value of void methods *)
	| Bool bool	(* Boolean value *)
	| Intg int	(* integer value *)
	| Null		(* null reference *)
	| Addr loc	(* addresses, i.e. locations of objects *)
types	      val   =         val_
translations "val" <= (type) "val_"
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"

constdefs

  the_Bool   :: "val => bool"
 "the_Bool v ==  @b. v = Bool b"
  the_Intg   :: "val => int"
 "the_Intg v ==  @i. v = Intg i"
  the_Addr   :: "val => loc"
 "the_Addr v ==  @a. v = Addr a"

datatype 'a e
	= NewC	tname		   (* class instance creation *)
	| NewA	ty ('a e)	   (* array creation *) ("New _[_]"[90,10   ]90)
	| Cast	ty ('a e)	   (* type cast *)
	| Lit	val		   (* literal value, references not allowed *)
	| LAcc	ename		   (* local (incl. parameter) access *)
	| LAss	ename	     ('a e)(* local assignment *)("_:=_"[      99,80]70)
	| FAcc ('a e) ref_ty ename (* field access *) ("_.{_}_"	[90,10,99   ]90)
	| FAss ('a e) ref_ty ename 
	                     ('a e)(* field ass. *)("_.{_}_:=_" [80,10,99,80]70)
	| AAcc ('a e)('a e)	   (* array access *) ("_[_]"	[90,10      ]90)
	| AAss ('a e)('a e)  ('a e)(* array ass. *)   ("_[_]:=_"[80,10,   80]70)
	| Call ('a e)mname ty('a e)(* method call*)("_.._{_}'(_')" [80,10,99]80)
	| Body  'a   ('a e) ((ename, val) table)  (* method body*)

datatype stmt
	= Skip			   (* empty      statement *)
	| Expr (stmt e)		   (* expression statement *)
	| Comp	stmt	stmt	   ("_;; _"			[      61,60]60)
	| Cond (stmt e)	stmt stmt  ("If'(_') _ Else _"		[   80,79,79]70)
	| Loop (stmt e)	stmt	   ("While'(_') _"		[      80,79]70)
	| Throw(stmt e)
	| TryC  stmt 
	         tname ename stmt  ("Try _ Catch'(_ _') _"	[79,80,80,79]70)
	| Fin   stmt    stmt	   ("_ Finally _" 		[      79,79]70)
types expr = stmt e

end