Chapter 14 Hoare logic for control structures

• 14.1 Deductive verification reminder
• 14.2 Hoare logic: a program logic for structured control
• 14.3 Hoare logic for jumps
• 14.4 Hoare logic for coroutines and cooperative threads
• 14.5 Further reading

14.1 Deductive verification reminder

Just as mathematical logics provide reasoning principles to prove properties of mathematical definitions, program logics provide reasoning principles to prove properties of programs such as functional correctness. This logic-based approach to program verification is called deductive verification.

In order to use deductive verification, the program must first be annotated with logical assertions about its state, such as

• preconditions: expected properties of inputs;
• postconditions: guaranteed properties of outputs;
• invariants attached to loops or data structures: expected to hold at every loop iteration or throughout the lifetime of the data structure.

Then, using a program logic for the programming language and with the help of automated or interactive theorem proving, we can prove that the preconditions imply the invariants and the postconditions.

For example, here is a C function annotated with logical assertions written in the ACSL specification language:

The precondition (requires) states that the parameter a given to set_to_zero must point to a valid array of size at least n. The postcondition (ensures) states that when set_to_zero returns, the elements 0 to n−1 of the array a contain the value 0. The assigns clause states that only these elements of a are modified, not any other memory location. Finally, the invariant clause in the loop asserts that the first i elements of array a have already been set to 0.

14.2 Hoare logic: a program logic for structured control

From Turing to Floyd to Hoare.  Deductive verification was initially developed in the context of unstructured programs represented as flowcharts (control flow graphs, CFG) annotated with logical assertions. This approach first appeared in an early communication by Turing (1949), but this text went unnoticed until it was formally published and commented on by Morris and Jones (1984). The same approach was independently reinvented and thoroughly studied by Floyd (1967).

However, the concept of a program logic is absent from both Turing (1949) and Floyd (1967). Instead, they focus on the next step in deductive verification after program logics: generating verification conditions from an annotated program.

Program logics as the foundations for deductive verification appear in the famous article An Axiomatic Basis for Computer Programming by Hoare (1969). Instead of flowcharts, Hoare considers Algol-style structured programs. This is significant because program logics and structured control are deeply intertwined. Not only program verification follows the structure of the program, but the rules of the program logic also correspond almost one-to-one with the control structures of the programming language, as shown in the remainder of this chapter.

Hoare triples.  Like most program logics, Hoare logic defines three-place relations between a command c and two logical assertions about the values of the program variables: a precondition P and a postcondition Q. These relations are called “Hoare triples” and are usually written as [  P  ]  c  [  Q  ] or {  P  }  c  {  Q  } .

The “strong Hoare triple” [  P  ]  c  [  Q  ] means that when the command c is started in a state that satisfies the precondition P, it always terminates without errors, and its final state satisfies the postcondition Q.

The “weak Hoare triple” {  P  }  c  {  Q  } is similar, except that it does not guarantee termination. It means that when the command c is started in a state that satisfies the precondition P, it executes without errors, and if it terminates, its final state satisfies the postcondition Q.

---

{  P  }  skip  {  P  }       (skip)

 

{  Q [x := e]  }  x := e  {  Q  }       (assign)

 

{  P  }  s1  {  Q  }       {  Q  }  s2  {  R  }       (seq)  {  P  }  s1; s2  {  R  }

 

{  P ∧ b  }  s1  {  Q  }       {  P ∧ ¬ b  }  s2  {  Q  }       (cond)  {  P  }  if b then s1 else s2  {  Q  }

 

{  P ∧ b  }  s  {  P  }       (while)  {  P  }  while b do s  {  P ∧ ¬ b  }

 

P ⇒ P′      {  P′  }  s  {  Q′  }      Q′ ⇒ Q      (consequence)  {  P  }  s  {  Q  }

 

Figure 14.1: The rules of weak Hoare logic for the IMP language.

---

Weak Hoare logic.  Figure 14.1 shows the rules for a weak Hoare logic (the one that does not guarantee termination). This logic applies to the IMP language of figure 6.1.

There are two axioms corresponding to the skip and assignment statements. A skip does not change the value of any variable. Therefore, any property P of the program variables that holds “before” skip also holds “after”. Hence, {  P  }  skip  {  P  } for all P.

Consider an assignment x := e and a postcondition Q. The postcondition Q does not have to hold for all possible values of x, only for the value e that was just assigned to x. Therefore, Q [x := e] must hold “before” the assignment. This explains the (assign) axiom {  Q{x := e}  }  x := e  {  Q  } . For example,

The rule (consequence) allows us to adjust the precondition and postcondition of a command s. We can replace a precondition P′ with a stronger or equivalent precondition P (that is, P ⇒ P′), and a postcondition Q′ with a weaker or equivalent postcondition Q (that is, Q′ ⇒ Q). For example, combining the (consequence) and (assign) rules, we have

Also by combining these two rules, we can show Floyd’s rule for assignments:

The remaining three rules capture the essence of the three control structures of IMP: sequencing, conditional, and while loops.

The assertion Q describes the intermediate state during the execution of s₁;s₂. It acts as a postcondition for s₁ and as a precondition for s₂. The precondition of s₁;s₂ is the same as that of s₁. The postcondition of s₂ is the same as that of s₁;s₂.

Both branches s₁ and s₂ of the conditional must guarantee the postcondition Q. The “then” branch s₁ can assume that the condition b is true, in addition to the precondition P, since it will not be executed if b is false. Similarly, the “else” branch s₂ can assume that b is false in addition to P.

The precondition P of a while loop is used as a loop invariant. The body s of the loop can assume that P holds initially, and that the loop condition b is true. It must then guarantee that P holds at the end of s, so that the next iteration can proceed. When the loop exits, the invariant P holds and the condition b is false. Therefore, the loop postcondition is P ∧ ¬ b.

---

{  0 ≤ a  }  ⇒  {  a = b · 0 + a  ∧  0 ≤ a  }   r := a;     {  a = b · 0 + r  ∧  0 ≤ r  }   q := 0;     {  a = b · q + r  ∧  0 ≤ r  }   while  r ≥ b  do (     {  a = b · q + r  ∧  0 ≤ r  ∧  r ≥ b  }  ⇒      {  a = b · (q + 1) + (r − b)  ∧  0 ≤ r − b  }      r := r − b;     {  a = b · (q + 1) + r  ∧  0 ≤ r  }      q := q + 1     {  a = b · q + r  ∧  0 ≤ r  }   )     {  a = b · q + r  ∧  0 ≤ r  ∧  r < b  }  ⇒     {  q = a / b  ∧  r = a mod b  }

Figure 14.2: Deductive verification of the Euclidean division algorithm. s1; {  Q  } s2 means that Q is the postcondition of s1 and the precondition of s2. {  P  } ⇒ {  P′  } denotes an application of the rule of consequence.

---

Figure 14.2 shows the steps in weak Hoare logic for verifying the following Euclidean division algorithm:

Assuming a ≥ 0 initially, this verification shows that q = a / b and r = a mod b at the end of the execution. Note that we have proved partial correctness, but not termination: the program loops if b ≤ 0.

Strong Hoare logic.  Figure 14.3 shows the rules for strong Hoare triples [  P  ]  c  [  Q  ] , those that guarantee termination in addition to partial correctness. Except the rule for loops, the rules are similar to the rules for weak triples. Indeed, skip and assignment statements always terminate, and sequences and conditionals preserve termination. Only loops can cause divergence, as in while true do s.

The rule for while loops ensures termination with the help of a variant expression e, which is a nonnegative integer expression that decreases strictly with each iteration of the loop. For some complex loops, multiple variants ordered lexicographically are needed to show termination.

The decrease of e is expressed using a ghost variable α: a mathematical variable that is not assignable and has the same value in the precondition and the postcondition. Therefore, having e = α in the precondition of s and e < α in its postcondition means that e strictly decreases during the execution of s.

For example, if Ediv is the Euclidean division program of figure 14.2, we can prove the following strong triple:

The loop variant is the variable r, which strictly decreases at each loop iteration provided that b > 0.

---

[  P  ]  skip  [  P  ]       (skip)

 

[  Q [x := e]  ]  x := e  [  Q  ]       (assign)

 

[  P  ]  s1  [  Q  ]       [  Q  ]  s2  [  R  ]       (seq)  [  P  ]  s1; s2  [  R  ]

 

[  P ∧ b  ]  s1  [  Q  ]       [  P ∧ ¬ b  ]  s2  [  Q  ]       (cond)  [  P  ]  if b then s1 else s2  [  Q  ]

 

∀ α,   [  P ∧ b ∧ e = α  ]  s  [  P ∧ 0 ≤ e < α  ]       (while)  [  P  ]  while b do s  [  P ∧ ¬ b  ]

 

P ⇒ P′      [  P′  ]  s  [  Q′  ]      Q′ ⇒ Q      (consequence)  [  P  ]  s  [  Q  ]

 

Figure 14.3: The rules of strong Hoare logic for the IMP language

---

Other kinds of loops.  We can provide verification rules for types of loops other than while loops. These rules can be derived from the rules of Hoare logic and the encodings of these other loops in terms of while loops.

For instance, here is a rule for do…while loops, with the exit test at the end of each iteration:

It follows from the equivalence of do s while b with s; while b do s.

Similarly, we can derive a rule for an Ada-style loop with the exit test located in the middle of the loop body:

Counted for loops are even more interesting, because they are guaranteed to terminate if the loop body always terminates. Define

We can derive the following strong Hoare triple for this counted loop:

The precondition ℓ ≤ h − 1 is the weakest precondition that ensures i = h + 1 at the end. The syntactic restriction on s ensures that neither i nor the free variables of h are modified during an execution of the loop body s. Otherwise, termination could be compromised, as in for   i = 0  to  0  do  i := i − 1 or for   i = 0  to  h  do  h := h + 1 .

Rather than imposing a syntactic restriction, we can add proof obligations ensuring that i and h have the same values at the beginning and at the end of s:

14.3 Hoare logic for jumps

Handling “goto” in a program logic.  As Hoare writes in the conclusion of his seminal paper,

Areas which do present real difficulty are labels and jumps, pointers, and name parameters. Proofs of programs which made use of these features are likely to be elaborate, and it is not surprising that this should be reflected in the complexity of the underlying axioms. (Hoare, 1969)

One obvious “real difficulty” is that goto jumps create control flows that are not accounted for by the rules of Hoare logic. Consider for example

The command s can be entered not only with b = true, as the rule (conditional) asserts, but also with b = false, since a jump to the label L is performed in this other case. To account for this fact, the program logic must ensure that the precondition of s holds regardless of how it is entered, whether by the normal flow of execution or via a goto L.

Clint and Hoare’s rule for goto.  Clint and Hoare (1972) propose the following rule for Algol-style block-scoped labels and goto:

The notation A ⊢ B (read: “A entails B”) corresponds to a hypothetical judgment in natural deduction: assuming A in addition to the rules of Hoare logic, we can derive B.

The premises of the rule above state that s₁ and s₂ are verified under the additional premise {  R  }  goto L  {  false  } , from which we can deduce {  R  }  goto L  {  X  } for any assertion X, using the (consequence) rule. This ensures that R, the precondition of s₂, holds whether s₂ is entered normally after s₁ finishes, or via a goto L statement in s₁ or s₂.

Note that there is no axiom for goto L statements. The only triples that can be deduced about a goto jump are those that follow from the hypothetical judgment {  R  }  goto L  {  false  } introduced by the (scoped-label) rule.

Issues with Clint and Hoare’s rule.  O’Donnell (1982) identifies delicate points of the approach proposed by Clint and Hoare (1972). First, in the case of nested blocks that define identically named labels L

“the” precondition associated with L is ambiguous:

This issue can be resolved by renaming one of the labels L, so as to ensure the freshness of the label names.

Second, the logical handling of {  R  }  goto L  {  false  } ⊢ A is delicate: it must be treated as a logical entailment, not a logical implication “ {  R  }  goto L  {  false  } implies A in some model”. In the latter case, since {  R  }  goto L  {  false  } is unconstrained by the axioms and rules of Hoare logic, we could take it to be false. Then, the implication would hold trivially, and we could derive incorrect Hoare triples such as:

The first premise can be considered to be true when understood as an implication {  false  }  goto L  {  false  } ⟹ {  true  }  goto L  {  false  } , yet does not hold when understood as logical entailment {  false  }  goto L  {  false  } ⊢ {  true  }  goto L  {  false  } . This is because the rule (consequence) does not allow us to replace a false precondition by a true precondition, and no other rule applies here.

The Arbib-Alagic-de Bruijn approach.  Another way to view goto statements is as an alternative way to exit from a command, besides reaching the end of the command. If there are multiple ways to exit from a command, we could use multiple postconditions for the verification, one for each exit method.

This approach was first proposed by Arbib and Alagic (1979) and further studied by de Bruin (1981). Hoare triples become quadruples

where J (as in “jumps”) is a mapping from labels to assertions. The quadruple means “if command s, started in an initial state satisfying P, terminates normally, then the final state satisfies Q; and if it terminates early by performing a goto L statement, the state at that point satisfies J(L)”. The J postcondition can be weakened as the usual postcondition Q.

The J postcondition may be false for commands that always terminate normally:

J is shared between the sub-commands of a sequence (and similarly for conditionals and loops):

A goto L statement can have all of its postconditions be false except for J(L), which is the precondition P of the goto:

In a block that associates a label L with a command s₂, all exits on goto L must satisfy the precondition R of s₂:

Early exits from loops.  The trick with multiple postconditions also applies to structured early exits from loops, such as the break statement. In this case, we can use quadruples {  P  }  s  {  Q  }   {  B  } , where Q is the normal postcondition and B the postcondition for early termination on a break statement. Perhaps confusingly, B is also the precondition for break statements:

Since break statements never terminate normally, the normal postcondition can be taken to be false. Here is the rule for while loops:

The loop catches break statements performed by the loop body s, converting them into normal loop termination. Therefore, the break postcondition of the loop can be false, and the break postcondition of the loop body is the normal postcondition Q of the loop.

We can extend the rule above with a Python-style else clause for a while loop, which is executed only if the loop terminates normally, but not on a break:

A unified treatment of early exits.  Rather than adding a postcondition each time we add a new way of exiting a command, we can use a single postcondition that is a function:

Exit types K are, for example,

The rules for commands that trigger an exit all have the same shape:

We write [K ↦ P] for the function λ K′. if K′ = K then P else false.

Each control structure handles one or more exit types, by adding constraints for the corresponding postcondition. For instance, the sequence handles normal termination:

We write Q + [K ↦ P] for the function λ K′. if K′ = K then P else Q(K′).

The loop handles break and continue exits in addition to normal termination:

The declaration of the label L handles the goto(L) exit:

Exception handlers handle exn(E) exits:

14.4 Hoare logic for coroutines and cooperative threads

Adding coroutines to IMP.  Clint (1973) considers the following presentation of asymmetric coroutines:

When the consumer s₂ performs call p, the execution of s₁ starts, or resumes just after the most recent yield p performed by s₁. When the producer s₁ performs yield p, the execution of s₂ resumes just after the most recent call p performed by s₂. The coroutine command terminates as soon as either s₁ or s₂ terminates. Exchanges of values between s₁ and s₂ take place over shared variables.

In the example above, the coroutine p maintains a histogram h of the observed values obs, and stops as soon as N values have been observed. The client of this coroutine calls p with various values of obs (here, 12 and 41).

Clint’s rule for coroutines.  We associate two assertions A_p and B_p to each coroutine p:

• A_p is the precondition of call p, and therefore the postcondition of yield p, since call p restarts a stopped yield p command;
• B_p is the precondition of yield p and therefore the postcondition of call p, since yield p restarts a stopped call p command.

Clint (1973) proposes the following rule for the coroutine construct:

Like Clint and Hoare’s rule for goto (section 14.3), Clint’s rule for coroutines uses entailments ⊢ in the premises: the verification of the producer s₁ can assume {  B_p  }  yield p  {  A_p  } , and the verification of the consumer s₂ can assume {  A_p  }  call p  {  B_p  } .

Both s₁ and s₂ must guarantee the postcondition Q of the coroutine statement, since the latter terminates as soon as s₁ or s₂ terminates.

The precondition of the producer s₁ is A_p because s₁ begins when s₂ calls p for the first time, in a state that satisfies the precondition A_p of p. In contrast, the precondition of the consumer s₁ is P, the precondition of the entire coroutine statement, because s₁ begins executing immediately.

Below is an outline of the verification of the “histogram” example above:

The invariant I states that the number c of observations is no greater than N, and that the histogram sums up to c:

The precondition A_p for each call statement is I ∧ 0 ≤ obs ≤ M. This ensures that the accesses h[obs] are within bounds. The postcondition B_p is simply the correctness invariant I that relates c and h.

Adding cooperative threads to IMP.  Consider the following command:

The execution of commands s₁, …, s_n is interleaved. Each command performs a yield statement when it is ready to suspend itself and transfer control to another command. Execution is sequential between two yield statements. The command run…end terminates when all commands s_i have terminated.

Below is an example of a producer-consumer model written in this style:

The two threads communicate values via a mailbox that consists of the data shared variable and the full Boolean shared variable. The full variable indicates whether or not the data variable contains a valid value. Initially, full is false. The producer thread (on the left) waits until the mailbox is empty (i.e. full is false), then writes a value in data and flags the mailbox as nonempty. The consumer thread (on the right) waits for the mailbox to be nonempty. It then extracts and processes its contents (data), and flags the mailbox as empty.

A rule for cooperative threads.  The following verification rule for the run…end construct is a symmetrized version of Clint’s rule for coroutines:

The precondition P is the invariant that holds at each “context switch”: when a yield statement causes one of the s_i to start executing, or a suspended yield to resume. It acts as both the precondition and the postcondition of yield. Since execution can start with any of the s_i, they all have P as the precondition. Execution terminates when the last running command terminates. Since this command can be any one of the s_i, all the s_i must guarantee the postcondition Q.

Below is the outline of the verification of the producer-consumer example above. Consider a property R(x) of the exchanged values x, such as R(x) = 0 ≤ x < 10. We assume that the produce and consume functions ensure and require this property, respectively:

The invariant P for the two coroutines is that if the mailbox is not empty, then its contents satisfy R:

We can verify the producer and the consumer independently, using the following intermediate assertions:

In the verification of the producer, after setting data to a value returned by produce and full to true, the invariant P is re-established, so we can iterate again.

In the verification of the consumer, when the while not full do loop terminates, we know that full is true and that the invariant P holds. It follows that R(data) holds. Therefore, we can safely pass data to consume. After setting full to false, the invariant P holds vacuously, so we can iterate again.

14.5 Further reading

Winskel (1993), chapters 9 and 10, gives a detailed account of Hoare logic, using Hoare’s axiomatic style. Nielson and Nielson (2007), chapters 6 and 7, give an alternative presentation of Hoare logic that builds on the operational semantics for IMP.

As described in chapter 15, separation logic (Reynolds, 2002) extends Hoare logic with the ability to reason about resources such as heap-allocated data. Concurrent separation logic (O’Hearn, 2007) further adds support for shared-memory concurrency. Both logics can prove stronger properties than Hoare logic. For example, in the producer/consumer example of section 14.4, we can prove that every resource allocated by the produce function is disposed of by the consume function, which shows that no produced data is lost by the communication protocol.

Procedures and functions are among the “areas [of program logics] which do present real difficulty” mentioned by Hoare (1969). While parameterless, nonrecursive procedures are easily handled, recursion and the various parameter passing semantics (by value, by reference, or by name) are challenging. Apt (1981) surveys the issues and the proposed Hoare logic rules for procedures and functions. Parkinson et al. (2006) use separation logic to re-explain the issues and re-derive the Hoare logic rules.