Commit e50928a2 authored by Ralf Jung's avatar Ralf Jung

document the sugar for 'idempotent' accessors

parent 6c06af44
......@@ -287,6 +287,8 @@
% for now, the update modality looks like a pvs without masks.
\NewDocumentCommand \upd {} {\mathop{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}
\NewDocumentCommand\Acc{O{} O{} m m}{\langle #3 \vsE #4 \rangle_{#1}^{#2}}
%% Hoare Triples
......@@ -513,6 +513,10 @@ For this reason, we also call such accessors \emph{non-atomic}.
The reasons accessors are useful is that they let us talk about ``opening X'' (\eg ``opening invariants'') without having to care what X is opened around.
Furthermore, as we construct more sophisticated and more interesting things that can be opened (\eg invariants that can be ``cancelled'', or STSs), accessors become a useful interface that allows us to mix and match different abstractions in arbitrary ways.
For the special case that $\prop = \propC$ and $\propB = \propB'$, we use the following notation that avoids repetition:
\[ \Acc[\mask_1][\mask_2]\prop{\Ret x. \propB} \eqdef \prop \vs[\mask_1][\mask_2] \Exists\var. \propB * (\propB \vsW[\mask_2][\mask_1] \prop) \]
This accessor is ``idempotent'' in the sense that it doesn't actually change the state. After applying it, we get our $\prop$ back so we end up where we started.
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "iris"
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment