Example.thy

(*  Title:      isabelle/Bali/Example.thy
    ID:         $Id: Example.thy,v 1.2 1998/04/08 15:26:59 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen

The following Bali example program includes:
 class declarations with inheritance, hiding of fields, and overriding of
  methods (with refined result type), 
 instance creation, local assignment, sequential composition,
 try & catch, method call with dynamic binding, literal values,
 expression statement, local access, type cast, field assignment (in part), skip

class Base {
  boolean vee;
  Base foo(Base x) {return x;}
}

class Ext extends Base{
  int vee;
  Ext foo(Base x) {((Ext)x).vee=1; return null;}
}


class Example {
  public static void main (String args[]) {
    Base e;
    e=new Ext();
    try {e.foo(null); }
    catch (NullPointerException x) {}
  }
}
*)

Example = Eval + 

datatype tnam_ = Base_ | Ext_
datatype enam_ = vee_  | x_ | e_

consts

  tnam_ :: "tnam_ => tnam"
  enam_ :: "enam_ => enam"

rules (* tnam_ and enam_ are intended to be isomorphic to tnam and enam *)

  inj_tnam_  "(tnam_ x = tnam_ y) = (x = y)"
  inj_enam_  "(enam_ x = enam_ y) = (x = y)"

  surj_tnam_ "? m. n = tnam_ m"
  surj_enam_ "? m. n = enam_ m"






syntax

  Base,  Ext	:: tname
  vee, x, e	:: ename

translations

  "Base" == "TName (tnam_ Base_)"
  "Ext"	 == "TName (tnam_ Ext_)"
  "vee"  == "EName (enam_ vee_)"
  "x"	 == "EName (enam_ x_)"
  "e"	 == "EName (enam_ e_)"


consts

  system_classes :: cdecl list
  tprg		 :: prog
  BaseC, ExtC    :: cdecl
  test		 :: stmt
  foo	         :: mname
  a,b		 :: loc

defs

  BaseC_def     "BaseC == (Base, (Some Object, [], 
				[(vee, PrimT Boolean)], 
				[((foo,Class Base),(x,Class Base),
				  ([],Skip,LAcc x))]))"
  ExtC_def	"ExtC  == (Ext,  (Some Base  , [], 
				[(vee, PrimT IntDefer)], 
				[((foo,Class Base),(x,Class Ext),
				  ([],Expr(Cast (Class Ext) (LAcc x).{ClassT 
				      Ext}vee:=Lit (Intg ($#1))),Lit Null))]))"

  system_classes_def "system_classes == [ObjectC, SXcptC Throwable,
		SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast,
		SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]"

  tprg_def "tprg == ([],system_classes@[BaseC,ExtC])"

  test_def "test == Expr(e:=NewC Ext);; 
		   Try Expr(LAcc e..foo{Class Base}(Lit Null))
		   Catch(SXcpt NullPointer x) (Throw (LAcc x))"












syntax

  NP		:: xname
  "classes"	:: cdecl list
  obj1, obj2	:: obj
  s0,s1,s2,s3,s4,s5,s6,s7:: state

translations

  "NP"   == "NullPointer"
  "classes" == "[ObjectC, SXcptC Throwable, 
		 SXcptC NP         , SXcptC OutOfMemory, SXcptC ClassCast, 
		 SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore , 
		 BaseC, ExtC]"
  "obj1" == "Obj Ext (empty[(vee, ClassT Base)|->Bool False ]
                           [(vee, ClassT Ext )|->Intg ($# 0)])"
  "obj2" == "Obj (SXcpt NP) empty"
  "s0" == " Norm              (empty                ,empty)"
  "s1" == " Norm              (empty[a|->obj1]        ,empty[e|->Addr a])"
  "s2" == " Norm              (empty[a|->obj1]        , 
						empty[This|->Addr a][x|->Null])"
  "s3" == "(Some (SysXcpt NP), empty[a|->obj1]        , 
						empty[This|->Addr a][x|->Null])"
  "s4" == "(Some (SysXcpt NP), empty[a|->obj1]        ,empty[e|->Addr a])"
  "s5" == "(Some (XcptLoc b ), empty[a|->obj1][b|->obj2],empty[e|->Addr a])"
  "s6" == " Norm              (empty[a|->obj1][b|->obj2],empty[e|->Addr a][x|->Addr b])"
  "s7" == "(Some (XcptLoc b ), empty[a|->obj1][b|->obj2],empty[e|->Addr a][x|->Addr b])"

end