equal
deleted
inserted
replaced
1 (* Title: HOL/NanoJava/State.thy |
1 (* Title: HOL/NanoJava/State.thy |
2 ID: $Id$ |
|
3 Author: David von Oheimb |
2 Author: David von Oheimb |
4 Copyright 2001 Technische Universitaet Muenchen |
3 Copyright 2001 Technische Universitaet Muenchen |
5 *) |
4 *) |
6 |
5 |
7 header "Program State" |
6 header "Program State" |
18 |
17 |
19 datatype val |
18 datatype val |
20 = Null --{* null reference *} |
19 = Null --{* null reference *} |
21 | Addr loc --{* address, i.e. location of object *} |
20 | Addr loc --{* address, i.e. location of object *} |
22 |
21 |
23 types fields |
22 types fields |
24 = "(fname \<rightharpoonup> val)" |
23 = "(fname \<rightharpoonup> val)" |
25 |
24 |
26 obj = "cname \<times> fields" |
25 obj = "cname \<times> fields" |
27 |
26 |
28 translations |
27 translations |
29 |
28 |
34 |
33 |
35 init_vars:: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)" |
34 init_vars:: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)" |
36 "init_vars m == Option.map (\<lambda>T. Null) o m" |
35 "init_vars m == Option.map (\<lambda>T. Null) o m" |
37 |
36 |
38 text {* private: *} |
37 text {* private: *} |
39 types heap = "loc \<rightharpoonup> obj" |
38 types heap = "loc \<rightharpoonup> obj" |
40 locals = "vname \<rightharpoonup> val" |
39 locals = "vname \<rightharpoonup> val" |
41 |
40 |
42 text {* private: *} |
41 text {* private: *} |
43 record state |
42 record state |
44 = heap :: heap |
43 = heap :: heap |
45 locals :: locals |
44 locals :: locals |
46 |
45 |
47 translations |
46 translations |
48 |
47 |
49 "heap" \<leftharpoondown> (type)"loc => obj option" |
48 "heap" \<leftharpoondown> (type)"loc => obj option" |
95 "new_obj a C \<equiv> hupd(a\<mapsto>(C,init_vars (field C)))" |
94 "new_obj a C \<equiv> hupd(a\<mapsto>(C,init_vars (field C)))" |
96 |
95 |
97 upd_obj :: "loc => fname => val => state => state" |
96 upd_obj :: "loc => fname => val => state => state" |
98 "upd_obj a f v s \<equiv> let (C,fs) = the (heap s a) in hupd(a\<mapsto>(C,fs(f\<mapsto>v))) s" |
97 "upd_obj a f v s \<equiv> let (C,fs) = the (heap s a) in hupd(a\<mapsto>(C,fs(f\<mapsto>v))) s" |
99 |
98 |
100 new_Addr :: "state => val" |
99 new_Addr :: "state => val" |
101 "new_Addr s == SOME v. (\<exists>a. v = Addr a \<and> (heap s) a = None) | v = Null" |
100 "new_Addr s == SOME v. (\<exists>a. v = Addr a \<and> (heap s) a = None) | v = Null" |
102 |
101 |
103 |
102 |
104 subsection "Properties not used in the meta theory" |
103 subsection "Properties not used in the meta theory" |
105 |
104 |