Lecture 32: Hoare Logic

1 Purpose

Talk about Hoare Logic.

2 Outline

Up until now, all of the programs we have proved properties about have been functional (and pure). But many programs are imperative (and stateful).

We will talk about how to prove properties about imperative programs, using a technique created (and named after) computer scientist Tony Hoare, developed starting in 1969.

To simplify our discussion, we’ll consider state to be program variables.

3 Language

We will use a simple imperative language, with the following syntax:

For example, X := X + 1 increments the value stored at the variable X.

For example, R := X; X := Y; Y := R swaps the contents of X and Y using R as a temporary variable.

For example, IF X = 0 THEN X := 1 ELSE X := 0 flips the value of X.

4 Hoare Logic

We use the notation {P} C {Q} (called Hoare triples) to say that, if the program C starts in a state satisfying P, then it will end in a state satisfying Q.

P and Q are logical statements that describe variables in the program. For example, {X = 0} X := X + 1 {X = 1} says that, if the variable X is 0, then after running X := X + 1, X will be 1.

Hoare triples are often called "partial correctness" statements, since they say that if the program C begins with a state satisfying P (the precondition), if it terminates, it will satisfy Q (the postcondition). This is partial because there is no guarantee that the program C terminates.

Clearly, some Hoare triples are not true. For example, {X = 0} X := X + 1 {X = 2} is not true: if X is 0, then after running X := X + 1, X will be 1, not 2.

Similarly, but more subtly, {X = x ∧ Y = y}X := Y; Y := X{X = y ∧ Y = x} is not true: since after running the first command, both X and Y contain the value y, so the second assignment does nothing.

We would like rules to be able to prove Hoare triples for programs, as they will allow us to be able to ensure that programs (in this case, mutable, imperative programs) satisfy their specifications. While the above attempt to exchange variables did not work, the following does:

{X = x ∧ Y = y}R := X; X := Y; Y := R{X = y ∧ Y = x}

One last note: we can use T (truth) as a trivial logical statement in either the precondition (to require nothing) or the postcondition (to guarantee nothing). A statement {P}C{T} is always (trivially) true, since we make no requirements on the state after C terminates (if it terminates). More usefully, a Hoare triple like {T}C{Q} has no prerequisites, but requires that, if C terminates, it does so in a state satisfying Q. For example, {T}X := 1{X = 1} is true.

5 Proving Hoare Triples

We prove Hoare triples using a set of axioms, presented in the form of inference rules, similar to how we presented the rules of intuitionistic and linear logic last time.

Where P[E/V] means replace occurrences of V with E in P.

We can use this to prove {X = 0}X := X + 1{X = 1}, as follows:

{X + 1 = 1}X := X + 1{X = 1} (by [assign])

{X = 0}X := X + 1{X = 1} (by algebraic simplification)

This rule usually looks backwards to people, but if we use it, we see why it is right (and alternates, which look "more reasonable", allow us to prove obviously false things).

For example, the rule:

Allows us to prove {X = 0}X := 1{1 = 0}, which is clearly nonsense. Another potential rule impersonator-prop:application-mark

But this allows us to prove {X = 0}X := 1{X = 0}, since 1 does not appear in X = 0 at all.

This rule shows that you can strengthen the precondition of the Hoare triple, by proving that the stronger precondition implies the weaker one.

Symmetrically, you can weaken the postcondition of the Hoare triple.

These rules allow you to split specifications into smaller pieces.

The next rule is a key way we reason about imperative programs: step by step.

We can combine several of these rules together to now prove the swap program:

6 Want to learn more?

This, and much more, is in notes by Mike Gordon https://www.cl.cam.ac.uk/archive/mjcg/HL/Notes/Notes.pdf.