equal
deleted
inserted
replaced
8 |
8 |
9 theory State = TypeRel: |
9 theory State = TypeRel: |
10 |
10 |
11 constdefs |
11 constdefs |
12 |
12 |
13 body :: "cname => mname => stmt" |
13 body :: "imname => stmt" |
14 "body C m \<equiv> bdy (the (method C m))" |
14 "body \<equiv> \<lambda>(C,m). bdy (the (method C m))" |
15 |
15 |
16 text {* locations, i.e.\ abstract references to objects *} |
16 text {* locations, i.e.\ abstract references to objects *} |
17 typedecl loc |
17 typedecl loc |
18 arities loc :: "term" |
18 arities loc :: "term" |
19 |
19 |
51 "locals" \<leftharpoondown> (type)"vname => val option" |
51 "locals" \<leftharpoondown> (type)"vname => val option" |
52 "state" \<leftharpoondown> (type)"(|heap :: heap, locals :: locals|)" |
52 "state" \<leftharpoondown> (type)"(|heap :: heap, locals :: locals|)" |
53 |
53 |
54 constdefs |
54 constdefs |
55 |
55 |
|
56 reset_locs :: "state => state" |
|
57 "reset_locs s \<equiv> s (| locals := empty |)" |
|
58 |
56 init_locs :: "cname => mname => state => state" |
59 init_locs :: "cname => mname => state => state" |
57 "init_locs C m s \<equiv> s (| locals:=init_vars (map_of (lcl (the (method C m))))|)" |
60 "init_locs C m s \<equiv> s (| locals:=init_vars (map_of (lcl (the (method C m)))) |)" |
58 |
61 |
59 text {* The first parameter of @{term set_locs} is of type @{typ state} |
62 text {* The first parameter of @{term set_locs} is of type @{typ state} |
60 rather than @{typ locals} in order to keep @{typ locals} private.*} |
63 rather than @{typ locals} in order to keep @{typ locals} private.*} |
61 constdefs |
64 constdefs |
62 set_locs :: "state => state => state" |
65 set_locs :: "state => state => state" |