author | oheimb |
Fri, 14 Jul 2000 16:32:51 +0200 | |
changeset 9346 | 297dcbf64526 |
child 9348 | f495dba0cb07 |
permissions | -rw-r--r-- |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
1 |
(* Title: isabelle/Bali/Example.thy |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
2 |
ID: $Id$ |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
3 |
Author: David von Oheimb |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
4 |
Copyright 1997 Technische Universitaet Muenchen |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
5 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
6 |
The following example Bali program includes: |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
7 |
class declarations with inheritance, hiding of fields, and overriding of |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
8 |
methods (with refined result type), |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
9 |
instance creation, local assignment, sequential composition, |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
10 |
method call with dynamic binding, literal values, |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
11 |
expression statement, local access, type cast, field assignment (in part), skip |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
12 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
13 |
class Base { |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
14 |
boolean vee; |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
15 |
Base foo(Base x) {return x;} |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
16 |
} |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
17 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
18 |
class Ext extends Base{ |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
19 |
int vee; |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
20 |
Ext foo(Base x) {((Ext)x).vee=1; return null;} |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
21 |
} |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
22 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
23 |
class Example { |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
24 |
public static void main (String args[]) { |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
25 |
Base e; |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
26 |
e=new Ext(); |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
27 |
try {e.foo(null); } |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
28 |
catch (NullPointerException x) {} |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
29 |
} |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
30 |
} |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
31 |
*) |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
32 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
33 |
Example = Eval + |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
34 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
35 |
datatype cnam_ = Base_ | Ext_ |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
36 |
datatype vnam_ = vee_ | x_ | e_ |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
37 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
38 |
consts |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
39 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
40 |
cnam_ :: "cnam_ \\<Rightarrow> cname" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
41 |
vnam_ :: "vnam_ \\<Rightarrow> vnam" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
42 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
43 |
rules (* cnam_ and vnam_ are intended to be isomorphic to cnam and vnam *) |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
44 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
45 |
inj_cnam_ "(cnam_ x = cnam_ y) = (x = y)" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
46 |
inj_vnam_ "(vnam_ x = vnam_ y) = (x = y)" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
47 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
48 |
surj_cnam_ "\\<exists>m. n = cnam_ m" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
49 |
surj_vnam_ "\\<exists>m. n = vnam_ m" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
50 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
51 |
syntax |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
52 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
53 |
Base, Ext :: cname |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
54 |
vee, x, e :: vname |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
55 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
56 |
translations |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
57 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
58 |
"Base" == "cnam_ Base_" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
59 |
"Ext" == "cnam_ Ext_" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
60 |
"vee" == "VName (vnam_ vee_)" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
61 |
"x" == "VName (vnam_ x_)" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
62 |
"e" == "VName (vnam_ e_)" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
63 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
64 |
rules |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
65 |
Base_not_Object "Base \\<noteq> Object" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
66 |
Ext_not_Object "Ext \\<noteq> Object" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
67 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
68 |
consts |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
69 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
70 |
foo_Base :: java_mb |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
71 |
foo_Ext :: java_mb |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
72 |
BaseC, ExtC :: java_mb cdecl |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
73 |
test :: stmt |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
74 |
foo :: mname |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
75 |
a,b :: loc |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
76 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
77 |
defs |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
78 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
79 |
foo_Base_def "foo_Base \\<equiv> ([x],[],Skip,LAcc x)" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
80 |
BaseC_def "BaseC \\<equiv> (Base, (Some Object, |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
81 |
[(vee, PrimT Boolean)], |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
82 |
[((foo,[Class Base]),Class Base,foo_Base)]))" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
83 |
foo_Ext_def "foo_Ext \\<equiv> ([x],[],Expr( {Ext}Cast (ClassT Ext) |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
84 |
(LAcc x)..vee:=Lit (Intg #1)), |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
85 |
Lit Null)" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
86 |
ExtC_def "ExtC \\<equiv> (Ext, (Some Base , |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
87 |
[(vee, PrimT Integer)], |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
88 |
[((foo,[Class Base]),Class Ext,foo_Ext)]))" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
89 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
90 |
test_def "test \\<equiv> Expr(e\\<Colon>=NewC Ext);; |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
91 |
Expr(LAcc e..foo({[Class Base]}[Lit Null]))" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
92 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
93 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
94 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
95 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
96 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
97 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
98 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
99 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
100 |
syntax |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
101 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
102 |
NP :: xcpt |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
103 |
tprg :: java_mb prog |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
104 |
obj1, obj2 :: obj |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
105 |
s0,s1,s2,s3,s4:: state |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
106 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
107 |
translations |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
108 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
109 |
"NP" == "NullPointer" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
110 |
"tprg" == "[ObjectC, BaseC, ExtC]" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
111 |
"obj1" <= "(Ext, empty((vee, Base)\\<mapsto>Bool False) |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
112 |
((vee, Ext )\\<mapsto>Intg #0))" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
113 |
"s0" == " Norm (empty ,empty )" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
114 |
"s1" == " Norm (empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a) )" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
115 |
"s2" == " Norm (empty(a\\<mapsto>obj1),empty(x\\<mapsto>Null)(This\\<mapsto>Addr a))" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
116 |
"s3" == "(Some NP, empty(a\\<mapsto>obj1),empty(x\\<mapsto>Null)(This\\<mapsto>Addr a))" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
117 |
end |