--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/Example.thy Fri Jul 14 16:32:51 2000 +0200
@@ -0,0 +1,117 @@
+(* Title: isabelle/Bali/Example.thy
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1997 Technische Universitaet Muenchen
+
+The following example Bali program includes:
+ class declarations with inheritance, hiding of fields, and overriding of
+ methods (with refined result type),
+ instance creation, local assignment, sequential composition,
+ 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 cnam_ = Base_ | Ext_
+datatype vnam_ = vee_ | x_ | e_
+
+consts
+
+ cnam_ :: "cnam_ \\<Rightarrow> cname"
+ vnam_ :: "vnam_ \\<Rightarrow> vnam"
+
+rules (* cnam_ and vnam_ are intended to be isomorphic to cnam and vnam *)
+
+ inj_cnam_ "(cnam_ x = cnam_ y) = (x = y)"
+ inj_vnam_ "(vnam_ x = vnam_ y) = (x = y)"
+
+ surj_cnam_ "\\<exists>m. n = cnam_ m"
+ surj_vnam_ "\\<exists>m. n = vnam_ m"
+
+syntax
+
+ Base, Ext :: cname
+ vee, x, e :: vname
+
+translations
+
+ "Base" == "cnam_ Base_"
+ "Ext" == "cnam_ Ext_"
+ "vee" == "VName (vnam_ vee_)"
+ "x" == "VName (vnam_ x_)"
+ "e" == "VName (vnam_ e_)"
+
+rules
+ Base_not_Object "Base \\<noteq> Object"
+ Ext_not_Object "Ext \\<noteq> Object"
+
+consts
+
+ foo_Base :: java_mb
+ foo_Ext :: java_mb
+ BaseC, ExtC :: java_mb cdecl
+ test :: stmt
+ foo :: mname
+ a,b :: loc
+
+defs
+
+ foo_Base_def "foo_Base \\<equiv> ([x],[],Skip,LAcc x)"
+ BaseC_def "BaseC \\<equiv> (Base, (Some Object,
+ [(vee, PrimT Boolean)],
+ [((foo,[Class Base]),Class Base,foo_Base)]))"
+ foo_Ext_def "foo_Ext \\<equiv> ([x],[],Expr( {Ext}Cast (ClassT Ext)
+ (LAcc x)..vee:=Lit (Intg #1)),
+ Lit Null)"
+ ExtC_def "ExtC \\<equiv> (Ext, (Some Base ,
+ [(vee, PrimT Integer)],
+ [((foo,[Class Base]),Class Ext,foo_Ext)]))"
+
+ test_def "test \\<equiv> Expr(e\\<Colon>=NewC Ext);;
+ Expr(LAcc e..foo({[Class Base]}[Lit Null]))"
+
+
+
+
+
+
+
+
+syntax
+
+ NP :: xcpt
+ tprg :: java_mb prog
+ obj1, obj2 :: obj
+ s0,s1,s2,s3,s4:: state
+
+translations
+
+ "NP" == "NullPointer"
+ "tprg" == "[ObjectC, BaseC, ExtC]"
+ "obj1" <= "(Ext, empty((vee, Base)\\<mapsto>Bool False)
+ ((vee, Ext )\\<mapsto>Intg #0))"
+ "s0" == " Norm (empty ,empty )"
+ "s1" == " Norm (empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a) )"
+ "s2" == " Norm (empty(a\\<mapsto>obj1),empty(x\\<mapsto>Null)(This\\<mapsto>Addr a))"
+ "s3" == "(Some NP, empty(a\\<mapsto>obj1),empty(x\\<mapsto>Null)(This\\<mapsto>Addr a))"
+end