pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-12-01 00:26:18 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Typo fix

Browse source
This commit is contained in:
Adam Chlipala 2020-04-14 11:55:26 -04:00
parent b632c66f85
commit 2efec7b61d
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
frap_book.tex
View file

@ -4168,7 +4168,7 @@ This result can be composed with soundness of any Hoare logic for the source lan
The associated Coq code defines one, essentially following our separation logic\index{separation logic} from last chapter.
\begin{theorem}
If $\hoare{P}{c}{Q}$, $P(h)$, $\dscomp{v}{c}{s}$, and $\texttt{result} \notin \dom{v}$, then it is invariant of the transition system starting in $(h, v, s)$ that execution never gets stuck.
If $\hoare{P}{c}{Q}$, $P(h)$, $\dscomp{v}{c}{s}$, and $\texttt{result} \notin \dom{v}$, then it is an invariant of the transition system starting in $(h, v, s)$ that execution never gets stuck.
\end{theorem}
\begin{proof}
First, we switch to proving an invariant of the system $(h, c)$ using the simulation from Theorem \ref{dscompsim}.