@@ -465,7 +465,6 @@ For this reason, we also call such accessors \emph{non-atomic}.
...
@@ -465,7 +465,6 @@ 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.
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.
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.
\ralf{This would be much more convincing if we had forward references here to sections describing canellable invariants and STSs.}