Skip to main content
Logo image

An Introduction to Imperative Programming

Sebastian Hack

Section 7.4 Verification

In this section, we discuss Hoare logic, a verification technique to statically verify that a program is correct with respect to a given specification.
We have already discussed Hoare triples as a notation to say that a program is partially/totally correct. We will now extend this notation to a logic, i.e. a set of rules on the abstract syntax of C0 programs with which we can derive statements (Hoare triples) about them. The overall idea is to define appropriate rules to derive Hoare triples for each syntactical element of C0. These rules can then be used to derive Hoare triples for entire programs.
We proceed as follows: We first define rules for Hoare triples for the statement/program language of C0 and see how we can use them to prove programs correct manually. Then, we look into how we can use these rules in a mechanized setting, i.e. how we can create an automatic verifier, a computer program that uses these rules to automatically prove programs correct.
To keep it simple, we focus on the initial definition of the C0 language in Section 6.2 and disregard pointers and blocks with local variables here.

Subsection 7.4.1 Hoare Logic

Before we start, we need to make an important distinction. In Definition 7.1.7 and Definition 7.1.6 we have defined Hoare triples semantically which means that we used properties of the program execution of a C0 program (more specifically its termination behavior) to define what a Hoare triple is. In this section, we are interested in defining a logic which means that we define a set of rules over the syntax of a language (here C0) to derive facts (here Hoare triples) about a term in that language (here a C0 program). To make the difference clear, we write
\begin{equation*} \models\hoare PpQ \end{equation*}
when we mean that program \(p\) is in fact totally/partially correct with respect to the specification \((P,Q)\text{.}\) This is the notion of a Hoare triple that we have introduced in Definition 7.1.7 and Definition 7.1.6. We write
\begin{equation*} \vdash\hoare PpQ \end{equation*}
when we mean that we derived the Hoare triple with the proof rules we develop in this section. Of course, the proof rules we define are only useful if they are sound which means that the Hoare triples we can derive with them are semantically true which formally means that \(\vdash\hoare PpQ\) entails \(\models\hoare PpQ\text{.}\) The rules we define in this section are sound but we do not prove it here because it requires a slightly more involved technical setup that is beyond the scope of this text.
In the following, we define Hoare triples first for the statements of C0 and then define how they can be lifted to Hoare triples of programs.

Weakening and Strengthening.

An assertion \(B\) is stronger than an assertion \(C\) if \(B\limp C\text{.}\) Correspondingly, \(C\) is weaker than \(B\text{.}\) Based on the definition of satisfiability (Definition 7.1.4), a weaker assertion is satisfied by more states. For example
\begin{align*} x>10\amp\text{ is stronger than }x>3\\ x=10\land y=5\amp\text{ is stronger than }y=5 \end{align*}
In a Hoare triple we can strengthen preconditions and weaken postconditions. Intuitively, this is true because of the following observation: If \(P'\simp P\text{,}\) each state satisfying \(P'\) also satisfies \(P\text{,}\) so if \(\vdash\hoare PsQ\text{,}\) we also have \(\vdash\hoare {P'}sQ\text{.}\) Similarly, if \(Q\simp Q'\text{,}\) each state that satisfies \(Q\) also satisfies \(Q'\text{.}\) Hence, if we have \(\vdash\hoare PsQ\text{,}\) we then also have \(\vdash\hoare Ps{Q'}\text{.}\) This is reflected in the following rule which is often called rule of consequence:
\begin{equation*} \begin{prooftree} \AxiomC{$P'\limp P$} \AxiomC{$\vdash\hoare PsQ$} \AxiomC{$Q\limp Q'$} \LeftLabel{[Consequence]} \TrinaryInfC{$\vdash\hoare {P'}s{Q'}$} \end{prooftree} \end{equation*}

Abort.

Aborting the program means that it doesn't properly terminate (refer to Remark 6.3.7 and Definition 7.1.7). Hence, in no state does the program \(\CAbort\) terminate in a state that would satisfy any postcondition. Therefore, for any postcondition \(Q\) the Hoare triple of \(\CAbort\) is
\begin{equation*} \begin{prooftree} \AxiomC{} \LeftLabel{[Abort]} \UnaryInfC{$\vdash\hoare {\lfalse}{\CAbort}{Q}$} \end{prooftree} \end{equation*}

Assignment.

Consider the assignment statement of C0 \(\CAssign xe\) and a post-condition \(Q\text{.}\) Now, let us consider what could be a valid pre-condition \(P\) that makes the Hoare triple \(\hoare P{\CAssign xe}Q\) true.
To this end, let us review the semantics of the assignment (see to Definition 6.3.4) in detail: First of all, the result of the R-evaluation of the expression \(e\) must be defined which is ensured by the predicate \(\exprdef\,e\text{.}\) Second, the effect of \(\CAssign xe\) is to evaluate \(e\) and assign its value to the variable \(x\text{:}\)
\begin{equation*} \config{\CAssign xe}{\sigma}\steprel\configt{\sigma'} \end{equation*}
So evaluating \(e\) on \(\sigma\) yields the same value as evaluating \(x\) on \(\sigma'\text{.}\) Hence, if \(\sigma'\) satisfies \(Q\text{,}\) \(\sigma\) will satisfy the assertion \(Q[e/x]\) (read: \(e\) replaces \(x\) in \(Q\)). because \(e\) evaluates to the same value on \(\sigma\) as \(x\) does on \(\sigma'\text{.}\) That's just the purpose of the assignment. So the Hoare triple
\begin{equation*} \vdash\hoare{\exprdef\,e\land Q[e/x]}{\CAssign xe}{Q} \end{equation*}
is true and our proof system gets another axiom:
Definition 7.4.1. Hoare triple for the assignment statement.
\begin{equation*} \begin{prooftree} \AxiomC{} \LeftLabel{[Assign]} \UnaryInfC{$\vdash\hoare{\exprdef\,e\land Q[e/x]}{\CAssign xe}{Q}$} \end{prooftree} \end{equation*}
The \(\exprdef\,e\) part comes from the fact that in C0, the evaluation of expressions can get stuck, so the precondition needs to capture that because if the assignment gets stuck, it neither diverges nor terminates properly.
Let us check this on some examples:
Example 7.4.2.
\begin{equation*} \begin{prooftree} \AxiomC{} \UnaryInfC{$\vdash\hoare {2>0}{\CAssign{\CVar x}{\CConst 2}}{\CVar x>0}$} \end{prooftree} \quad \begin{prooftree} \AxiomC{} \UnaryInfC{$\vdash\hoare {\CBinary{*}{\CConst 2}{\CVar y}=\CVar y}{\CAssign{\CVar x}{\CBinary{*}{\CConst 2}{\CVar y}}}{\CVar x=\CVar y}$} \end{prooftree} \end{equation*}
\begin{equation*} \begin{prooftree} \AxiomC{} \UnaryInfC{$\vdash\hoare {\CBinary{+}{\CVar y}{\CConst 1}=\CConst 5}{\CAssign{\CVar x}{\CBinary{+}{\CVar y}{\CConst 1}}}{\CVar x=\CConst 5}$} \end{prooftree} \quad \begin{prooftree} \AxiomC{} \UnaryInfC{$\vdash\hoare {\CVar z\ne 0\land\CBinary{/}{\CVar y}{\CVar z}=\CConst 5}{\CAssign{\CVar x}{\CBinary{/}{\CVar y}{\CVar z}}}{\CVar x=\CConst 5}$} \end{prooftree} \end{equation*}

Block.

The Hoare triple for a block just falls back to the Hoare triple of its constituent program (rule [Block]). The empty program \(\CTerm\) does nothing so the Hoare triple \(\hoare Q\CTerm Q\) is valid. More interesting is the Hoare triple for the program that consists of a statement and a rest program.
In principle, the following rule says that if we can prove Hoare triples of the first statement and the remainder of the block in which the postcondition of the first statement is the precondition of the remainder, we can derive a Hoare triple of the entire block. Intuitively this is justified by the observation that the first Hoare triple yields that, if \(s_1\) terminates, it terminates in a state that fulfills the precondition of the remainder of the block which then, by its Hoare triple, will, (if it terminates) terminate in a state that fulfills \(Q\text{.}\)
Definition 7.4.3. Hoare triples for the block statement and programs.
\begin{equation*} \begin{prooftree} \AxiomC{$\vdash\hoare PsQ$} \AxiomC{$\vdash\hoare QpR$} \LeftLabel{[Seq]} \BinaryInfC{$\vdash\hoare P{\CSeq sp}R$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{} \LeftLabel{[Term]} \UnaryInfC{$\vdash\hoare Q{\CTerm}Q$} \end{prooftree} \end{equation*}
\begin{equation*} \begin{prooftree} \AxiomC{$\vdash\hoare PpQ$} \LeftLabel{[Block]} \UnaryInfC{$\vdash\hoare{P}{\CBlock{p}}{Q}$} \end{prooftree} \end{equation*}
Because sequences of statements (which form a program) are always terminated by \(\varepsilon\text{,}\) we define a convenience rule for a program that contains of two statements. This rule can be used to conveniently “process” the last two statements of a longer program without having to resort to the [Term] rule.
\begin{equation*} \begin{prooftree} \AxiomC{$\vdash\hoare P{s_1}Q$} \AxiomC{$\vdash\hoare Q{s_2}R$} \LeftLabel{[SeqS]} \BinaryInfC{$\vdash\hoare{P}{\CSeq{s_1}{\CSeq{s_2}\CTerm}}{R}$} \end{prooftree} \end{equation*}
Example 7.4.4.
Let us consider the following program, that exchanges the contents of two variables:
\begin{equation*} {\CBlock{\CAssnVV tx \CAssnVV xy \CAssnVV yt}} \end{equation*}
When formulating the specification, we run into a small problem: We'd like to express in the postcondition that \(\CVar y\) equals the value that \(\CVar x\) had at the beginning of the program. However, the program overwrites \(\CVar x\) and we cannot relate to \(\CVar x\) initial value anymore. This can be solved by using ghost variables (see (7.3)) that capture the initial values of all variables in the program but are forbidden to be modified by the program itself.
So, the Hoare triple, we'd like to prove is:
\begin{equation*} \vdash\hoare{\CVar Y=\CVar y\land\CVar X=\CVar x} {\CBlock{\CAssnVV tx \CAssnVV xy \CAssnVV yt}}{\CVar Y=\CVar x\land\CVar X=\CVar y} \end{equation*}
For now, we know only the precondition and the postcondition because they are part of our proof goal. But the [Seq] rule requires that we come up with a condition \(R\) to split up the block Hoare triple into smaller ones. We have to choose \(R\) so that we can complete the proofs. Initially, it may not be clear how to pick the right \(R\) so that the proof goes through. In our simple example, we can however exploit the fact that the constituent statements solely are assignment statements: looking back at Definition 7.4.1 we see that the precondition of the Hoare triple of an assignment is actually derived from the postcondition. We can use this insight to derive all the \(R\)s in our proof tree. To this end, let us sketch the proof tree first and then derive all the missing \(R\)s using the assignment's Hoare triple.
\begin{equation*} \begin{prooftree} \AxiomC{$\vdash\hoare{R_3}{\CAssnVV tx}{R_2}$} \AxiomC{$\vdash\hoare{R_2}{\CAssnVV xy}{R_1}$} \AxiomC{$\vdash\hoare{R_1}{\CAssnVV yt}{Q}$} \LeftLabel{[SeqS]} \BinaryInfC{$\vdash\hoare{R_2}{\CAssnVV xy \CAssnVV yt}{Q}$} \LeftLabel{[Seq]} \BinaryInfC{$\vdash\hoare{\CVar Y=\CVar y\land\CVar X=\CVar x}{\CAssnVV tx \CAssnVV xy \CAssnVV yt}{\CVar Y=\CVar x\land\CVar X=\CVar y}$} \LeftLabel{[Block]} \UnaryInfC{$\vdash\hoare{\underbrace{\CVar Y=\CVar y\land\CVar X=\CVar x}_{=P}}{\CBlock{\CAssnVV tx \CAssnVV xy \CAssnVV yt}}{\underbrace{\CVar Y=\CVar x\land\CVar X=\CVar y}_{=Q}}$} \end{prooftree} \end{equation*}
Now, the assignment Hoare triple determines the \(R\)s in the following way:
\begin{align*} R_1\amp =\CVar Y=\CVar x\land\CVar X=\CVar t\\ R_2\amp =\CVar Y=\CVar y\land\CVar X=\CVar t\\ R_3\amp =\CVar Y=\CVar y\land\CVar X=\CVar x \end{align*}
We see that the assertions \(R_3\) and \(P\) are syntactically the same which completes the proof. We come back to this kind of proof technique in Subsection 7.4.2 where we actually develop an algorithm to determine the missing invariants.

If-Then-Else.

A proof for the Hoare triple \(\vdash\hoare P{\CIf e{s_1}{s_2}}Q\) can be obtained from proofs about the constituent statements. However, the preconditions of the Hoare triples of the then and else case can be strengthened by the conditional because we know that each case that \(s_1\) is executed in also satisfies \(e\) (and similarly for \(s_2\) and \(\neg e\)).
Definition 7.4.5. Hoare triple for if-then-else.
\begin{equation*} \begin{prooftree} \AxiomC{$\vdash\hoare {e\land P}{s_1}Q$} \AxiomC{$\vdash\hoare {\neg e\land P}{s_2}Q$} \LeftLabel{[If]} \BinaryInfC{$\vdash\hoare{P}{\CIf e{s_1}{s_2}}{Q}$} \end{prooftree} \end{equation*}
Example 7.4.6.
Let us consider a small program that computes the minimum two numbers:
\begin{equation*} \CIf{\CBinary{<}{\CVar x}{\CVar y}}{\CAssnVV rx}{\CAssnVV ry} \end{equation*}
The Hoare triple we would like to prove is:
\begin{equation*} \vdash\hoare{\ltrue}{\CIf{\CBinary{<}{\CVar x}{\CVar y}}{\CAssnVV rx}{\CAssnVV ry}}{\CVar r\le\CVar x\land\CVar r\le\CVar y\land(\CVar r=\CVar x\lor\CVar r=\CVar y)} \end{equation*}
By Definition 7.4.5, we get the following first step in our proof tree:
\begin{equation*} \begin{prooftree} \AxiomC{$\vdash\hoare{\CBinary{\lt}xy}{\CAssnVV rx}{Q}$} \AxiomC{$\vdash\hoare{\CBinary{\ge}xy}{\CAssnVV ry}{Q}$} \LeftLabel{[If]} \BinaryInfC{$\vdash\hoare{\ltrue}{\CIf{\CBinary{<}{\CVar x}{\CVar y}}{\CAssnVV rx}{\CAssnVV ry}}{\underbrace{\CVar r\le\CVar x\land\CVar r\le\CVar y\land(\CVar r=\CVar x\lor\CVar r=\CVar y)}_{=Q}}$} \end{prooftree} \end{equation*}
Now, we run into a small problem. Let's consider the triple for the then-part: using rule [Assign] (Definition 7.4.1), we can prove the triple
\begin{equation*} \begin{prooftree} \AxiomC{} \UnaryInfC{$\vdash\hoare{Q[\CVar x/\CVar r]}{\CAssnVV rx}{Q}$} \end{prooftree} \end{equation*}
but not
\begin{equation*} \begin{prooftree} \AxiomC{} \UnaryInfC{$\vdash\hoare{\CBinary{\lt}xy}{\CAssnVV rx}{Q}$} \end{prooftree} \end{equation*}
Both preconditions are syntactically different (\(Q[\CVar x/\CVar r]\ne\CBinary{\lt}xy\)) but logically equivalent (\(Q[\CVar x/\CVar r]\equiv\CBinary{\lt}xy\)): they are satisfied by the exact same set of states. So, we cannot apply the rule [Assign] directly.
We can solve this problem by using the rule of consequence to generate an appropriate verification condition:
\begin{equation*} \begin{prooftree} \AxiomC{$\CBinary{\lt}xy\simp Q[\CVar x/\CVar r]$} \AxiomC{} \RightLabel{[Assign]} \UnaryInfC{$\vdash\hoare{Q[\CVar x/\CVar r]}{\CAssnVV rx}{Q}$} \LeftLabel{[Consequence]} \BinaryInfC{$\vdash\hoare{\CBinary{\lt}xy}{\CAssnVV rx}{Q}$} \end{prooftree} \end{equation*}
Verification conditions are logical formulas that result from the [Consequence] rule and constitute additional premises that have to be satisfied in a Hoare-logic proof. We will come back to them in Subsection 7.4.2.
Coming back to the example above, the else case can be dealt with similarly and generates another verification condition:
\begin{equation*} \begin{prooftree} \AxiomC{$\CBinary{\ge}xy\simp Q[\CVar y/\CVar r]$} \AxiomC{} \RightLabel{[Assign]} \UnaryInfC{$\vdash\hoare{Q[\CVar y/\CVar r]}{\CAssnVV ry}{Q}$} \LeftLabel{[Consequence]} \BinaryInfC{$\vdash\hoare{\CBinary{\ge}xy}{\CAssnVV ry}{Q}$} \end{prooftree} \end{equation*}

Loops.

To define the proof rule for the while loop we resort to the concept of a loop invariant. A loop invariant is an assertion that holds true before and after the execution of a loop body. Hence, if some assertion \(I\) is a loop invariant, it will also hold before the loop was entered and after the loop was left (if it was left at all). This gives rise to the following proof rule:
\begin{equation*} \begin{prooftree} \AxiomC{$\vdash\hoare{I\land e}s{I}$} \LeftLabel{[While]} \UnaryInfC{$\vdash\hoare{I}{\CWhile es}{I\land\neg e}$} \end{prooftree} \end{equation*}
The premise expresses that \(I\) must be a loop invariant. Note that we can strengthen the precondition because whenever \(s\) is executed, \(e\) also holds. In a similar way we know that as soon as we have left the loop, \(e\) will be false, hence we can stipulate the postcondition \(I\land\neg e\text{.}\)
Example 7.4.7.
Let us consider an example here as well. We subtract \(\CVar y\) from \(\CVar x\) until \(\CVar x\) becomes less than \(\CVar y\text{.}\) At the same time, we count how many times we subtracted \(\CVar y\) in \(q\text{.}\) In the end, \(\CVar q\) is the quotient of \(\CVar x\) divided by \(\CVar y\) and \(\CVar x\) contains the remainder.
\begin{equation*} \begin{prooftree} \AxiomC{} \RightLabel{[Assign]} \UnaryInfC{$\vdash\hoare{P}{\CAssnVV q0}{I}$} \AxiomC{$\mathsf{Tree}_W$} \RightLabel{[SeqS]} \BinaryInfC{$\vdash\hoare{\underbrace{X=x}_{=P}}{\CAssnVV q0 \underbrace{\CWhile {\CVar x\geq \CVar y} {\CBlock{\CAssign{\CVar x}{\CVar x-\CVar y}\CAssign{\CVar q}{\CVar q+\CConst 1}}}}_{\eqdef W}}{\underbrace{\underbrace{\CVar q\cdot \CVar y+\CVar x=\CVar X}_{=I}\land \CVar x\lt \CVar y}_{=Q}}$} \end{prooftree} \end{equation*}
For better readability, we split off a part of the proof tree into a separate part designated by \(\mathsf{Tree}_W\text{.}\)
\begin{equation*} \begin{prooftree} \AxiomC{$I\land \CVar x\geq \CVar y\Rightarrow R[\CVar x-\CVar y/\CVar x]$} \AxiomC{} \RightLabel{[Assign]} \UnaryInfC{$\vdash\hoare{R[\CVar x-\CVar y/\CVar x]}{\CAssign{\CVar x}{\CVar x-\CVar y}}{R}$} \RightLabel{[Csq]} \BinaryInfC{$\vdash\hoare{I\land \CVar x\geq \CVar y}{\CAssign{\CVar x}{\CVar x-\CVar y}}{R}$} \AxiomC{} \RightLabel{[Assign]} \UnaryInfC{$\vdash\hoare{R}{\CAssign{\CVar q}{\CVar q+\CConst 1}}{I}$} \RightLabel{[SeqS]} \BinaryInfC{$\vdash\hoare{I \land \CVar x\geq \CVar y}{\CAssign{\CVar x}{\CVar x-\CVar y}\CAssign{\CVar q}{\CVar q+\CConst 1}}{I}$} \RightLabel{[Block]} \UnaryInfC{$\vdash\hoare{I \land \CVar x\geq \CVar y}{\CBlock{\CAssign{\CVar x}{\CVar x-\CVar y}\CAssign{\CVar q}{\CVar q+\CConst 1}}}{I}$} \RightLabel{[While]} \UnaryInfC{$\vdash\hoare{I}{W}{I\land \CVar x \lt \CVar y}$} \end{prooftree} \end{equation*}
For the correctness proof, we need to remember the original value of \(x\) with a ghost variable. The invariant \(\CVar q\cdot \CVar y + \CVar x = \CVar X\) is conveniently also the postcondition of the program together with the fact that the remainder is smaller than the divisor. Therefore, we do not need the consequence rule for the while loop.
Let us go through the proof from right to left. After the loop, the condition is false. Therefore, we know \(\CVar x\lt \CVar y\text{.}\) It remains to show that the invariant \(\CVar q\cdot \CVar y + \CVar x = \CVar X\) is true before the loop was entered and in each iteration of the loop. We can do this by using the [While] rule.
Before and after each iteration of the loop, \(\CVar q\) contains the count of how many times we subtracted \(\CVar y\) from \(\CVar x\text{.}\) In the loop, we subtract \(\CVar y\) from \(\CVar x\) one additional time and increase \(\CVar q\) by one. By doing this, we invalidate that invariant for a moment in the loop body but restore it afterward before reaching the end of the loop body. The intermediate condition \(R\) is true at the point before \(\CVar q\) is increased but after \(\CVar y\) is subtracted from \(\CVar x\text{.}\)
\begin{gather*} R = I[\CVar q+1/\CVar q] = (\CVar q\cdot \CVar y + \CVar x + \CVar y = \CVar X) \end{gather*}
By applying the [Assign] rule to \(R\text{,}\) we get the back to the invariant:
\begin{gather*} I = R[\CVar x-\CVar y/\CVar x] = (\CVar q\cdot \CVar y + \CVar x - \CVar y + \CVar y = \CVar X) = (\CVar q \cdot \CVar y +\CVar x = \CVar X) \end{gather*}
Lastly, it remains to show that the invariant was satisfied before the loop was entered. This is done by using the [Assign] rule for the first assignment.
\begin{gather*} P = I[\CConst 0/\CVar q] = (\CConst 0\cdot \CVar y + \CVar x = \CVar X) = (\CVar x = \CVar X) \end{gather*}
Prove that the remainder is non-negative for a non-negative \(x\text{.}\)
Do you need the pre-condition \(\CConst 0\lt \CVar y\text{?}\) Why or why not?

Subsection 7.4.2 Mechanizing Verification

We have seen in the examples in Subsection 7.4.1 that some rules require the verifier to “guess” assertions to complete the proofs. This was the case for the rules for the sequence, if-then-else, and the while loop. In the examples, we also made the experience that sometimes these free assertions were determined by other rules: for example, the assignment rule essentially defines the precondition based on its postcondition. This helped us to determine the “free” assertions of the sequence rule in Example 7.4.4.
In this section, we introduce two functions
\begin{align*} \hpc \amp:(\Stmt\cup\Prg)\to\Assert\to\Assert\\ \hvc \amp:(\Stmt\cup\Prg)\to\Assert\to\powerset{\Assert} \end{align*}
that determine, given a postcondition \(Q\text{,}\) for each statement or program, a precondition and a set of verification conditions such that
\begin{equation*} \begin{prooftree} \AxiomC{$\hvc q\,Q$} \UnaryInfC{$\vdash\hoare {\hpc q\,Q}qQ$} \end{prooftree} \end{equation*}
where \(q\) is either a statement or a program. We can use such rules together with the consequence rule to prove a program correct with respect to a specification \((P,Q)\) in the following way:
\begin{equation} \begin{prooftree} \AxiomC{$P\limp\hpc q\,Q$} \AxiomC{$\hvc q\,Q$} \UnaryInfC{$\vdash\hoare{\hpc q\,Q}qQ$} \BinaryInfC{$\vdash\hoare PqQ$} \end{prooftree}\tag{7.4} \end{equation}
The idea behind this is that the function \(\hpc\) determines a precondition that describes the states under which an execution of \(q\) properly terminates (if it terminates at all) in a state that satisfies a given postcondition \(Q\text{.}\) One can indeed show that except for the while loop, the function \(\hpc\) gives the weakest precondition, i.e. the precondition that describes exactly those states for which the program terminates properly in a state that satisfies the postcondition \(Q\text{.}\)
The function \(\hvc\) collects verification conditions that are necessary to justify \(\vdash\hoare{\hpc q\,Q}q{Q}\text{.}\) In doing so, we essentially defer the proof of the program's correctness to a theorem prover, a tool that can check if a verification condition is valid or not. 17 

Definition 7.4.9. Preconditions and Verification Conditions.

\begin{align*} \hpc\,\denot{\CTerm}\,Q \amp = Q\\ \hpc\,\denot{\CSeq sp}\,Q \amp = \hpc\,s\,(\hpc\,p\,Q)\\ \hpc\,\denot{\CAssign{\CVar x}{e}}\,Q \amp = Q[e/\CVar x]\\ \hpc\,\denot{\CBlock{p}}\,Q \amp = \hpc\,p\,Q\\ \hpc\,\denot{\CIf{e}{s_1}{s_2}}\,Q \amp = (e\land\hpc\,s_1\,Q)\lor(\neg e\land\hpc\,s_2\,Q)\\ \hpc\,\denot{\CWhileInv{e}{s}{I}}\,Q \amp = I \end{align*}
\begin{align*} \hvc \denot{\CTerm}\,Q \amp = \{\}\\ \hvc \denot{\CSeq sp}\,Q \amp = \hvc s\,(\hpc\,p\,Q)\cup \hvc\,p\,Q\\ \hvc \denot{\CAssign{\CVar x}{e}}\,Q \amp = \{\}\\ \hvc \denot{\CBlock{p}}\,Q \amp = \hvc p\,Q\\ \hvc \denot{\CIf{e}{s_1}{s_2}}\,Q \amp = (\hvc s_1\,Q)\cup(\hvc s_2\,Q)\\ \hvc \denot{\CWhileInv{e}{s}{I}}\,Q \amp = \{I\land e\limp\hpc s\,I, \neg e\land I\limp Q\}\cup(\hvc s\,I) \end{align*}
The while rule does not so nicely fit into this schema because the invariant of the while loop cannot be automatically inferred but has to be annotated by the programmer, hence the syntax \(\mathtt{\_Inv}(I)\text{.}\) Especially, the invariant cannot be automatically deduced from the postcondition and in the definition of \(\hpc\) for while, the postcondition \(Q\) is simply ignored. Instead, the while case relies on several verification conditions that “connect” the while loop to the rest of the program.
The following theorems state that Definition 7.4.9 is sound.
Sketch. By induction over \(s\text{.}\) The assignment and empty block case are trivial; just put in the definition of \(\hpc\) and \(\hvc\) into the rule of the theorem and we get the empty block and assignment rules from Subsection 7.4.1. We'll show the if-then-else and while case here.
  • if-then-else: \(s=\CIf e{s_1}{s_2}\text{.}\) By induction, we have that the rules for \(s_1\) and \(s_2\) are sound. Hence, we can derive the hoare triple in question:
    \begin{equation*} \begin{prooftree} \AxiomC{$\hvc s_1\,Q$} \UnaryInfC{$\vdash\hoare{\hpc {s_1}\,Q}{s_1}{Q}$} \LeftLabel{[Conseq]$\qquad\quad$} \UnaryInfC{$\vdash\hoare{e\land\hpc {s}\,Q}{s_1}{Q}$} \AxiomC{$\hvc s_2\,Q$} \UnaryInfC{$\vdash\hoare{\hpc {s_2}\,Q}{s_2}{Q}$} \RightLabel{[Conseq]} \UnaryInfC{$\vdash\hoare{\neg e\land\hpc {s}\,Q}{s_2}{Q}$} \LeftLabel{[If]} \BinaryInfC{$\vdash\hoare{\hpc s\,Q}s{Q}$} \end{prooftree} \end{equation*}
    Using the consequence rule, we strengthen the preconditions of \(s_1\) and \(s_2\) accordingly. \(\hpc s\,Q\) is now defined such that \(e\land\hpc s\,Q\Rightarrow\hpc {s_1}\,Q\) and \(\neg e\land\hpc s\,Q\Rightarrow\hpc {s_2}\,Q\text{.}\) The verification conditions that are needed to justify this derivation are just the ones of \(s_1\) and \(s_2\text{,}\) so \(\hvc s\,Q=(\hvc {s_1}\,Q)\cup (\hvc {s_2}\,Q)\)
  • The while loop \(\CWhileInv esI\text{:}\) We need to prove that \(\vdash\hoare {\hpc \denot{\CWhileInv esI}\,Q}{\CWhileInv esI}Q\) with \(\hpc s\,Q=I\text{.}\) By induction, we have that the rule
    \begin{equation*} \begin{prooftree} \AxiomC{$\hvc s\,I$} \UnaryInfC{$\vdash\hoare{\hpc s\,I}sI$} \end{prooftree} \end{equation*}
    is sound. We use this to derive our proof goal using the following derivation:
    \begin{equation*} \begin{prooftree} \AxiomC{$I\land e\limp\hpc s\,I$} \AxiomC{$\hvc s\,I$} \UnaryInfC{$\vdash\hoare{\hpc s\,I}sI$} \LeftLabel{[Conseq]$\qquad\quad$} \BinaryInfC{$\vdash\hoare{I\land e}sI$} \LeftLabel{[While]} \UnaryInfC{$\vdash\hoare I{\CWhileInv esI}{\neg e\land I}$} \AxiomC{$\neg e\land I\limp Q$} \LeftLabel{[Conseq]$\qquad\quad$} \BinaryInfC{$\vdash\hoare I{\CWhileInv esI}Q$} \end{prooftree} \end{equation*}
    In that derivation, we used the consequence rule twice and generate two additional verification conditions: \(I\land e\limp\hpc s\,I\) and \(\neg e\land I\limp Q\) which is reflected in the definition of \(\hvc\text{.}\)
Exercise.

Example 7.4.12.

Consider the division program from Example 7.4.7.
\begin{equation*} \CAssign{\CVar q}{\CConst 0} \CWhileInv{\CBinary{\ge}{\CVar x}{\CVar y}}{ \underbrace{\CBlock{ \CAssign{\CVar x}{\CBinary{-}{\CVar x}{\CVar y}} \CAssign{\CVar q}{\CBinary{+}{\CVar q}{\CConst 1}} }}_{s} }{\CVar q*\CVar y+\CVar x=\CVar X} \end{equation*}
which we want to prove correct with respect to the specification
\begin{align*} P \amp = \CVar x=\CVar X\\ Q \amp = \CVar q*\CVar y+\CVar x=\CVar X\land \CVar x\lt\CVar y \end{align*}
using the loop invariant
\begin{align*} I \amp = \CVar q*\CVar y+\CVar x=\CVar X \end{align*}
Using Definition 7.4.9, we have:
\begin{align*} \hpc \denot{\mathtt{while}\ \dots}\,Q \amp = I\\ \hpc \denot{\CAssign{\CVar q}{\CConst 0}\dots}\,Q \amp = \hpc \denot{\CAssign{\CVar q}{\CConst 0}}\,(\hpc \denot{\mathtt{while}\ \dots}\,Q)\\ \amp = \hpc \denot{\CAssign{\CVar q}{\CConst 0}}\,I = (\CVar 0*\CVar y+\CVar x=\CVar X) \end{align*}
and
\begin{align*} \hvc \denot{\CAssign{\CVar q}{\CConst 0}\dots}\,Q \amp = \hvc \denot{\CAssign{\CVar q}{\CConst 0}}\,(\hpc \denot{\mathtt{while}\ \dots}\,Q)\cup \hvc \denot{\mathtt{while}\dots}\,Q\\ \amp = \hvc \denot{\mathtt{while}\dots}\,Q\\ \hvc \denot{\mathtt{while}\ \dots}\,Q \amp = (\hvc s\,I)\cup \{\CBinary{\lt}{\CVar x}{\CVar y}\land I\simp Q,I\land\CBinary{\ge}{\CVar x}{\CVar y}\simp\hpc s\,I \} \\ \hvc s\,I \amp = \emptyset\\ \hpc s\,I \amp = \left[(\CVar q+\CConst 1)*\CVar y+(\CVar x-\CVar y)=\CVar X\right] \end{align*}
So in summary, we have:
\begin{align*} \hpc \denot{\CAssign{\CVar q}{\CConst 0}\dots}\,Q \amp = \CConst 0*\CVar y+\CVar x=X\\ \hvc \denot{\CAssign{\CVar q}{\CConst 0}\dots}\,Q \amp = \{\CBinary{\lt}{\CVar x}{\CVar y}\land I\simp Q,I\land\CBinary{\ge}{\CVar x}{\CVar y}\simp\hpc s\,I \} \end{align*}
Coming back to (7.4), all verification conditions are:
  1. \(\displaystyle P\simp \CConst 0*\CVar y+\CVar x=X\)
  2. \(\displaystyle \CVar x\lt\CVar y\land I\simp Q\)
  3. \(\displaystyle I\land\CVar x\ge\CVar y\simp (\CVar q+\CConst 1)*\CVar y+(\CVar x-\CVar y)=\CVar X\)
They can now be given to a theorem solver. If the solver reports that they are valid, the program is partially correct with respect to the given specification.

Assert and Assume.

Let us define two further language elements that will allow us to specify pre- and postconditions directly in the program. Assert is defined as
\begin{equation*} \CAssert{e}=\CIf{e}{\CBlock{}}{\CAbort} \end{equation*}
and therefore
\begin{equation*} \hpc \denot{\CAssert e}\,Q=e\land Q\quad \hvc \denot{\CAssert e}\,Q=\{\} \end{equation*}
We use the statement \(\CAssume{a}\) to specify pre-conditions or give additional constraints. In a more realistic setting, one could for example provide additional information on inputs, like maybe some input is always in a specific range, etc. Assume is directly defined through a while loop that makes the program diverge if the condition \(e\) is not fulfilled. This leads to a loop invariant that states that \(\neg e\) or \(Q\) holds (or written differently: \(e\simp Q\)). The \(Q\) part comes from the fact that if the loop terminates (in this case equivalent to not being entered), we want the postcondition \(Q\) is satisfied.
\begin{equation*} \CAssume{e}\defeq\CWhileInv{\neg e}{\CBlock{}}{e\simp Q} \end{equation*}
and with the loop invariant \(e\simp Q\text{,}\) if follows that
\begin{equation*} \hpc \denot{\CAssume{e}}\,Q=e\simp Q\quad \hvc \denot{\CAssume e}\,Q=\emptyset \end{equation*}
Exercise. Investigate the proof tree for the left side.
Note that the decidability of verification conditions strongly depends on the theories the conditions use. Some of the practically most relevant theories (e.g. arithmetic on natural numbers including multiplication) are not decidable, which means that the theorem prover might not terminate.
<Prev^TopNext>