aspec: mapsto syntax update for Isabelle2023
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
parent
286278d9e8
commit
450234e062
|
@ -77,8 +77,8 @@ definition
|
|||
tcb_bound_notification = None,
|
||||
tcb_mcpriority = minBound,
|
||||
tcb_arch = init_arch_tcb
|
||||
\<rparr>)
|
||||
(us_global_pd_ptr \<mapsto> us_global_pd)"
|
||||
\<rparr>,
|
||||
us_global_pd_ptr \<mapsto> us_global_pd)"
|
||||
|
||||
definition
|
||||
"init_cdt \<equiv> Map.empty"
|
||||
|
|
|
@ -244,7 +244,7 @@ definition set_eobject :: "obj_ref \<Rightarrow> etcb \<Rightarrow> unit det_ext
|
|||
where
|
||||
"set_eobject ptr obj \<equiv>
|
||||
do es \<leftarrow> get;
|
||||
ekh \<leftarrow> return $ ekheap es(ptr \<mapsto> obj);
|
||||
ekh \<leftarrow> return $ (ekheap es)(ptr \<mapsto> obj);
|
||||
put (es\<lparr>ekheap := ekh\<rparr>)
|
||||
od"
|
||||
|
||||
|
|
|
@ -35,7 +35,7 @@ where
|
|||
kobj <- get_object ptr;
|
||||
assert (a_type kobj = a_type obj);
|
||||
s \<leftarrow> get;
|
||||
put (s\<lparr>kheap := kheap s(ptr \<mapsto> obj)\<rparr>)
|
||||
put (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>)
|
||||
od"
|
||||
|
||||
|
||||
|
|
Loading…
Reference in New Issue