We've begun applying the mathematical tools developed in the first part of the course to studying the theory of a small programming language, Imp.

• We defined a type of abstract syntax trees for Imp, together with an evaluation relation (a partial function on states) that specifies the operational semantics of programs.
  The language we defined, though small, captures some of the key features of full-blown languages like C, C++, and Java, including the fundamental notion of mutable state and some common control structures.
• We proved a number of metatheoretic properties — "meta" in the sense that they are properties of the language as a whole, rather than properties of particular programs in the language. These included:
  • determinacy of evaluation
  • equivalence of some different ways of writing down the definition
  • guaranteed termination of certain classes of programs
  • correctness (in the sense of preserving meaning) of a number of useful program transformations
  • behavioral equivalence of programs (in the optional chapter Equiv.v).
  If we stopped here, we would still have something useful: a set of tools for defining and discussing programming languages and language features that are mathematically precise, flexible, and easy to work with, applied to a set of key properties.
  All of these properties are things that language designers, compiler writers, and users might care about knowing. Indeed, many of them are so fundamental to our understanding of the programming languages we deal with that we might not consciously recognize them as "theorems." But properties that seem intuitively obvious can sometimes be quite subtle — or, in some cases, actually even wrong!
  We'll return to this theme later in the course when we discuss types and type soundness.
• We saw a couple of examples of program verification — using the precise definition of Imp to prove formally that certain particular programs (e.g., factorial and slow subtraction) satisfied particular specifications of their behavior.

In this chapter, we'll take this last idea further. We'll develop a reasoning system called Floyd-Hoare Logic — commonly, if somewhat unfairly, shortened to just Hoare Logic — in which each of the syntactic constructs of Imp is equipped with a single, generic "proof rule" that can be used to reason about programs involving this construct. Hoare Logic originates in the 1960s, and it continues to be the subject of intensive research right up to the present day. It lies at the core of a huge variety of tools that are now being used to specify and verify real software systems.

Hoare Logic

Hoare Logic offers two important things: a natural way of writing down specifications of programs, and a compositional proof technique for proving that these specifications are met — where by "compositional" we mean that the structure of proofs directly mirrors the structure of the programs that they are about.

Assertions

If we're going to talk about specifications of programs, the first thing we'll want is a way of making assertions about properties that hold at particular points in time — i.e., properties that may or may not be true of a given state of the memory.

Exercise: 1 star (assertions)

Paraphrase the following assertions in English. ☐ This way of writing assertions is formally correct — it precisely captures what we mean, and it is exactly what we will use in Coq proofs — but it is a bit heavy to look at, for several reasons. First, every single assertion that we ever write is going to begin with fun st => ; (2) this state st is the only one that we ever use to look up variables (we never need to talk about two different states at the same time); and (3) all the variable lookups in assertions are cluttered with asnat or aslist coercions. When we are writing down assertions informally, we can make some simplifications: drop the initial fun st =>, write just X instead of st X, and elide asnat and aslist. Informally, instead of writing we'll write just

Hoare Triples

Next, we need a way of specifying — making claims about — the behavior of commands. Since we've defined assertions as a way of making claims about the properties of states, and since the behavior of a command is to transform one state to another, a claim about a command takes the following form:

• "If c is started in a state satisfying assertion P, and if c eventually terminates, then the final state is guaranteed to satisfy the assertion Q."

Such a claim is called a Hoare Triple. The property P is called the precondition of c; Q is the postcondition of c. (Traditionally, Hoare triples are written {P} c {Q}, but single braces are already used for other things in Coq.)

Since we'll be working a lot with Hoare triples, it's useful to have a compact notation:

(The hoare_spec_scope annotation here tells Coq that this notation is not global but is intended to be used in particular contexts. The Open Scope tells Coq that this file is one such context. The first notation — with missing postcondition — will not actually be used here; it's just a placeholder for a notation that we'll want to define later, when we discuss decorated programs.)

Exercise: 1 star (triples)

Paraphrase the following Hoare triples in English. ☐

Exercise: 1 star (valid_triples)

Which of the following Hoare triples are valid — i.e., the claimed relation between P, c, and Q is true? (Note that we're using informal mathematical notations for expressions inside of commands, for readability. We'll continue doing so throughout the chapter.) ☐ To get us warmed up, here are two simple facts about Hoare triples.

Weakest Preconditions

Some Hoare triples are more interesting than others. For example, is not very interesting: it is perfectly valid, but it tells us nothing useful. Since the precondition isn't satisfied by any state, it doesn't describe any situations where we can use the command X ::= Y + 1 to achieve the postcondition X <= 5. By contrast, is useful: it tells us that, if we can somehow create a situation in which we know that Y <= 4 ∧ Z = 0, then running this command will produce a state satisfying the postcondition. However, this triple is still not as useful as it could be, because the Z = 0 clause in the precondition actually has nothing to do with the postcondition X <= 5. The most useful triple (with the same command and postcondition) is this one: In other words, Y <= 4 is the weakest valid precondition of the command X ::= Y + 1 for the postcondition X <= 5. In general, we say that "P is the weakest precondition of c for Q" if

• {{P}} c {{Q}}, and
• whenever P' is an assertion such that {{P'}} c {{Q}}, we have P' st implies P st for all states st.

That is, P is the weakest precondition of c for Q if (a) P is a precondition for Q and c, and (b) P is the weakest (easiest to satisfy) assertion that guarantees Q after c.

Exercise: 1 star (wp)

What are the weakest preconditions of the following commands for the following postconditions? ☐

Proof Rules

The goal of Hoare logic is to provide a compositional method for proving the validity of Hoare triples. That is, the structure of a program's correctness proof should mirror the structure of the program itself. To this end, in the sections below, we'll introduce one rule for reasoning about each of the different syntactic forms of commands in Imp — one for assignment, one for sequencing, one for conditionals, etc. — plus a couple of "structural" rules that are useful for gluing things together.

Assignment

The rule for assignment is the most fundamental of the Hoare logic proof rules. Here's how it works. Consider this (valid) Hoare triple: In English: if we start out in a state where the value of Y is 1 and we assign Y to X, then we'll finish in a state where X is 1. That is, the property of being equal to 1 gets transferred from Y to X. Similarly, in the same property (being equal to one) gets transferred to X from the expression Y + Z on the right-hand side of the assignment. More generally, if a is any arithmetic expression, then is a valid Hoare triple. Even more generally, a is any arithmetic expression and Q is any property of numbers, then is a valid Hoare triple. Rephrasing this a bit gives us the general Hoare rule for assignment: For example, these are valid applications of the assignment rule: We could try to formalize the assignment rule directly in Coq by treating Q as a family of assertions indexed by arithmetic expressions — something like this: But this formulation is not very nice, for two reasons. First, it is not quite true! (As a counterexample, consider a Q that inspects the syntax of its argument, such as together with any V = Id 0 because a precondition that reduces to True leads to a postcondition that is False.) And second, even if we could prove something similar to this, it would be awkward to use. A much smoother way of formalizing the rule arises from the following observation:

• "Q where a is substituted for X" holds in a state st iff Q holds in the state update st X (aeval st a).

That is, asserting that a substituted variant of Q holds in some state is the same as asserting that Q itself holds in a substituted variant of the state. Here is the definition of substitution in a state:

This gives us the formal proof rule for assignment:

	(hoare_asgn)
{{assn_sub V a Q}} V::=a {{Q}}

Here's a first formal proof using this rule.

This proof is a little clunky because the hoare_asgn rule doesn't literally apply to the initial goal: it only works with triples whose precondition has precisely the form assn_sub Q V a for some Q, V, and a. So we have to start with asserting a little lemma to get the goal into this form. Doing this kind of fiddling with the goal state every time we want to use hoare_asgn would get tiresome pretty quickly. Fortunately, there are easier alternatives. One simple one is to state a slightly more general theorem that introduces an explicit equality hypothesis:

With this version of hoare_asgn, we can do the proof much more smoothly.

Exercise: 2 stars (hoare_asgn_examples)

Translate these informal Hoare triples... ...into formal statements and use hoare_asgn_eq to prove them.

☐

Exercise: 3 stars (hoarestate2)

The assignment rule looks backward to almost everyone the first time they see it. If it still seems backward to you, it may help to think a little about alternative "forward" rules. Here is a seemingly natural one: Explain what is wrong with this rule. (* FILL IN HERE *)
☐

Exercise: 3 stars, optional (hoare_asgn_weakest)

Show that the precondition in the rule hoare_asgn is in fact the weakest precondition.

☐

Consequence

The discussion above about the awkwardness of applying the assignment rule illustrates a more general point: sometimes the preconditions and postconditions we get from the Hoare rules won't quite be the ones we want — they may (as in the above example) be logically equivalent but have a different syntactic form that fails to unify with the goal we are trying to prove, or they actually may be logically weaker (for preconditions) or stronger (for postconditions) than what we need. For instance, while follows directly from the assignment rule, the more natural triple does not. This triple is also valid, but it is not an instance of hoare_asgn (or hoare_asgn_eq) because True and 3 = 3 are not syntactically equal assertions. In general, if we can derive {{P}} c {{Q}}, it is valid to change P to P' as long as P' is strong enough to imply P, and change Q to Q' as long as Q implies Q'. This observation is captured by the following Rule of Consequence.

{{P'}} c {{Q'}}
P implies P' (in every state)
Q' implies Q (in every state)	(hoare_consequence)
{{P}} c {{Q}}

For convenience, we can state two more consequence rules — one for situations where we want to just strengthen the precondition, and one for when we want to just weaken the postcondition.

{{P'}} c {{Q}}
P implies P' (in every state)	(hoare_consequence_pre)
{{P}} c {{Q}}

{{P}} c {{Q'}}
Q' implies Q (in every state)	(hoare_consequence_post)
{{P}} c {{Q}}

Here are the formal versions:

For example, we might use (the "_pre" version of) the consequence rule like this: Or, formally...

Digression: The eapply Tactic

This is a good moment to introduce another convenient feature of Coq. Having to write P' explicitly in the example above is a bit annoying because the very next thing we are going to do — applying the hoare_asgn rule — is going to determine exactly what it should be. We can use eapply instead of apply to tell Coq, essentially, "The missing part is going to be filled in later."

In general, eapply H tactic works just like apply H except that, instead of failing if unifying the goal with the conclusion of H does not determine how to instantiate all of the variables appearing in the premises of H, eapply H will replace these variables with existential variables (written ?nnn) as placeholders for expressions that will be determined (by further unification) later in the proof. There is also an eassumption tactic that works similarly.

Skip

Since SKIP doesn't change the state, it preserves any property P:

	(hoare_skip)
{{ P }} SKIP {{ P }}

Sequencing

More interestingly, if the command c1 takes any state where P holds to a state where Q holds, and if c2 takes any state where Q holds to one where R holds, then doing c1 followed by c2 will take any state where P holds to one where R holds:

{{ P }} c1 {{ Q }}
{{ Q }} c2 {{ R }}	(hoare_seq)
{{ P }} c1;c2 {{ R }}

Note that, in the formal rule hoare_seq, the premises are given in "backwards" order (c2 before c1). This matches the natural flow of information in many of the situations where we'll use the rule. Informally, a nice way of recording a proof using this rule is as a "decorated program" where the intermediate assertion Q is written between c1 and c2:

Exercise: 2 stars (hoare_asgn_example4)

Translate this decorated program into a formal proof:

☐

Exercise: 3 stars, optional (swap_exercise)

Write an Imp program c that swaps the values of X and Y and show (in Coq) that it satisfies the following specification:

☐

Exercise: 3 stars, optional (hoarestate1)

Explain why the following proposition can't be proven:

☐

Conditionals

What sort of rule do we want for reasoning about conditional commands? Certainly, if the same assertion Q holds after executing either branch, then it holds after the whole conditional. So we might be tempted to write:

{{P}} c1 {{Q}}
{{P}} c2 {{Q}}
{{P}} IFB b THEN c1 ELSE c2 {{Q}}

However, this is rather weak. For example, using this rule, we cannot show that: since the rule tells us nothing about the state in which the assignments take place in the "then" and "else" branches. But, actually, we can say something more precise. In the "then" branch, we know that the boolean expression b evaluates to true, and in the "else" branch, we know it evaluates to false. Making this information available in the premises of the lemma gives us more information to work with when reasoning about the behavior of c1 and c2 (i.e., the reasons why they establish the postcondtion Q).

{{P ∧  b}} c1 {{Q}}
{{P ∧ ~b}} c2 {{Q}}	(hoare_if)
{{P}} IFB b THEN c1 ELSE c2 FI {{Q}}

To interpret this rule formally, we need to do a little work. Strictly speaking, the assertion we've written, P ∧ b, is the conjunction of an assertion and a boolean expression, which doesn't typecheck. To fix this, we need a way of formally "lifting" any bexp b to an assertion. We'll write bassn b for the assertion "the boolean expression b evaluates to true (in the given state)."

A couple of useful facts about bassn:

Now we can formalize the Hoare proof rule for conditionals and prove it correct.

Here is a formal proof that the program we used to motivate the rule satisfies the specification we gave.

Loops

Finally, we need a rule for reasoning about while loops. Suppose we have a loop and we want to find a pre-condition P and a post-condition Q such that is a valid triple. First of all, let's think about the case where b is false at the beginning, so that the loop body never executes at all. In this case, the loop behaves like SKIP, so we might be tempted to write But, as we remarked above for the conditional, we know a little more at the end — not just P, but also the fact that b is false in the current state. So we can enrich the postcondition a little: What about the case where the loop body does get executed? In order to ensure that P holds when the loop finally exits, we certainly need to make sure that the command c guarantees that P holds whenever c is finished. Moreover, since P holds at the beginning of the first execution of c, and since each execution of c re-establishes P when it finishes, we can always assume that P holds at the beginning of c. This leads us to the following rule:

{{P}} c {{P}}
{{P}} WHILE b DO c END {{P ∧ ~b}}

The proposition P is called an invariant. This is almost the rule we want, but again it can be improved a little: at the beginning of the loop body, we know not only that P holds, but also that the guard b is true in the current state. This gives us a little more information to use in reasoning about c. Here is the final version of the rule:

{{P ∧ b}} c {{P}}	[hoare_while]
{{P}} WHILE b DO c END {{P ∧ ~b}}

We can also use the while rule to prove the following Hoare triple, which may seem surprising at first...

Actually, this result shouldn't be surprising. If we look back at the definition of hoare_triple, we can see that it asserts something meaningful only when the command terminates.

If the command doesn't terminate, we can prove anything we like about the post-condition. Here's a more direct proof of the same fact:

Hoare rules that only talk about terminating commands are often said to describe a logic of "partial" correctness. It is also possible to give Hoare rules for "total" correctness, which build in the fact that the commands terminate.

Exercise: Hoare Rules for REPEAT

Exercise: 4 stars (hoare_repeat)

In this exercise, we'll add a new constructor to our language of commands: CRepeat. You will write the evaluation rule for repeat and add a new hoare logic theorem to the language for programs involving it. We recommend that you do this exercise before the ones that follow, as it should help solidify your understanding of the material.

REPEAT behaves like WHILE, except that the loop guard is checked after each execution of the body, with the loop repeating as long as the guard stays false. Because of this, the body will always execute at least once.

Add new rules for REPEAT to ceval below. You can use the rules for WHILE as a guide, but remember that the body of a REPEAT should always execute at least once, and that the loop ends when the guard becomes true. Then update the ceval_cases tactic to handle these added cases.

A couple of definitions from above, copied here so they use the new ceval.

Now state and prove a theorem, hoare_repeat, that expresses an appropriate proof rule for repeat commands. Use hoare_while as a model.

☐

Decorated Programs

The whole point of Hoare Logic is that it is compositional — the structure of proofs exactly follows the structure of programs. This fact suggests that we we could record the essential ideas of a proof informally (leaving out some low-level calculational details) by decorating programs with appropriate assertions around each statement. Such a decorated program carries with it an (informal) proof of its own correctness. For example, here is a complete decorated program: Concretely, a decorated program consists of the program text interleaved with assertions. To check that a decorated program represents a valid proof, we check that each individual command is locally consistent with its accompanying assertions in the following sense:

• SKIP is locally consistent if its precondition and postcondition are the same
      {{ P }} 
      SKIP
      {{ P }} 
• The sequential composition of commands c1 and c2 is locally consistent (with respect to assertions P and R) if c1 is (with respect to P and Q) and c2 is (with respect to Q and R):
      {{ P }} 
      c1;
      {{ Q }} 
      c2
      {{ R }}
• An assignment is locally consistent if its precondition is the appropriate substitution of its postcondition:
      {{ P where a is substituted for X }}  
      X ::= a  
      {{ P }}
• A conditional is locally consistent (with respect to assertions P and Q) if the assertions at the top of its "then" and "else" branches are exactly P∧b and P/\~b and if its "then" branch is locally consistent (with respect to P∧b and Q) and its "else" branch is locally consistent (with respect to P/\~b and Q):
      {{ P }} 
      IFB b THEN
        {{ P ∧ b }} 
        c1 
        {{ Q }}
      ELSE
        {{ P ∧ ~b }} 
        c2
        {{ Q }}
      FI
• A while loop is locally consistent if its postcondition is P/\~b (where P is its precondition) and if the pre- and postconditions of its body are exactly P∧b and P:
      {{ P }} 
      WHILE b DO
        {{ P ∧ b }} 
        c1 
        {{ P }}
      END
      {{ P ∧ ~b }} 
• A pair of assertions separated by => is locally consistent if the first implies the second (in all states):
      {{ P }} =>
      {{ P' }} 

Reasoning About Programs with Hoare Logic

Example: Slow Subtraction

Informally: Formally:

Exercise: Reduce to Zero

Here is a while loop that is so simple it needs no invariant: Your job is to translate this proof to Coq. It may help to look at the slow_subtraction proof for ideas.

Exercise: 2 stars (reduce_to_zero_correct)

☐

Exercise: Slow Addition

The following program adds the variable X into the variable Z by repeatedly decrementing X and incrementing Z.

Exercise: 3 stars (add_slowly_decoration)

Following the pattern of the subtract_slowly example above, pick a precondition and postcondition that give an appropriate specification of add_slowly; then (informally) decorate the program accordingly.

☐

Exercise: 3 stars (add_slowly_formal)

Now write down your specification of add_slowly formally, as a Coq Hoare_triple, and prove it valid.

☐

Example: Parity

Here's another, slightly trickier example. Make sure you understand the decorated program completely. Understanding all the details of the Coq proof is not required, though it is not actually very hard — all the required ideas are already in the informal version.

Exercise: 3 stars (wrong_find_parity_invariant)

A plausible first attempt at stating an invariant for find_parity is the following.

Why doesn't this work? (Hint: Don't waste time trying to answer this exercise by attempting a formal proof and seeing where it goes wrong. Just think about whether the loop body actually preserves the property.)

☐

Example: Finding Square Roots

Exercise: 3 stars, optional (sqrt_informal)

Write a decorated program corresponding to the above correctness proof.

☐

Exercise: Factorial

Recall the factorial Imp program:

Exercise: 3 stars, optional (fact_informal)

Decorate the fact_com program to show that it satisfies the specification given by the pre and postconditions below. Just as we have done above, you may elide the algebraic reasoning about arithmetic, the less-than relation, etc., that is (formally) required by the rule of consequence: (* FILL IN HERE *)
☐

Exercise: 4 stars, optional (fact_formal)

Prove formally that fact_com satisfies this specification, using your informal proof as a guide. You may want to state the loop invariant separately (as we did in the examples).

☐

Reasoning About Programs with Lists

Exercise: 3 stars (list_sum)

Here is a direct definition of the sum of the elements of a list, and an Imp program that computes the sum.

Provide an informal proof of the following specification of sum_program in the form of a decorated version of the program.

☐ Next, let's look at a formal Hoare Logic proof for a program that deals with lists. We will verify the following program, which checks if the number Y occurs in the list X, and if so sets Z to 1.

The proof we will use, written informally, looks as follows: The only interesting part of the proof is the choice of loop invariant: This states that at each iteration of the loop, the original list l is equal to the append of the current value of X and some other list p which is not the value of any variable in the program, but keeps track of enough information from the original state to make the proof go through. (Such a p is sometimes called a "ghost variable"). In order to show that such a list p exists, in each iteration we add the head of X to the end of p. This needs the function snoc, from Poly.v.

The main proof uses various lemmas.

Exercise: 4 stars, optional (list_reverse)

Recall the function rev from Poly.v, for reversing lists.

Write an Imp program list_reverse_program that reverses lists. Formally prove that it satisfies the following specification: You may find the lemmas append_nil and rev_equation useful.

☐

Formalizing Decorated Programs

The informal conventions for decorated programs amount to a way of displaying Hoare triples in which commands are annotated with enough embedded assertions that checking the validity of the triple is reduced to simple algebraic calculations showing that some assertions were stronger than others. In this section, we show that this informal presentation style can actually be made completely formal.

Syntax

The first thing we need to do is to formalize a variant of the syntax of commands that includes embedded assertions. We call the new commands decorated commands, or dcoms.

To avoid clashing with the existing Notation definitions for ordinary commands, we introduce these notations in a special scope called dcom_scope, and we wrap examples with the declaration % dcom to signal that we want the notations to be interpreted in this scope. Careful readers will note that we've defined two notations for the DCPre constructor, one with and one without a =>. The "without" version is intended to be used to supply the initial precondition at the very top of the program.

It is easy to go from a dcom to a com by erasing all annotations.

The choice of exactly where to put assertions in the definition of dcom is a bit subtle. The simplest thing to do would be to annotate every dcom with a precondition and postcondition. But this would result in very verbose programs with a lot of repeated annotations: for example, a program like SKIP;SKIP would have to be annotated as with pre- and post-conditions on each SKIP, plus identical pre- and post-conditions on the semicolon! Instead, the rule we've followed is this:

• The post-condition expected by each dcom d is embedded in d
• The pre-condition is supplied by the context.

In other words, the invariant of the representation is that a dcom d together with a precondition P determines a Hoare triple {{P}} (extract d) {{post d}}, where post is defined as follows:

We can define a similar function that extracts the "initial precondition" from a decorated program.

This function is not doing anything sophisticated like calculating a weakest precondition; it just recursively searches for an explicit annotation at the very beginning of the program, returning default answers for programs that lack an explicit precondition (like a bare assignment or SKIP). Using pre and post, and assuming that we adopt the convention of always supplying an explicit precondition annotation at the very beginning of our decorated programs, we can express what it means for a decorated program to be correct as follows:

To check whether this Hoare triple is valid, we need a way to extract the "proof obligations" from a decorated program. These obligations are often called verification conditions, because they are the facts that must be verified (by some process looking at the decorated program) to see that the decorations are logically consistent and thus add up to a proof of correctness.

Extracting Verification Conditions

First, a bit of notation:

We will write P ⇒ Q (in ASCII, P ~~> Q) for assert_implies P Q.