From e50928a2c1567b3dd633794f96c6a387da3fc03e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 6 Dec 2016 19:05:29 +0100
Subject: [PATCH] document the sugar for 'idempotent' accessors
---
docs/iris.sty | 2 ++
docs/program-logic.tex | 4 ++++
2 files changed, 6 insertions(+)
diff --git a/docs/iris.sty b/docs/iris.sty
index 51d4ebae4..136cc677a 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -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
\newcommand*{\hoaresizebox}[1]{%
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 1d33f1f1a..997215f1b 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -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"
--
GitLab