author | oheimb |
Wed, 06 Dec 2000 19:10:36 +0100 | |
changeset 10613 | 78b1d6c3ee9c |
parent 10229 | 10e2d29a77de |
child 10763 | 08e1610c1dcb |
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 |
|
10229 | 18 |
class Ext extends Base { |
9346
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[]) { |
9498 | 25 |
Base e=new Ext(); |
26 |
e.foo(null); |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
27 |
} |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
28 |
} |
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 |
Example = Eval + |
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 |
datatype cnam_ = Base_ | Ext_ |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
34 |
datatype vnam_ = vee_ | x_ | e_ |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
35 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
36 |
consts |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
37 |
|
10042 | 38 |
cnam_ :: "cnam_ => cname" |
39 |
vnam_ :: "vnam_ => vnam" |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
40 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
41 |
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
|
42 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
43 |
inj_cnam_ "(cnam_ x = cnam_ y) = (x = y)" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
44 |
inj_vnam_ "(vnam_ x = vnam_ y) = (x = y)" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
45 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
46 |
surj_cnam_ "\\<exists>m. n = cnam_ m" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
47 |
surj_vnam_ "\\<exists>m. n = vnam_ m" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
48 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
49 |
syntax |
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 |
Base, Ext :: cname |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
52 |
vee, x, e :: vname |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
53 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
54 |
translations |
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 |
"Base" == "cnam_ Base_" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
57 |
"Ext" == "cnam_ Ext_" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
58 |
"vee" == "VName (vnam_ vee_)" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
59 |
"x" == "VName (vnam_ x_)" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
60 |
"e" == "VName (vnam_ e_)" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
61 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
62 |
rules |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
63 |
Base_not_Object "Base \\<noteq> Object" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
64 |
Ext_not_Object "Ext \\<noteq> Object" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
65 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
66 |
consts |
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 |
foo_Base :: java_mb |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
69 |
foo_Ext :: java_mb |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
70 |
BaseC, ExtC :: java_mb cdecl |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
71 |
test :: stmt |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
72 |
foo :: mname |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
73 |
a,b :: loc |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
74 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
75 |
defs |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
76 |
|
10042 | 77 |
foo_Base_def "foo_Base == ([x],[],Skip,LAcc x)" |
10613
78b1d6c3ee9c
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10229
diff
changeset
|
78 |
BaseC_def "BaseC == (Base, (Object, |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
79 |
[(vee, PrimT Boolean)], |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
80 |
[((foo,[Class Base]),Class Base,foo_Base)]))" |
10042 | 81 |
foo_Ext_def "foo_Ext == ([x],[],Expr( {Ext}Cast Ext |
9348 | 82 |
(LAcc x)..vee:=Lit (Intg #1)), |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
83 |
Lit Null)" |
10613
78b1d6c3ee9c
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10229
diff
changeset
|
84 |
ExtC_def "ExtC == (Ext, (Base , |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
85 |
[(vee, PrimT Integer)], |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
86 |
[((foo,[Class Base]),Class Ext,foo_Ext)]))" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
87 |
|
10042 | 88 |
test_def "test == Expr(e::=NewC Ext);; |
9793 | 89 |
Expr(LAcc e..foo({[Class Base]}[Lit Null]))" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
90 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
91 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
92 |
syntax |
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 |
NP :: xcpt |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
95 |
tprg :: java_mb prog |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
96 |
obj1, obj2 :: obj |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
97 |
s0,s1,s2,s3,s4:: state |
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 |
translations |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
100 |
|
9498 | 101 |
"NP" == "NullPointer" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
102 |
"tprg" == "[ObjectC, BaseC, ExtC]" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
103 |
"obj1" <= "(Ext, empty((vee, Base)\\<mapsto>Bool False) |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
104 |
((vee, Ext )\\<mapsto>Intg #0))" |
9793 | 105 |
"s0" == " Norm (empty, empty)" |
106 |
"s1" == " Norm (empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a))" |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
107 |
"s2" == " Norm (empty(a\\<mapsto>obj1),empty(x\\<mapsto>Null)(This\\<mapsto>Addr a))" |
9348 | 108 |
"s3" == "(Some NP, empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a))" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
109 |
end |