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

We'll use Coq's notation features to make assertions look as much like informal math as possible. For example, instead of writing
      fun st ⇒ st X = m we'll usually write just
      X = m

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.

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

Hoare Triples, Informally

A Hoare triple is a claim about the state before and after executing a command:
      {{P}} c {{Q}} This means:

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

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 and the command in the middle is a reference to the Coq variable m, which is bound outside the Hoare triple.

Hoare Triples, Formally

We can formalize valid Hoare triples in Coq as follows:

Proof Rules

Here's our plan:

• introduce one "proof rule" for each Imp syntactic form
• plus a couple of "structural rules" that help glue proofs together
• prove these rules correct in terms of the definition of valid_hoare_triple
• 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 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 }}

Assignment

How can we complete this triple?
       {{ ??? }} X := Y {{ X = 1 }} One natural possibility is:
       {{ Y = 1 }} X := Y {{ X = 1 }} The precondition is just the postcondition, but with X replaced by Y.

How about this one?
       {{ ??? }} X := X + Y {{ X = 1 }} Replace X with X + Y:
       {{ X + Y = 1 }} X := X + Y {{ X = 1 }} This works because "equals 1" holding of X is guaranteed by the property "equals 1" holding of whatever is being assigned to X.

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.

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:

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.

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.

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.

Here's a good candidate for automation:

Tactic eapply will find st for us.

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

...as can the proof for the postcondition consequence rule.

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.

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.

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 c₁ and c₂:
  {{ 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.

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.

Better:

{{P /\   b}} c1 {{Q}}
{{P /\ ~ b}} c2 {{Q}}	(hoare_if)
{{P}} if b then c1 else c2 end {{Q}}

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

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

That is (unwrapping the notations):
      Theorem hoare_if : ∀ P Q b c₁ c₂,
        {{fun st ⇒ P st ∧ bassertion b st}} c₁ {{Q}} →
        {{fun st ⇒ P st ∧ ¬(bassertion b st)}} c₂ {{Q}} →
        {{P}} if b then c₁ else c₂ end {{Q}}.

Example

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.

While Loops

The Hoare rule for while loops is based on the idea of a command invariant (or just invariant): an assertion whose truth is guaranteed after executing a command, assuming it is true before. That is, an assertion P is a command invariant of c if
      {{P}} c {{P}} holds. Note that the command invariant might temporarily become false in the middle of executing c, but by the end of c it must be restored.

The Hoare while rule combines the idea of a command invariant with information about when guard b does or does not hold.

{{P /\ b}} c {{P}}	(hoare_while)
{{P} while b do c end {{P /\ ~b}}

We call P a loop invariant of while b do c end if
      {{P ∧ b}} c {{P}} is a valid Hoare triple. This means that P will be true at the end of the loop body whenever the loop body executes. If P contradicts b, this holds trivially since the precondition is false. For instance, X = 0 is a loop invariant of
      while X = 2 do X := 1 end since the program will never enter the loop.

Summary

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}} if b then c1 else c2 end {{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}}

Our task in this chapter has been to define the rules of Hoare logic, and prove that the definitions are sound. Having done so, we can now work within Hoare logic to prove that particular programs satisfy particular Hoare triples. In the next chapter, we'll see how Hoare logic is can be used to prove that more interesting programs satisfy interesting specifications of their behavior. Crucially, we will do so without ever again unfolding the definition of Hoare triples -- i.e., we will take the rules of Hoare logic as a closed world for reasoning about programs.