pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

ConcurrentSeparationLogic chapter: proofreading

Browse source
This commit is contained in:
Adam Chlipala 2016-04-29 17:37:17 -04:00
parent 2f1d28a36a
commit 8c67fc5468
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
frap_book.tex
View file

@ -3983,7 +3983,7 @@ Two lemmas express crucial techniques to isolate elements within iterated conjun
\end{proof}
\begin{lemma}\label{cslinvariant}
If $\hoare{P}{c}{Q}$, and if a heap $h$ satisfies the predicate $(P * \bigstar{\ell}{L}{\mathcal I(\ell)})$, then an invariant of the system starting at state $(h, \emptyset, c)$ is: for reachable state $(h', l', c')$, there exists $P'$ where $\hoare{P'}{c'}{Q}$, such that $h'$ satisfies $(P' * \bigstar{\ell}{L}{\guarded{\ell \notin L}{\mathcal I(\ell)}})$.
If $\hoare{P}{c}{Q}$, and if a heap $h$ satisfies the predicate $(P * \bigstar{\ell}{L}{\mathcal I(\ell)})$, then an invariant of the system starting at state $(h, \emptyset, c)$ is: for reachable state $(h', l', c')$, there exists $P'$ where $\hoare{P'}{c'}{Q}$, such that $h'$ satisfies $(P' * \bigstarp{\ell}{L}{\guarded{\ell \notin l'}{\mathcal I(\ell)}})$.
\end{lemma}
\begin{proof}
By invariant induction\index{invariant induction}, using Lemma \ref{nonelocked} for the base case and Lemma \ref{cslpreservation} for the induction step, the latter with $R = \emp$.
@ -3996,7 +3996,7 @@ Two lemmas express crucial techniques to isolate elements within iterated conjun
By induction on the derivation of $\hoare{P}{c}{Q}$.
\end{proof}
The overall soundness proof proceeds by invariant weakening\index{invariant weakening} to the invariant established by Lemma \ref{cslinvariant}.
The overall soundness proof proceeds by invariant weakening\index{invariant weakening} with the invariant established by Lemma \ref{cslinvariant}.
We prove the inclusion of new invariant in old by Lemma \ref{cslprogress}.