Hoare: Hoare Logic, Part I

In the final chaper of Logical Foundations (Software Foundations, volume 1), we began 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 this volume when we discuss types and type soundness. In this chapter, though, we turn to a different set of issues. Our goal in this chapter 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 structured proof technique for proving that programs are correct with respect to such specifications -- where by "structured" we mean that the structure of proofs directly mirrors the structure of the programs that they are about.

Assertions

An assertion is a logical claim about the state of a program's memory -- formally, a property of states.

For example,

• fun st ⇒ st X = 3 holds for states st in which value of X is 3,
• fun st ⇒ True hold for all states, and
• fun st ⇒ False holds for no states.

Exercise: 1 star, standard, optional (assertions)

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

☐

Notations for Assertions

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 almost 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 fun st => st X = m we'll write just X = m . Here the "doubly curly" braces {{ and }} delimit the scope of an assertion. We'll see more examples below. This example also illustrates a convention that we'll use throughout the Hoare Logic chapters: in informal assertions, capital letters like X, Y, and Z are Imp variables, while lowercase letters like x, y, m, and n are ordinary Coq variables (of type nat). This is why, when translating from informal to formal, we replace X with st X but leave m alone. The convention described above can be implemented in Coq with a little syntax magic, using coercions and annotation scopes, much as we did with the <{ com }> notation in Imp. This new notation automatically lifts aexps, numbers, and Props into Assertions when they appear in the {{ _ }} scope, or when Coq knows that the type of an expression is Assertion. There is no need to understand the details of how these notation hacks work, so we hide them in the HTML version of the notes. (We barely understand some of it ourselves!) For the gory details, see the Coq development. Define syntax notations for working with Assertions

One small limitation of this approach is that we don't have an automatic way to coerce a function application that appears within an assertion to make appropriate use of the state when its arguments should be interpets as Imp arithmetic expressions. Instead, we introduce a notation #f e1 .. en that stands for (fun st ⇒ f (e1 st) .. (en st), letting us manually mark such function calls when they're needed as part of an assertion.

Occasionally we need to "escape" a raw "Coq-defined" function to express a particularly complicated assertion. We can do that using a $ prefix, as in {{ $(raw_coq) }}. For example, {{ $(fun st ⇒ ∀ X, st X = 0) }} indicates an assertion that every variable of X maps to 0 in the given state.

Example Assertions

Here are some example assertions that take advantage of this new notation.

Assertion Implication

Given two assertions P and Q, we say that P implies Q, written P ->> Q, if, whenever P holds in some state st, Q also holds.

Note that the notation for assertion implication is analogous to the "usual" Coq implication →.

We'll also want the "iff" variant of implication between assertions:

(The hoare_spec_scope annotation here tells Coq that this notation is not global but is intended to be used in particular contexts.)

Hoare Triples, Informally

A Hoare triple is a claim about the state before and after executing a command. The standard notation is {P} c {Q} meaning:

• If command c begins execution in a state satisfying assertion P,
• and if c eventually terminates in some final state,
• then that final state will satisfy the assertion Q.

Assertion P is called the precondition of the triple, and Q is the postcondition. Because single braces are already used for other things in Coq, we'll write Hoare triples with double braces: P c Q For example,

• {{X = 0}} X := X + 1 {{X = 1}} is a valid Hoare triple, stating that command X := X + 1 will transform a state in which X = 0 to a state in which X = 1.
• ∀ m, {{X = m}} X := X + 1 {{X = m + 1}} is a proposition stating that the Hoare triple {{X = m}} X := X + 1 {{X = m + 1}} is valid for any choice of m. Note that m in the two assertions is a reference to the Coq variable m, which is bound outside the Hoare triple.

Exercise: 1 star, standard, optional (triples)

Exercise: 1 star, standard, optional (valid_triples)

Which of the following Hoare triples are valid -- i.e., the claimed relation between P, c, and Q is true? 1) True X := 5 X = 5 2) X = 2 X := X + 1 X = 3 3) True X := 5; Y := 0 X = 5 4) X = 2 /\ X = 3 X := 5 X = 0 5) True skip False 6) False skip True 7) True while true do skip end False 8) X = 0 while X = 0 do X := X + 1 end X = 1 9) X = 1 while X <> 0 do X := X + 1 end X = 100

Hoare Triples, Formally

We can formalize valid Hoare triples in Coq as follows:

Notation for Hoare triples

Exercise: 1 star, standard (hoare_post_true)

Prove that if Q holds in every state, then any triple with Q as its postcondition is valid.

☐

Exercise: 1 star, standard (hoare_pre_false)

Prove that if P holds in no state, then any triple with P as its precondition is valid.

☐

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

Skip

Since skip doesn't change the state, it preserves any assertion P:

---

(hoare_skip) P skip P

Sequencing

If 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, 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.

Assignment

The rule for assignment is the most fundamental of the Hoare logic proof rules. Here's how it works. Consider this incomplete Hoare triple: ??? X := Y X = 1 We want to assign Y to X and finish in a state where X is 1. What could the precondition be? One possibility is Y = 1, because if Y is already 1 then assigning it to X causes X to be 1. That leads to a valid Hoare triple: Y = 1 X := Y X = 1 It may seem as though coming up with that precondition must have taken some clever thought. But there is a mechanical way we could have done it: if we take the postcondition X = 1 and in it replace X with Y---that is, replace the left-hand side of the assignment statement with the right-hand side---we get the precondition, Y = 1. That same idea works in more complicated cases. For example: ??? X := X + Y X = 1 If we replace the X in X = 1 with X + Y, we get X + Y = 1. That again leads to a valid Hoare triple: X + Y = 1 X := X + Y X = 1 Why does this technique work? The postcondition identifies some property P that we want to hold of the variable X being assigned. In this case, P is "equals 1". To complete the triple and make it valid, we need to identify a precondition that guarantees that property will hold of X. Such a precondition must ensure that the same property holds of whatever is being assigned to X. So, in the example, we need "equals 1" to hold of X + Y. That's exactly what the technique guarantees. In general, the postcondition could be some arbitrary assertion Q, and the right-hand side of the assignment could be some arbitrary arithmetic expression a: ??? X := a Q The precondition would then be Q, but with any occurrences of X in it replaced by a. Let's introduce a notation for this idea of replacing occurrences: Define Q [X |-> a] to mean "Q where a is substituted in place of X". This yields the Hoare logic rule for assignment: Q [X |-> a] X := a Q One way of reading this rule is: If you want statement X := a to terminate in a state that satisfies assertion Q, then it suffices to start in a state that also satisfies Q, except where a is substituted for every occurrence of X. To many people, this rule seems "backwards" at first, because it proceeds from the postcondition to the precondition. Actually it makes good sense to go in this direction: the postcondition is often what is more important, because it characterizes what we can assume afer running the code. Nonetheless, it's also possible to formulate a "forward" assignment rule. We'll do that later in some exercises. Here are some valid instances of the assignment rule: (X <= 5) [X |-> X + 1] (that is, X + 1 <= 5) X := X + 1 X <= 5 (X = 3) [X |-> 3] (that is, 3 = 3) X := 3 X = 3 (0 <= X /\ X <= 5) [X |-> 3] (that is, 0 <= 3 /\ 3 <= 5) X := 3 {{ 0 <= X /\ X <= 5 To formalize the rule, we must first formalize the idea of "substituting an expression for an Imp variable in an assertion", which we refer to as assertion substitution, or assertion_sub. That is, intuitively, 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 P' should mention a wherever P mentions X. This operation is related to the idea of substituting Imp expressions for Imp variables that we saw in Equiv (subst_aexp and friends). The difference is that, here, P is an arbitrary Coq assertion, so we can't directly "edit" its text. However, we can achieve the same effect by evaluating P in an updated state, defined as follows:

This notation allows us to write this operation as: P[ X |-> a] That is, P [X |-> a] stands for 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 in more detail, 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 fun st => (fun st' => st' X <= 5) (X !-> aeval st 3 ; st), which simplifies to fun st => (fun st' => st' X <= 5) (X !-> 3 ; st) and further simplifies to fun st => ((X !-> 3 ; st) X) <= 5 and finally to fun st => 3 <= 5. 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 fun st => (fun st' => st' X <= 5) (X !-> aeval st (X + 1) ; st), which simplifies to fun st => (X !-> aeval st (X + 1) ; st) X <= 5 and further simplifies to fun st => (aeval st (X + 1)) <= 5. That is, P' is the assertion that X + 1 is at most 5. We can demonstrate formally that we have captured intuitive meaning of "assertion subsitution" by proving some example logical equivalences:

Now, using the substitution operation we've just defined, 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.

Of course, what we'd probably prefer is to prove this simpler triple: X < 4 X := X + 1 X < 5 We will see how to do so in the next section. Complete these Hoare triples by providing an appropriate precondition using ∃, then prove then with apply hoare_asgn. If you find that tactic doesn't suffice, double check that you have completed the triple properly.

Exercise: 2 stars, standard, optional (hoare_asgn_examples1)

☐

Exercise: 2 stars, standard, optional (hoare_asgn_examples2)

☐

Exercise: 2 stars, standard, especially useful (hoare_asgn_wrong)

The assignment rule looks backward to almost everyone the first time they see it. If it still seems puzzling to you, 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 use it to complete the proof below, showing 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)

By using a parameter m (a Coq number) 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 (X !-> m ; st) /\ st X = aeval (X !-> m ; st) a Note that we need to write out the postcondition in "desugared" form, because it needs to talk about two different states: we use the original value of X to reconstruct the state st' before the assignment took place. (Also note that this rule is more complicated than hoare_asgn!) Prove that this rule is correct.

☐

Exercise: 2 stars, advanced, optional (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. Prove that it is correct.

---

(hoare_asgn_fwd_exists) fun st => P st X := a fun st => exists m, P (X !-> m ; st) /\ st X = aeval (X !-> m ; st) 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, (X = 3) [X |-> 3] X := 3 X = 3, follows directly from the assignment rule, but True X := 3 X = 3 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: True ->> (X = 1) [X |-> 1] X := 1 X = 1 Or, formally...

We can also use it to prove the example mentioned earlier. X < 4 ->> (X < 5)[X |-> X + 1] X := X + 1 X < 5 Or, formally ...

Finally, here is 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

Automation

Many of the proofs we have done so far with Hoare triples can be streamlined using the automation techniques that we introduced in the Auto chapter of Logical Foundations. Recall that the auto tactic can be told to unfold definitions as part of its proof search. Let's give it that hint for the definitions and coercions we're using:

Also recall that auto will search for a proof involving intros and apply. By default, the theorems that it will apply include any of the local hypotheses, as well as theorems in a core database. The proof of hoare_consequence_pre, repeated below, looks like an opportune place for such automation, because all it does is unfold, intros, and apply. (It uses assumption, too, but that's just application of a hypothesis.)

Merely using auto, though, doesn't complete the proof.

The problem is the apply Hhoare with... part of the proof. Coq isn't able to figure out how to instantiate st without some help from us. Recall, though, that there are versions of many tactics that will use existential variables to make progress even when the regular versions of those tactics would get stuck. Here, the eapply tactic will introduce an existential variable ?st as a placeholder for st, and eassumption will instantiate ?st with st when it discovers st in assumption Heval. By using eapply we are essentially telling Coq, "Be patient: The missing part is going to be filled in later in the proof."

The eauto tactic will use eapply as part of its proof search. So, the entire proof can actually be done in just one line.

Of course, it's hard to predict that eauto suffices here without having gone through the original proof of hoare_consequence_pre to see the tactics it used. But now that we know eauto worked there, it's a good bet that it will also work for hoare_consequence_post.

We can also use eapply to streamline a proof (hoare_asgn_example1), that we did earlier as an example of using the consequence rule:

The final bullet of that proof also looks like a candidate for automation.

Now we have quite a nice proof script: it simply identifies the Hoare rules that need to be used and leaves the remaining low-level details up to Coq to figure out. By now it might be apparent that the entire proof could be automated if we added hoare_consequence_pre and hoare_asgn to the hint database. We won't do that in this chapter, so that we can get a better understanding of when and how the Hoare rules are used. In the next chapter, Hoare2, we'll dive deeper into automating entire proofs of Hoare triples. The other example of using consequence that we did earlier, hoare_asgn_example2, requires a little more work to automate. We can streamline the first line with eapply, but we can't just use auto for the final bullet, since it needs lia.

Let's introduce our own tactic to handle both that bullet and the bullet from example 1:

Again, we have quite a nice proof script. All the low-level details of proofs about assertions have been taken care of automatically. Of course, assertion_auto isn't able to prove everything we could possibly want to know about assertions -- there's no magic here! But it's good enough so far.

Exercise: 2 stars, standard (hoare_asgn_examples_2)

Prove these triples. Try to make your proof scripts nicely automated by following the examples above.

☐

Sequencing + Assignment

Here's an example of a program involving both sequencing and assignment. Note the use of hoare_seq in conjunction with hoare_consequence_pre and the eapply tactic.

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 c1 and c2: a = n X := a X = n ; <--- decoration for Q skip X = n We'll come back to the idea of decorated programs in much more detail in the next chapter.

Exercise: 2 stars, standard, especially useful (hoare_asgn_example4)

Translate this "decorated program" into a formal proof: True ->> 1 = 1 X := 1 X = 1 ->> X = 1 /\ 2 = 2 ; Y := 2 X = 1 /\ Y = 2 Note the use of "->>" decorations, each marking a use of hoare_consequence_pre. We've started you off by providing a use of hoare_seq that explicitly identifies X = 1 as the intermediate assertion.

☐

Exercise: 3 stars, standard (swap_exercise)

Write an Imp program c that swaps the values of X and Y and show that it satisfies the following specification: X <= Y c Y <= X Your proof should not need to use unfold valid_hoare_triple. Hints:

• Remember that Imp commands need to be enclosed in <{...}> brackets.
• Remember that the assignment rule works best when it's applied "back to front," from the postcondition to the precondition. So your proof will want to start at the end and work back to the beginning of your program.
• Remember that eapply is your friend.)

☐

Exercise: 4 stars, advanced (invalid_triple)

Show that a = n X := 3; Y := a Y = n is not a valid Hoare triple for some choices of a and n. Conceptual hint: Invent a particular a and n for which the triple in invalid, then use those to complete the proof. Technical hint: Hypothesis H below begins ∀ a n, .... You'll want to instantiate that with the particular a and n you've invented. You can do that with assert and apply, but you may remember (from Tactics.v in Logical Foundations) that Coq offers an even easier tactic: specialize. If you write specialize H with (a := your_a) (n := your_n) the hypothesis will be instantiated on your_a and your_n. Having chosen your a and n, proceed as follows:

• Use the (assumed) validity of the given hoare triple to derive a state st' in which Y has some value y1
• Use the evaluation rules (E_Seq and E_Asgn) to show that Y has a different value y2 in the same final state st'
• Since y1 and y2 are both equal to st' Y, they are equal to each other. But we chose them to be different, so this is a contradiction, which finishes the proof.

☐

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 if b then c1 else c2 Q However, this is rather weak. For example, using this rule, we cannot show True if X = 0 then Y := 2 else Y := X + 1 end X <= Y 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 c1 and c2 (i.e., the reasons why they establish the postcondition Q). P /\ b c1 Q P /\ ~ b c2 Q

---

(hoare_if) P if b then c1 else c2 end 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 bassertion b for the assertion "the boolean expression b evaluates to true (in the given state)."

A useful fact about bassertion:

We mentioned the congruence tactic in passing in Auto when building the find_rwd tactic. Like find_rwd, congruence is able to automatically find that both beval st b = false and beval st b = true are being assumed, notice the contradiction, and discriminate to complete the proof. Now we can formalize the Hoare proof rule for conditionals and prove it correct.

That is (unwrapping the notations): Theorem hoare_if : forall P Q b c1 c2, fun st => P st /\ bassertion b st c1 Q -> fun st => P st /\ ~ (bassertion b st) c2 Q -> P if b then c1 else c2 end Q.

Example

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

As we did earlier, it would be nice to eliminate all the low-level proof script that isn't about the Hoare rules. Unfortunately, the assertion_auto tactic we wrote wasn't quite up to the job. Looking at the proof of if_example, we can see why. We had to unfold a definition (bassertion) and use a theorem (eqb_eq) that we didn't need in earlier proofs. So, let's add those into our tactic, and clean it up a little in the process.

Now the proof is quite streamlined.

We can even shorten it a little bit more.

For later proofs, it will help to extend assertion_auto' to handle inequalities, too.

Exercise: 2 stars, standard (if_minus_plus)

Prove the theorem below using hoare_if. Do not use unfold valid_hoare_triple. The assertion_auto'' tactic we just defined may be useful.

☐

Exercise: One-sided conditionals

In this exercise we consider extending Imp with "one-sided conditionals" of the form if1 b then c end. 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 if1 b then c end does nothing. We recommend that you complete this exercise before attempting 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.)