Commit 7b1297e6 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Proof : simple changes.

parent 7e715113
......@@ -272,7 +272,7 @@ we get the following:
\monoWitness{\offset}{\pair\status\sview}
\isep \ownGhost\gmonos{\mapsingleton \offset {\authfull \pair{\status'}{\sview'}}}
}{%
\status \leq \status' \land (\status = \status' \implies \sview \viewgeq \sview')
\status \leq \status' \land (\status = \status'\implies \sview \viewgeq \sview')
}
%
\end{mathpar}
......@@ -385,7 +385,7 @@ $\eview \viewleq \sview$.
% …
There are more properties that are invariant of the code, and thus can be added
There are more properties that are invariant of the code, and thus could be added
to the list and verified as well, however they are not needed in order to carry
the proof of the specification: for example, that \reftail and \refhead are
strictly monotonic, or that statuses are non-negative.
the proof of the specification: for example, \reftail and \refhead are
strictly monotonic, and statuses are non-negative.
Supports Markdown
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