author | wenzelm |
Mon, 15 Nov 2010 17:40:38 +0100 | |
changeset 40547 | 05a82b4bccbc |
parent 35102 | cc7a0b9f938c |
child 44035 | 322d1657c40c |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/Type.thy |
2 |
Author: David von Oheimb |
|
3 |
Copyright 1999 Technische Universitaet Muenchen |
|
11070 | 4 |
*) |
8011 | 5 |
|
12911 | 6 |
header {* \isaheader{Java types} *} |
8011 | 7 |
|
16417 | 8 |
theory Type imports JBasis begin |
8011 | 9 |
|
12517 | 10 |
typedecl cnam |
11 |
||
12 |
-- "exceptions" |
|
13 |
datatype |
|
14 |
xcpt |
|
15 |
= NullPointer |
|
16 |
| ClassCast |
|
17 |
| OutOfMemory |
|
8011 | 18 |
|
12517 | 19 |
-- "class names" |
20 |
datatype cname |
|
21 |
= Object |
|
22 |
| Xcpt xcpt |
|
12951 | 23 |
| Cname cnam |
12517 | 24 |
|
25 |
typedecl vnam -- "variable or field name" |
|
26 |
typedecl mname -- "method name" |
|
27 |
||
28 |
-- "names for @{text This} pointer and local/field variables" |
|
29 |
datatype vname |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
30 |
= This |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
31 |
| VName vnam |
8011 | 32 |
|
12517 | 33 |
-- "primitive type, cf. 4.2" |
34 |
datatype prim_ty |
|
35 |
= Void -- "'result type' of void methods" |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
36 |
| Boolean |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
37 |
| Integer |
8011 | 38 |
|
12517 | 39 |
-- "reference type, cf. 4.3" |
40 |
datatype ref_ty |
|
41 |
= NullT -- "null type, cf. 4.1" |
|
42 |
| ClassT cname -- "class type" |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
43 |
|
12517 | 44 |
-- "any type, cf. 4.1" |
45 |
datatype ty |
|
46 |
= PrimT prim_ty -- "primitive type" |
|
47 |
| RefT ref_ty -- "reference type" |
|
8011 | 48 |
|
35102 | 49 |
abbreviation NT :: ty |
50 |
where "NT == RefT NullT" |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
51 |
|
35102 | 52 |
abbreviation Class :: "cname => ty" |
53 |
where "Class C == RefT (ClassT C)" |
|
8011 | 54 |
|
55 |
end |