author | kleing |
Thu, 21 Sep 2000 10:42:49 +0200 | |
changeset 10042 | 7164dc0d24d8 |
parent 9348 | f495dba0cb07 |
child 10061 | fe82134773dc |
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 |
|
17 |
||
10042 | 18 |
obj_ty :: "obj => ty" |
19 |
"obj_ty obj == Class (fst obj)" |
|
8011 | 20 |
|
10042 | 21 |
init_vars :: "('a \\<times> ty) list => ('a \\<leadsto> val)" |
22 |
"init_vars == map_of o map (\\<lambda>(n,T). (n,default_val T))" |
|
8011 | 23 |
|
24 |
datatype xcpt (* exceptions *) |
|
25 |
= NullPointer |
|
26 |
| ClassCast |
|
27 |
| OutOfMemory |
|
28 |
||
29 |
types aheap = "loc \\<leadsto> obj" (* "heap" used in a translation below *) |
|
30 |
locals = "vname \\<leadsto> val" |
|
31 |
||
32 |
state (* simple state, i.e. variable contents *) |
|
33 |
= "aheap \\<times> locals" |
|
34 |
(* heap, local parameter including This *) |
|
35 |
||
36 |
xstate (* state including exception information *) |
|
37 |
= "xcpt option \\<times> state" |
|
38 |
||
39 |
syntax |
|
10042 | 40 |
heap :: "state => aheap" |
41 |
locals :: "state => locals" |
|
42 |
Norm :: "state => xstate" |
|
8011 | 43 |
|
44 |
translations |
|
45 |
"heap" => "fst" |
|
46 |
"locals" => "snd" |
|
47 |
"Norm s" == "(None,s)" |
|
48 |
||
49 |
constdefs |
|
50 |
||
10042 | 51 |
new_Addr :: "aheap => loc \\<times> xcpt option" |
52 |
"new_Addr h == SOME (a,x). (h a = None \\<and> x = None) | x = Some OutOfMemory" |
|
8011 | 53 |
|
10042 | 54 |
raise_if :: "bool => xcpt => xcpt option => xcpt option" |
55 |
"raise_if c x xo == if c \\<and> (xo = None) then Some x else xo" |
|
8011 | 56 |
|
10042 | 57 |
np :: "val => xcpt option => xcpt option" |
58 |
"np v == raise_if (v = Null) NullPointer" |
|
8011 | 59 |
|
10042 | 60 |
c_hupd :: "aheap => xstate => xstate" |
61 |
"c_hupd h'== \\<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))" |
|
8011 | 62 |
|
10042 | 63 |
cast_ok :: "'c prog => cname => aheap => val => bool" |
64 |
"cast_ok G C h v == v = Null \\<or> G\\<turnstile>obj_ty (the (h (the_Addr v)))\\<preceq> Class C" |
|
8011 | 65 |
|
66 |
end |