Copyright (c) 2016

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
THE SOFTWARE.

In the past couple of chapters, 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 of particular programs in the language. These included:
  • 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
  • correctness (in the sense of preserving meaning) of a number of useful program transformations
  • behavioral equivalence of programs (in the Equiv chapter).

If we stopped here, we would already 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 (sometimes also subtly wrong!). We'll return to the theme of metatheoretic properties of whole languages later in the book when we discuss types and type soundness. In this chapter, though, we turn to a different set of issues. Our goal is to carry out some simple examples of program verification — i.e., to use the precise definition of Imp to prove formally that particular programs satisfy particular specifications of their behavior. We'll develop a reasoning system called Floyd-Hoare Logic — often shortened to just Hoare Logic — in which each of the syntactic constructs of Imp is equipped with a generic "proof rule" that can be used to reason compositionally about the correctness of programs involving this construct. Hoare Logic originated 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 multitude of tools that are being used in academia and industry to specify and verify real software systems. Hoare Logic combines two beautiful ideas: a natural way of writing down specifications of programs, and a compositional proof technique for proving that programs are correct with respect to such specifications — where by "compositional" we mean that the structure of proofs directly mirrors the structure of the programs that they are about.

Assertions

To talk about specifications of programs, the first thing we need is a way of making assertions about properties that hold at particular points during a program's execution — i.e., claims about the current state of the memory when execution reaches that point. Formally, an assertion is just a family of propositions indexed by a state.

Exercise: 1 star, optional (assertions)

Paraphrase the following assertions in English (or your favorite natural language).

☐ This way of writing assertions can be a little bit heavy, for two reasons: (1) every single assertion that we ever write is going to begin with fun st ⇒ ; and (2) this state st is the only one that we ever use to look up variables in assertions (we will never need to talk about two different memory states at the same time). For discussing examples informally, we'll adopt some simplifying conventions: we'll drop the initial fun st ⇒, and we'll write just X to mean st X. Thus, 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.

(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.) We'll also want the "iff" variant of implication between assertions:

Hoare Triples

Next, we need a way of making formal claims about the behavior of commands. In general, the behavior of a command is to transform one state to another, so 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: (The traditional notation is {P} c {Q}, but single braces are already used for other things in Coq.)

Exercise: 1 star, optional (triples)

Paraphrase the following Hoare triples in English. ☐

Exercise: 1 star, optional (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, rather than their formal aexp and bexp encodings. We'll continue doing so throughout the chapter.) To get us warmed up for what's coming, here are two simple facts about Hoare triples.

Proof Rules

The goal of Hoare logic is to provide a compositional method for proving the validity of specific Hoare triples. That is, we want the structure of a program's correctness proof to mirror the structure of the program itself. To this end, in the sections below, we'll introduce a 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 for gluing things together. We will then be able to 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 — let's call it 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.

Exercise: 2 stars (hoare_asgn_examples)

Translate these informal Hoare triples... ...into formal statements (use the names assn_sub_ex₁ and assn_sub_ex₂) and use hoare_asgn to prove them.

☐

Exercise: 2 stars (hoare_asgn_wrong)

The assignment rule looks backward to almost everyone the first time they see it. If it still seems puzzling, it may help to think a little about alternative "forward" rules. Here is a seemingly natural one:

	(hoare_asgn_wrong)
{{ True }} X ::= a {{ X = a }}

Give a counterexample showing that this rule is incorrect and argue informally that it is really a counterexample. (Hint: The rule universally quantifies over the arithmetic expression a, and your counterexample needs to exhibit an a for which the rule doesn't work.)

☐

Exercise: 3 stars, advanced (hoare_asgn_fwd)

However, by using an auxiliary variable m to remember the original value of X we can define a Hoare rule for assignment that does, intuitively, "work forwards" rather than backwards.

	(hoare_asgn_fwd)
{{fun st ⇒ P st ∧ st X = m}}
X ::= a
{{fun st ⇒ P st' ∧ st X = aeval st' a }}
(where st' = t_update st X m)

Note that we use the original value of X to reconstruct the state st' before the assignment took place. Prove that this rule is correct (the first hypothesis is the functional extensionality axiom, which you will need at some point). Also note that this rule is more complicated than hoare_asgn.

☐

Exercise: 2 stars, advanced (hoare_asgn_fwd_exists)

Another way to define a forward rule for assignment is to existentially quantify over the previous value of the assigned variable.

	(hoare_asgn_fwd_exists)
{{fun st ⇒ P st}}
X ::= a
{{fun st ⇒ ∃m, P (t_update st X m) ∧
st X = aeval (t_update st X m) a }}

☐

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 can 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 can 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 at the same time.

{{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 annoying, both because the assertion is a bit long and also because, in 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 later in the proof."

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), which function as placeholders for expressions that will be determined (by further unification) later in the proof. In order for Qed to succeed, all existential variables need to be determined by the end of the proof. Otherwise Coq will (rightly) refuse to accept the proof. Remember that the Coq tactics build proof objects, and proof objects containing existential variables are not complete.

Coq gives a warning after apply HP. (The warnings look different between Coq 8.4 and Coq 8.5. In 8.4, the warning says "No more subgoals but non-instantiated existential variables." In 8.5, it says "All the remaining goals are on the shelf," meaning that we've finished all our top-level proof obligations but along the way we've put some aside to be done later, and we have not finished those.) Trying to close the proof with Qed gives an error.

An additional constraint is that existential variables cannot be instantiated with terms containing ordinary variables that did not exist at the time the existential variable was created. (The reason for this technical restriction is that allowing such instantiation would lead to inconsistency of Coq's logic.)

Doing apply HP' above fails with the following error: In this case there is an easy fix: doing destruct HP before doing eapply HQ.

The apply HP' in the last step unifies the existential variable in the goal with the variable y. Note that the assumption tactic doesn't work in this case, since it cannot handle existential variables. However, Coq also provides an eassumption tactic that solves the goal if one of the premises matches the goal up to instantiations of existential variables. We can use it instead of apply HP' if we like.

Exercise: 2 stars (hoare_asgn_examples_2)

Translate these informal Hoare triples... ...into formal statements (name them assn_sub_ex₁' and assn_sub_ex₂') and use hoare_asgn and hoare_consequence_pre to prove them.

☐

Skip

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

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

Sequencing

More interestingly, if the command c₁ takes any state where P holds to a state where Q holds, and if c₂ takes any state where Q holds to one where R holds, then doing c₁ followed by c₂ 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 (c₂ before c₁). This matches the natural flow of information in many of the situations where we'll use the rule, since the natural way to construct a Hoare-logic proof is to begin at the end of the program (with the final postcondition) and push postconditions backwards through commands until we reach the beginning. Informally, a nice way of displaying a proof using the sequencing rule is as a "decorated program" where the intermediate assertion Q is written between c₁ and c₂: Here's an example of a program involving both assignment and sequencing.

We typically use hoare_seq in conjunction with hoare_consequence_pre and the eapply tactic, as in this example.

Exercise: 2 stars (hoare_asgn_example4)

Translate this "decorated program" into a formal proof:

☐

Exercise: 3 stars (swap_exercise)

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

☐

Exercise: 3 stars (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 of the branches, 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 since the rule tells us nothing about the state in which the assignments take place in the "then" and "else" branches. Fortunately, 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 rule gives us more information to work with when reasoning about the behavior of c₁ and c₂ (i.e., the reasons why they establish the postcondition 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 — i.e., it 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.

Example

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

Exercise: 2 stars (if_minus_plus)

Prove the following hoare triple using hoare_if:

Exercise: One-sided conditionals

Exercise: 4 stars (if1_hoare)

In this exercise we consider extending Imp with "one-sided conditionals" of the form IF₁ b THEN c FI. Here b is a boolean expression, and c is a command. If b evaluates to true, then command c is evaluated. If b evaluates to false, then IF₁ b THEN c FI does nothing. We recommend that you do this exercise before the ones that follow, as it should help solidify your understanding of the material. The first step is to extend the syntax of commands and introduce the usual notations. (We've done this for you. We use a separate module to prevent polluting the global name space.)

Next we need to extend the evaluation relation to accommodate IF₁ branches. This is for you to do... What rule(s) need to be added to ceval to evaluate one-sided conditionals?

Now we repeat (verbatim) the definition and notation of Hoare triples.

Finally, we (i.e., you) need to state and prove a theorem, hoare_if₁, that expresses an appropriate Hoare logic proof rule for one-sided conditionals. Try to come up with a rule that is both sound and as precise as possible.

For full credit, prove formally hoare_if1_good that your rule is precise enough to show the following valid Hoare triple: Hint: Your proof of this triple may need to use the other proof rules also. Because we're working in a separate module, you'll need to copy here the rules you find necessary.

☐

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 — 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...

Of course, this result is not surprising if we remember that the definition of hoare_triple asserts that the postcondition must hold only when the command terminates. If the command doesn't terminate, we can prove anything we like about the post-condition. 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. However, in this course we will only talk about partial correctness.

Exercise: REPEAT

Exercise: 4 stars, advanced (hoare_repeat)

In this exercise, we'll add a new command to our language of commands: REPEAT c UNTIL a END. You will write the evaluation rule for repeat and add a new Hoare rule to the language for programs involving it.

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.

To make sure you've got the evaluation rules for REPEAT right, prove that ex1_repeat evaluates correctly.

Now state and prove a theorem, hoare_repeat, that expresses an appropriate proof rule for repeat commands. Use hoare_while as a model, and try to make your rule as precise as possible.

For full credit, make sure (informally) that your rule can be used to prove the following valid Hoare triple:

☐

Summary

So far, we've introduced Hoare Logic as a tool for reasoning about Imp programs. In the reminder of this chapter we'll explore a systematic way to use Hoare Logic to prove properties about programs. The rules of Hoare Logic are:

	(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.

Additional Exercises

Exercise: 3 stars (himp_hoare)

In this exercise, we will derive proof rules for the HAVOC command, which we studied in the last chapter. First, we enclose this work in a separate module, and recall the syntax and big-step semantics of Himp commands.

The definition of Hoare triples is exactly as before. Unlike our notion of program equivalence, which had subtle consequences with occassionally nonterminating commands (exercise havoc_diverge), this definition is still fully satisfactory. Convince yourself of this before proceeding.

Complete the Hoare rule for HAVOC commands below by defining havoc_pre and prove that the resulting rule is correct.