author | oheimb |
Tue, 02 Jan 2001 22:41:17 +0100 | |
changeset 10763 | 08e1610c1dcb |
parent 10061 | fe82134773dc |
child 11026 | a50365d21144 |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/State.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
5 |
||
6 |
State for evaluation of Java expressions and statements |
|
7 |
*) |
|
8 |
||
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
9240
diff
changeset
|
9 |
State = TypeRel + Value + |
8011 | 10 |
|
11 |
types fields_ |
|
12 |
= "(vname \\<times> cname \\<leadsto> val)" (* field name, defining class, value *) |
|
13 |
||
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
9240
diff
changeset
|
14 |
obj = "cname \\<times> fields_" (* class instance with class name and fields *) |
8011 | 15 |
|
16 |
constdefs |
|
10042 | 17 |
obj_ty :: "obj => ty" |
18 |
"obj_ty obj == Class (fst obj)" |
|
8011 | 19 |
|
10042 | 20 |
init_vars :: "('a \\<times> ty) list => ('a \\<leadsto> val)" |
21 |
"init_vars == map_of o map (\\<lambda>(n,T). (n,default_val T))" |
|
8011 | 22 |
|
23 |
datatype xcpt (* exceptions *) |
|
24 |
= NullPointer |
|
25 |
| ClassCast |
|
26 |
| OutOfMemory |
|
27 |
||
28 |
types aheap = "loc \\<leadsto> obj" (* "heap" used in a translation below *) |
|
29 |
locals = "vname \\<leadsto> val" |
|
30 |
||
31 |
state (* simple state, i.e. variable contents *) |
|
32 |
= "aheap \\<times> locals" |
|
33 |
(* heap, local parameter including This *) |
|
34 |
||
35 |
xstate (* state including exception information *) |
|
36 |
= "xcpt option \\<times> state" |
|
37 |
||
38 |
syntax |
|
10042 | 39 |
heap :: "state => aheap" |
40 |
locals :: "state => locals" |
|
41 |
Norm :: "state => xstate" |
|
8011 | 42 |
|
43 |
translations |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
44 |
"heap" => "fst" |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
45 |
"locals" => "snd" |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
46 |
"Norm s" == "(None,s)" |
8011 | 47 |
|
48 |
constdefs |
|
49 |
||
10042 | 50 |
new_Addr :: "aheap => loc \\<times> xcpt option" |
51 |
"new_Addr h == SOME (a,x). (h a = None \\<and> x = None) | x = Some OutOfMemory" |
|
8011 | 52 |
|
10042 | 53 |
raise_if :: "bool => xcpt => xcpt option => xcpt option" |
54 |
"raise_if c x xo == if c \\<and> (xo = None) then Some x else xo" |
|
8011 | 55 |
|
10042 | 56 |
np :: "val => xcpt option => xcpt option" |
57 |
"np v == raise_if (v = Null) NullPointer" |
|
8011 | 58 |
|
10042 | 59 |
c_hupd :: "aheap => xstate => xstate" |
60 |
"c_hupd h'== \\<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))" |
|
8011 | 61 |
|
10042 | 62 |
cast_ok :: "'c prog => cname => aheap => val => bool" |
63 |
"cast_ok G C h v == v = Null \\<or> G\\<turnstile>obj_ty (the (h (the_Addr v)))\\<preceq> Class C" |
|
8011 | 64 |
|
65 |
end |