You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Greater use of heap projections in invariants and in state_relation may ease some reasoning in Refine.
For example, pspace_relation, the greatest component of state_relation, could make far greater use of heap projections, in a way similar to what is done in cstate_relation in CRefine. For example, we could write pspace_relation as a conjunction over the various kernel object types, each saying, for example, that given an abstract heap of TCBs (with tcbs_of) and a concrete heap of TCBs (with tcbs_of'), that their domains are equal, and that at the points in the domain, tcb_relation holds between the abstract and concrete TCBs.
The text was updated successfully, but these errors were encountered:
Greater use of heap projections in invariants and in
state_relation
may ease some reasoning in Refine.For example,
pspace_relation
, the greatest component ofstate_relation
, could make far greater use of heap projections, in a way similar to what is done incstate_relation
in CRefine. For example, we could writepspace_relation
as a conjunction over the various kernel object types, each saying, for example, that given an abstract heap of TCBs (withtcbs_of
) and a concrete heap of TCBs (withtcbs_of'
), that their domains are equal, and that at the points in the domain,tcb_relation
holds between the abstract and concrete TCBs.The text was updated successfully, but these errors were encountered: