Skip to main content

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 first focus on partial correctness and will then later discuss total correctness.

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 Hoare triples for each syntactic elements and see how we can use them to prove programs correct manually. We will then reason about the soundness of these rules, i.e. prove that whatever we can derive with our rules is in fact sound with respect to the semantics of C0. Then, we look into how we can use these rules in a mechanized setting, i.e. a computer program that uses these rules to automatically prove programs correct. Finally, we discuss the extension to total correctness which involves arguing about termination functions.

To keep it simple, we discuss or initial C0 language 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.8 and Definition 7.1.7 we have defined Hoare triples semantically. In this section, we are interested in defining a logic which means a set of proof rules that allow us to derive Hoare triples from a given set of axioms. To make the difference clear, we write

\begin{equation*} \models\hoare PsQ \end{equation*}

when we mean that program \(s\) 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.8 and Definition 7.1.7. We write

\begin{equation*} \vdash\hoare PsQ \end{equation*}

when we mean that we derived the Hoare triple with the proof rules we develop in this section. In Subsection 7.4.2 we will sketch a proof that shows that our rules are sound which formally means that \(\vdash\hoare PsQ\) entails \(\models\hoare PsQ\text{.}\)

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 Corollary 6.3.8 and Definition 7.1.8). 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: 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{\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{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 {\CConst 5=\CBinary{+}{\CVar y}{\CConst 1}}{\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\CConst 5=\CBinary{/}{\CVar y}{\CVar z}}{\CAssign{\CVar x}{\CBinary{/}{\CVar y}{\CVar z}}}{\CVar x=\CConst 5}$} \end{prooftree} \end{equation*}

Block.

Hoare triples for blocks can be broken up into Hoare triples of the individual elements. Here, we are giving two rules that “take apart” the block from the beginning. In principle, other rules are imaginable, e.g. one that decomposes the block into all its constituent statements. The rule we give here will be helpful in Subsection 7.4.3, when we discuss an algorithm to automatically verify programs.

In principle, the following rule says that if we can prove Hoare triples of the first statement and the remainder of 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.
\begin{equation*} \begin{prooftree} \AxiomC{$\vdash\hoare{P}{s_1}R$} \AxiomC{$\vdash\hoare{R}{\CBlock{s_2,\dots,s_n}}Q$} \LeftLabel{[Block]} \BinaryInfC{$\vdash\hoare{P}{\CBlock{s_1,\dots,s_n}}{Q}$} \end{prooftree} \end{equation*}
\begin{equation*} \begin{prooftree} \AxiomC{} \LeftLabel{[Empty]} \UnaryInfC{$\vdash\hoare Q{\CBlock{}}Q$} \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 introducing ghost variables that capture the initial values of all variables in the program but are forbidden to be modified by the program itself. We denote the ghost variables here with capital letters.

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 block rule requires that we come of 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 actually 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}$} \AxiomC{$\vdash\hoare{Q}{\CBlock{}}{Q}$} \BinaryInfC{$\vdash\hoare{R_1}{\CBlock{\CAssnVV yt}}{Q}$} \BinaryInfC{$\vdash\hoare{R_2}{\CBlock{\CAssnVV xy \CAssnVV yt}}{Q}$} \BinaryInfC{$\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.3 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}$} \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 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{} \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.3.

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{} \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 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{Tree$_W$} \AxiomC{} \RightLabel{[Empty]} \UnaryInfC{$\vdash\hoare{Q}{\CBlock{}}{Q}$} \RightLabel{[Block]} \BinaryInfC{$\vdash\hoare{I}{\CBlock{W}}{Q}$} \RightLabel{[Block]} \BinaryInfC{$\vdash\hoare{\underbrace{X=x}_{=P}}{\CBlock{\CAssnVV q0 \underbrace{\CWhile {x\geq y} {\CBlock{\CAssign{\CVar x}{\CVar x-\CVar y}\CAssign{\CVar q}{\CVar q+\CConst 1}}}}_{=W}}}{\underbrace{\underbrace{\CVar q\cdot \CVar y+\CVar x=\CVar X}_{=I}\land \CVar x\lt \CVar y}_{=Q}}$} \end{prooftree} \end{equation*}
We split off the proof for the while body into Tree\(_W\) and used a custom [Block\(_1\)] rule for better readability:
\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{[Conseq]} \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{[Block$_1$]} \UnaryInfC{$\vdash\hoare{R}{\CBlock{\CAssign{\CVar q}{\CVar q+\CConst 1}}}{I}$} \RightLabel{[Block]} \BinaryInfC{$\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 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 Soundness

In the last section, we have defined proof rules to derive Hoare triples. However, at no point did we ground these proof rules in the semantics of C0. This is the subject of this section. Soundness means that the Hoare triples we derive with our rules are actually telling us the truth with respect to the semantics of C0. Put a bit more formally:

\begin{equation*} \vdash\hoare PsQ\quad\implies\quad\models\hoare PsQ \end{equation*}

where

\begin{equation*} \models\hoare PsQ \end{equation*}

is defined as (Definition 7.1.8)

\begin{equation} \forall\sigma.\,(\sigma\models P)\limp\left(\forall c.\config s\sigma\terminates c\limp(\exists \sigma'.\,c=\sigma'\land\sigma'\models Q)\right)\tag{7.3} \end{equation}

One important ingredient for the soundness proof is to define a so-called big-step semantics for C0 that captures the terminating and aborting behavior of C0 programs. In principle, this big-step semantics is similar to our definition of termination in Definition 6.3.6. However, it consists of inference rules that will provide the facts that make the soundness proof go through nicely. We will not develop this in great detail here but only give a sketch on how this proof goes and how the big-step semantics is defined.

Big-step Semantics.

We define a relation \({}\bigstep{}\subseteq \Stmt\times\Sigma\times K\) (where \(K\) is the set of configurations) so that \(\config{s}{\sigma}\bigstep k\) if \(\config{s}{\sigma}\) terminates in \(k\text{.}\) We show only some of the rules here and focus on the properly terminating behavior.

\begin{equation*} \begin{prooftree} \AxiomC{$\denotR{e}\sigma=v\in\Val$} \AxiomC{$\denotL{l}\sigma=a\in\Addr$} \BinaryInfC{$\config{\CAssign le}{(\rho,\mu)}\bigstep (\rho,\mu[a\mapsto v])$} \end{prooftree} \end{equation*}
\begin{equation*} \begin{prooftree} \AxiomC{} \UnaryInfC{$\config{\CBlock{}}{\sigma}\bigstep\sigma$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\config{s_1}\sigma\bigstep\sigma'$} \AxiomC{$\config{\CBlock{s_2,\dots,s_n}}{\sigma'}\bigstep\sigma''$} \BinaryInfC{$\config{\CBlock{s_1,\dots,s_n}}{\sigma}\bigstep\sigma''$} \end{prooftree} \end{equation*}
\begin{equation*} \begin{prooftree} \AxiomC{$\denotR{e}\sigma\ne 0$} \AxiomC{$\config{s_1}\sigma\bigstep\sigma'$} \BinaryInfC{$\config{\CIf e{s_1}{s_2}}{\sigma}\bigstep\sigma'$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\denotR{e}\sigma= 0$} \AxiomC{$\config{s_2}\sigma\bigstep\sigma'$} \BinaryInfC{$\config{\CIf e{s_1}{s_2}}{\sigma}\bigstep\sigma'$} \end{prooftree} \end{equation*}
\begin{equation*} \begin{prooftree} \AxiomC{$\denotR{e}\sigma\ne 0$} \AxiomC{$\config{s}\sigma\bigstep\sigma'$} \AxiomC{$\config{\CWhile es}\sigma'\bigstep\sigma''$} \TrinaryInfC{$\config{\CWhile es}{\sigma}\bigstep\sigma'$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\denotR{e}\sigma= 0$} \UnaryInfC{$\config{\CWhile es}{\sigma}\bigstep\sigma$} \end{prooftree} \end{equation*}
\begin{equation*} \dots \text{remaining rules not shown for the sake of simplicity} \dots \end{equation*}

The next step would be to prove that \(\bigstep\) is equivalent to \(\terminates\) so that we can make use of \(\bigstep\) when arguing about partial correctness. We do not do this here for the sake of brevity but just take it for granted.

Using the big-step semantics, we then come to the actual theorem with its proof.

by induction over the rules defined in Subsection 7.4.1. Note that this is just a sketch to show the basic principle and we only consider some of the cases here.

  • The assignment axiom is

    \begin{equation*} \begin{prooftree} \AxiomC{} \LeftLabel{[Assign]} \UnaryInfC{$\vdash\hoare{\exprdef e\land Q[e/\CVar x]}{\CAssign{\CVar x}e}{Q}$} \end{prooftree} \end{equation*}

    To show this rule sound, we have to plug in \(\exprdef\,e\land Q[e/\CVar x]\text{,}\) the assignment itself, and \(Q\) into (7.3):

    \begin{equation*} \forall\sigma.\,(\sigma\models \exprdef\,e\land Q[e/\CVar x])\limp \left(\forall c.\config{\CAssign{\CVar x}e}\sigma\terminates c\limp(\exists \sigma'.\,c=\sigma'\land\sigma'\models Q)\right) \end{equation*}

    So, assume some state \(\sigma\models Q[e/\CVar x]\text{.}\) In each such state, according to Definition 6.3.4 \(\config{\CAssign{\CVar x}e}{\sigma}\) terminates properly for each such state in the state \(\sigma'=\sigma[\CVar x\mapsto v]\) with \(v=\denotR e\sigma\text{.}\) The question now is if \(\sigma'\models Q\text{.}\) So we need to show that

    \begin{equation*} \sigma\models \exprdef e\land Q[e/\CVar x]\quad\limp\quad\sigma[\CVar x\mapsto\denotR e{\sigma}]\models Q \end{equation*}

    This can be proved by induction over the assertion \(Q\text{.}\) The most interesting case is when \(Q=\CVar x\text{.}\) Based on Definition 7.1.3, \(\sigma\models\CVar x\) if \(\denotR{\CVar x}\sigma\ne 0\text{.}\) So we need to prove that

    \begin{equation*} \denotR{\CVar x[e/\CVar x]}\sigma\ne 0\quad\implies\quad\denotR{\CVar x}{\sigma[\CVar x\mapsto\denotR e{\sigma}]}\ne 0 \end{equation*}

    which is trivially true.

  • The empty block axiom is

    \begin{equation*} \begin{prooftree} \AxiomC{} \LeftLabel{[Empty]} \UnaryInfC{$\vdash\hoare{Q}{\CBlock{}}{Q}$} \end{prooftree} \end{equation*}
    To show this rule sound, we have to again plug it into (7.3):
    \begin{equation*} \forall\sigma.\,(\sigma\models Q)\limp \left(\forall c.\config{\CBlock{}}\sigma\bigstep c \limp(\exists \sigma'.\,c=\sigma'\land\sigma'\models Q)\right) \end{equation*}
    Now, \(\config{\CBlock{}}{\sigma}\bigstep\sigma\) is an axiom of our big-step semantics, so \(c=\sigma\) and there exists a \(\sigma'\) such that \(c=\sigma'\) and \(\sigma'\models Q\text{,}\) namely \(\sigma\text{.}\)

  • The non-empty block rule is

    \begin{equation*} \begin{prooftree} \AxiomC{$\vdash\hoare{P}{s_1}R$} \AxiomC{$\vdash\hoare{R}{\CBlock{s_2,\dots,s_n}}Q$} \LeftLabel{[Block]} \BinaryInfC{$\vdash\hoare{P}{\CBlock{s_1,\dots,s_n}}{Q}$} \end{prooftree} \end{equation*}

    The induction hypothesis tells us that the Hoare triples in the premises are sound, so we can assume that \(\models\hoare P{s_1}R\) and \(\models\hoare R{\CBlock{s_2,\dots,s_n}}Q\text{.}\) This means that if \(s_1\) terminates properly, it terminates in a state that satisfies \(R\) and similarly for the other premise.

    Let us now make the simplification of assuming that both programs in the premise terminate properly if they terminate. In a real proof we'd also have to consider the possibility that either of them aborts or gets stuck but we will not cover this here for the sake of simplicity.

    Let us now again put in the constituents of this Hoare triple into the definition of partial correctness:

    \begin{equation*} \forall\sigma.\,(\sigma\models P)\limp \left(\forall c.\config{\CBlock{s_1,\dots,s_n}}\sigma\bigstep c \limp(\exists \sigma'.\,c=\sigma'\land\sigma'\models Q)\right) \end{equation*}

    and assume there is a state \(\sigma\) that satisfies the precondition \(P\text{.}\) Assume further that the block terminates in a state \(\sigma''\text{.}\) By the block rule of the big-step semantics, we then have that \(\config{s_1}{\sigma}\bigstep\sigma'\) and \(\config{\CBlock{s_2,\dots,s_n}}{\sigma'}\bigstep\sigma''\text{.}\) By the induction hypothesis, we have that if \(s_1\) terminates, it terminates properly in a state that satisfies \(R\text{.}\) And also that that the rest of the block will terminate properly, if it terminates, in a state that satisfies \(Q\) and hence the entire block, executed on a state that satisfies \(P\text{,}\) will terminate properly in a state that satisfies \(Q\) if it terminates properly. Both together gives that if the block terminates, it terminates in a state that satisfies \(Q\text{.}\)

  • The while loop rule is

    \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 tells us that \(I\) is a loop invariant and by the induction hypothesis we can assume that whenever we execute the loop body \(s\) on a state that satisfies \(I\land e\text{,}\) it will, if it terminates, terminate in a state that satisfies \(I\text{.}\)

    Let us first consider a state \(\sigma\) that satisfies the precondition \(I\text{.}\) We will now start a second induction over the big-step relation \(\bigstep\text{.}\)

    • In the base case we have \(\denotR e\sigma=0\) and need to show

      \begin{equation*} \left(\config{\CWhile es}\sigma\bigstep\sigma \limp(\exists \sigma'.~ \sigma'\models I\land\neg e)\right) \end{equation*}
      \(c\) can be chosen to be \(\sigma\) and together with \(\denotR e\sigma=0\) we have that \(\sigma\models I\land\neg e\text{.}\)

    • In the induction step we have that \(\denotR e\sigma\ne 0\text{,}\) \(\config s\sigma\bigstep\sigma'\text{,}\) and \(\config{\CWhile es}{\sigma'}\bigstep\sigma''\text{.}\) These are the premises for the big-step rule of while. Now, assume \(\sigma\) satisfies \(I\text{.}\) Because \(\denotR e\sigma\ne 0\text{,}\) we have that \(\sigma\models I\land e\text{.}\) This allows us to use the outer induction hypothesis which is \(\models\hoare{I\land e}sI\text{.}\) From that we can conclude that if \(s\) terminates, it terminates in a state that satisfies \(I\text{.}\) With \(\config s\sigma\bigstep\sigma'\) we get that \(\sigma'\models I\text{.}\) The induction hypothesis tells us that if \(\sigma'\) satisfies \(I\) then \(\config{\CWhile es}{\sigma'}\) will terminate in \(\sigma''\) which satisfies \(I\land\neg e\text{.}\) Therefore, if \(\CWhile es\) terminates, it terminates in a state that satisfies \(I\land\neg e\text{.}\)

Subsection 7.4.3 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 block, 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 Block rule in Example 7.4.4.

In this section, we introduce two functions

\begin{align*} \hpc \amp:\Stmt\to\Assert\to\Assert\\ \hvc \amp:\Stmt\to\Assert\to\powerset{\Assert} \end{align*}

that determine, given a postcondition \(Q\text{,}\) for each statement a precondition and a set of verification conditions such that

\begin{equation*} \begin{prooftree} \AxiomC{$\hvc s\,Q$} \UnaryInfC{$\vdash\hoare {\hpc s\,Q}sQ$} \end{prooftree} \end{equation*}

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 s\,Q$} \AxiomC{$\hvc s\,Q$} \UnaryInfC{$\vdash\hoare{\hpc s\,Q}sQ$} \BinaryInfC{$\vdash\hoare PsQ$} \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 \(s\) properly terminates (if it terminates at all) in a state that satisfies a given postcondition \(Q\text{.}\) One can indeed show that for all statements 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 s\,Q}s{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.10. Preconditions and Verification Conditions.

\begin{align*} \hpc\,\denot{\CAssign{\CVar x}{e}}\,Q \amp = Q[e/\CVar x]\\ \hpc\,\denot{\CBlock{}}\,Q \amp = Q\\ \hpc\,\denot{\CBlock{s_1,\dots,s_n}}\,Q \amp = \hpc\,s_1\,(\hpc\,\denot{\CBlock{s_2,\dots,s_n}}\,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{\CAssign{\CVar x}{e}}\,Q \amp = \{\}\\ \hvc \denot{\CBlock{}}\,Q \amp = \{\}\\ \hvc \denot{\CBlock{s_1,\dots,s_n}}\,Q \amp = \hvc s_1\,(\hpc\denot{\CBlock{s_2,\dots,s_n}}\,Q)\cup \hvc \denot{\CBlock{s_2,\dots,s_n}}\,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 theorem states that Definition 7.4.10 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}$} \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}$} \UnaryInfC{$\vdash\hoare{\neg e\land\hpc {s}\,Q}{s_2}{Q}$} \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$} \BinaryInfC{$\vdash\hoare{I\land e}sI$} \UnaryInfC{$\vdash\hoare I{\CWhileInv esI}{\neg e\land I}$} \AxiomC{$\neg e\land I\limp Q$} \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{.}\)

Example 7.4.12.

Consider the division program from Example 7.4.7.

\begin{equation*} \CBlock{ \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.10, we have:

\begin{align*} \hpc \denot{\mathtt{while}\ \dots}\,Q \amp = I\\ \hpc \denot{\CBlock{\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{\CBlock{\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 = (\CVar q+\CConst 1)*\CVar y+(\CVar x-\CVar y)=\CVar X \end{align*}

So in summary, we have:

\begin{align*} \hpc \denot{\CBlock{\CAssign{\CVar q}{\CConst 0}\dots}}\,Q \amp = \CConst 0*\CVar y+\CVar x=X\\ \hvc \denot{\CBlock{\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 that 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=\{\} \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.