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.
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
when we mean that program is in fact totally/partially correct with respect to the specification . This is the notion of a Hoare triple that we have introduced in Definition 7.1.7 and Definition 7.1.6. We write
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 entails . 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.
An assertion is stronger than an assertion if . Correspondingly, is weaker than . Based on the definition of satisfiability (Definition 7.1.4), a weaker assertion is satisfied by more states. For example
In a Hoare triple we can strengthen preconditions and weaken postconditions. Intuitively, this is true because of the following observation: If , each state satisfying also satisfies , so if , we also have . Similarly, if , each state that satisfies also satisfies . Hence, if we have , we then also have . This is reflected in the following rule which is often called rule of consequence:
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 terminate in a state that would satisfy any postcondition. Therefore, for any postcondition the Hoare triple of is
Consider the assignment statement of C0 and a post-condition . Now, let us consider what could be a valid pre-condition that makes the Hoare triple 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 must be defined which is ensured by the predicate . Second, the effect of is to evaluate and assign its value to the variable :
So evaluating on yields the same value as evaluating on . Hence, if satisfies , will satisfy the assertion (read: replaces in ).
because evaluates to the same value on as does on . That’s just the purpose of the assignment. So the Hoare triple
is true and our proof system gets another axiom:
The 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:
The Hoare triple for a block just falls back to the Hoare triple of its constituent program (rule [Block]). The empty program does nothing so the Hoare triple 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 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 .
Because sequences of statements (which form a program) are always terminated by , 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.
Let us consider the following program, that exchanges the contents of two variables: When formulating the specification, we run into a small problem: We’d like to express in the postcondition that equals the value that had at the beginning of the program. However, the program overwrites and we cannot relate to 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:
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 to split up the block Hoare triple into smaller ones. We have to choose so that we can complete the proofs. Initially, it may not be clear how to pick the right 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 s in our proof tree. To this end, let us sketch the proof tree first and then derive all the missing s using the assignment’s Hoare triple.
Now, the assignment Hoare triple determines the s in the following way:
We see that the assertions and are syntactically the same which completes the proof. We come back to this kind of proof technique in Section 7.4.2 where we actually develop an algorithm to determine the missing assertions.
A proof for the Hoare triple 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 is executed in also satisfies (and similarly for and ).
Let us consider a small program that computes the minimum two numbers:
The Hoare triple we would like to prove is:
By Definition 7.4.5, we get the following first step in our proof tree:
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
but not
Both preconditions are syntactically different. 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:
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 Section 7.4.2.
Coming back to the example above, the else case can be dealt with similarly and generates another verification condition:
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 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:
The premise expresses that must be a loop invariant. Note that we can strengthen the precondition because whenever is executed, also holds. In a similar way we know that as soon as we have left the loop, will be false, hence we can stipulate the postcondition .
Let us consider an example here as well. We subtract from until becomes less than . At the same time, we count how many times we subtracted in . In the end, is the quotient of divided by and contains the remainder.
For better readability, we split off a part of the proof tree into a separate part designated by .
For the correctness proof, we need to remember the original value of with a ghost variable. The invariant 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 . It remains to show that the invariant 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, contains the count of how many times we subtracted from . In the loop, we subtract from one additional time and increase 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 is true at the point before is increased but after is subtracted from .
By applying the [Assign] rule to , we get the back to the invariant:
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.
We have seen in the examples in Section 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
that determine, given a postcondition , for each statement or program, a precondition and a set of verification conditions such that
where 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 in the following way:
The idea behind this is that the function determines a precondition that describes the states under which an execution of properly terminates (if it terminates at all) in a state that satisfies a given postcondition . One can indeed show that except for the while loop, the function 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 .
The function collects verification conditions that are necessary to justify . 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. 10Note 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.
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 . Especially, the invariant cannot be automatically deduced from the postcondition and in the definition of for while, the postcondition 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.
For each statement , the following rule is sound.
Proof.
Sketch. By induction over .
The assignment and empty block case are trivial; just put in the definition of and into the rule of the theorem and we get the empty block and assignment rules from Section 7.4.1. We’ll show the if-then-else and while case here.
By induction, we have that the rules for and are sound. Hence, we can derive the hoare triple in question:
Using the consequence rule, we strengthen the preconditions of and accordingly. is now defined such that and . The verification conditions that are needed to justify this derivation are just the ones of and , so
We need to prove that
with . By induction, we have that the rule
is sound. We use this to derive our proof goal using the following derivation:
In that derivation, we used the consequence rule twice and generate two additional verification conditions: and which is reflected in the definition of .
For each program , the following rule is sound.
Proof. Exercise.
Consider the division program from Example 7.4.7.
which we want to prove correct with respect to the specification
using the loop invariant
Using Definition 7.4.9, we have:
and
So in summary, we have:
Coming back to (7.4), all verification conditions are:
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.
Let us define two further language elements that will allow us to specify pre- and postconditions directly in the program. Assert is defined as
and therefore
We use the statement 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 is not fulfilled. This leads to a loop invariant that states that or holds (or written differently: ). The part comes from the fact that if the loop terminates (in this case equivalent to not being entered), we want the postcondition is satisfied.
and with the loop invariant , if follows that
Proof. Exercise. Investigate the proof tree for the left side.