What we've done so far:

• Formalized Imp
  • identifiers and states
  • abstract syntax trees
  • evaluation functions (for aexps and bexps)
  • evaluation relation (for commands)
• Proved some metatheoretic properties
  • determinism of evaluation
  • equivalence of some different ways of writing down the definitions (e.g. functional and relational definitions of arithmetic expression evaluation)
  • guaranteed termination of certain classes of programs
  • meaning-preservation of some program transformations
  • behavioral equivalence of programs (Equiv)

This chapter:

• A systematic method for reasoning about the correctness of particular programs

Hoare Logic

Goals:

• a natural notation for program specifications
• a compositional proof technique for program correctness

Plan:

• assertions (Hoare Triples)
• proof rules
• decorated programs
• loop invariants
• examples

Assertions

Informally, instead of writing we'll write just Given two assertions P and Q, we say that P implies Q, written P ⇾ Q (in ASCII, P ->> Q), if, whenever P holds in some state st, Q also holds.

We'll also have occasion to use the "iff" variant of implication between assertions:

Hoare Triples

Since the behavior of a command is to transform one state to another, it is natural to express claims about commands in terms of assertions that are true before and after the command executes:

• "If command c is started in a state satisfying assertion P, and if c eventually terminates in some final state, then this final state will satisfy the assertion Q."

Such a claim is called a Hoare Triple. The property P is called the precondition of c, while Q is the postcondition. Formally:

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

Proof Rules

Plan:

• introduce one "proof rule" for each Imp syntactic form
• plus a couple of "structural rules" that help glue proofs together
• prove programs correct using these proof rules, without ever unfolding the definition of hoare_triple

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. This can be made even more general. To conclude that an arbitrary property Q holds after X ::= a, we need to assume that Q holds before X ::= a, but with all occurrences of X replaced by a in Q. This leads to the Hoare rule for assignment where "Q [X ↦ a]" is pronounced "Q where a is substituted for X". For example, these are valid applications of the assignment rule: To formalize the rule, we must first formalize the idea of "substituting an expression for an Imp variable in an assertion." That is, given a proposition P, a variable X, and an arithmetic expression a, we want to derive another proposition P' that is just the same as P except that, wherever P mentions X, P' should instead mention a. Since P is an arbitrary Coq proposition, we can't directly "edit" its text. Instead, we can achieve the effect we want by evaluating P in an updated state:

That is, P [X ↦ a] is an assertion P' that is just like P except that, wherever P looks up the variable X in the current state, P' instead uses the value of the expression a. To see how this works, let's calculate what happens with a couple of examples. First, suppose P' is (X ≤ 5) [X ↦ 3] — that is, more formally, P' is the Coq expression which simplifies to and further simplifies to and by further simplification to That is, P' is the assertion that 3 is less than or equal to 5 (as expected). For a more interesting example, suppose P' is (X ≤ 5) [X ↦ X+1]. Formally, P' is the Coq expression which simplifies to and further simplifies to That is, P' is the assertion that X+1 is at most 5. Now we can give the precise proof rule for assignment:

	(hoare_asgn)
{{Q [X ↦ a]}} X ::= a {{Q}}

We can prove formally that this rule is indeed valid.

Here's a first formal proof using this rule.

Consequence

Sometimes the preconditions and postconditions we get from the Hoare rules won't quite be the ones we want in the particular situation at hand — they may 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, does not. This triple is valid, but it is not an instance of hoare_asgn because True and (X = 3) [X ↦ 3] are not syntactically equal assertions. However, they are logically equivalent, so if one triple is valid, then the other must certainly be as well. We might capture this observation with the following rule:

{{P'}} c {{Q}}
P ⇿ P'	(hoare_consequence_pre_equiv)
{{P}} c {{Q}}

Taking this line of thought a bit further, we can see that strengthening the precondition or weakening the postcondition of a valid triple always produces another valid triple. This observation is captured by two Rules of Consequence.

{{P'}} c {{Q}}
P ⇾ P'	(hoare_consequence_pre)
{{P}} c {{Q}}

{{P}} c {{Q'}}
Q' ⇾ Q	(hoare_consequence_post)
{{P}} c {{Q}}

Here are the formal versions:

For example, we might use the first consequence rule like this: Or, formally...

Finally, for convenience in some proofs, we can state a "combined" rule of consequence that allows us to vary both the precondition and the postcondition.

{{P'}} c {{Q'}}
P ⇾ P'
Q' ⇾ Q	(hoare_consequence)
{{P}} c {{Q}}

Digression: The eapply Tactic

This is a good moment to introduce another convenient feature of Coq. We had to write "with (P' := ...)" explicitly in the proof of hoare_asgn_example1 and hoare_consequence above, to make sure that all of the metavariables in the premises to the hoare_consequence_pre rule would be set to specific values. (Since P' doesn't appear in the conclusion of hoare_consequence_pre, the process of unifying the conclusion with the current goal doesn't constrain P' to a specific assertion.) This is a little annoying, both because the assertion is a bit long and also because for hoare_asgn_example1 the very next thing we are going to do — applying the hoare_asgn rule — will tell us exactly what it should be! We can use eapply instead of apply to tell Coq, essentially, "Be patient: The missing part is going to be filled in soon."

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 so-called existential variables (written ?nnn) as placeholders for expressions that will be determined (by further unification) later in the proof.

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 }}

Informally, a nice way of recording a proof using the sequencing rule is as a "decorated program" where the intermediate assertion Q is written between c1 and c2:

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. Better:

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

To make this formal, 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."

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

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 — i.e., let's assume 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}}

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 (showing that it establishes the invariant by the time it finishes). This gives us the final version of the rule:

{{P ∧ b}} c {{P}}	(hoare_while)
{{P}} WHILE b DO c END {{P ∧ ~b}}

The proposition P is called an invariant of the loop. One subtlety in the terminology is that calling some assertion P a "loop invariant" doesn't just mean that it is preserved by the body of the loop in question (i.e., {{P}} c {{P}}, where c is the loop body), but rather that P together with the fact that the loop's guard is true is a sufficient precondition for c to ensure P as a postcondition. This is a slightly (but significantly) weaker requirement. For example, if P is the assertion X = 0, then P is an invariant of the loop although it is clearly not preserved by the body of the loop.

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

Review

The rules of Hoare Logic:

	(hoare_asgn)
{{Q [X ↦ a]}} X::=a {{Q}}

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

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

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

{{P ∧ b}} c {{P}}	(hoare_while)
{{P}} WHILE b DO c END {{P ∧ ~b}}

{{P'}} c {{Q'}}
P ⇾ P'
Q' ⇾ Q	(hoare_consequence)
{{P}} c {{Q}}

In the next chapter, we'll see how these rules are used to prove that programs satisfy specifications of their behavior.