@@ -367,7 +367,7 @@ The adequacy statement now reads as follows:

Notice that the state invariant $S$ used by the weakest precondition is chosen \emph{after} doing a fancy update, which allows it to depend on the names of ghost variables that are picked in that initial fancy update.

\paragraph{Hoare triples.}

It turns out that weakest precondition is actually quite convenient to work with, in particular when perfoming these proofs in Coq.

It turns out that weakest precondition is actually quite convenient to work with, in particular when performing these proofs in Coq.

Still, for a more traditional presentation, we can easily derive the notion of a Hoare triple: