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)

We've dealt with a few sorts of properties of Imp programs:

• Termination
• Nontermination
• Equivalence

Overview of this chapter... Topic:

• A systematic method for reasoning about the functional correctness of programs in Imp

Goals:

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

Plan:

• specifications (assertions / Hoare triples)
• proof rules
• loop invariants
• decorated programs
• 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, if, whenever P holds in some state st, Q also holds.

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

Hoare Triples

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 assertion 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:

To get us warmed up for what's coming, here are two simple facts about Hoare triples. (Make sure you understand what they mean.)

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: 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, to conclude that an arbitrary assertion 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", which we refer to as assertion substitution, or assn_sub. 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 P' should mention a wherever P mentions X.

Since P is an arbitrary Coq assertion, 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.

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 finally 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, using the concept of substitution, 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 would be even more helpful is to prove this simpler triple: 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, 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...

We can also use it to prove the example mentioned earlier. Or, formally ...

Finally, for convenience in proofs, here is a combined rule of consequence that allows us to vary both the precondition and the postcondition in one go.

{{P'}} c {{Q'}}
P ->> P'
Q' ->> Q	(hoare_consequence)
{{P}} c {{Q}}

Skip

Since SKIP doesn't change the state, it preserves any assertion 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 }}

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.

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

Better:

{{P ∧   b}} c1 {{Q}}
{{P ∧ ¬b}} c2 {{Q}}	(hoare_if)
{{P}} TEST 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.

Example

Recap

Idea: create a domain specific logic for reasoning about properties of Imp programs.

• This hides the low-level details of the semantics of the program
• Leads to a compositional reasoning process

The basic structure is given by Hoare triples of the form:

• P and Q are assertions about the state of the Imp program.
• "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."

The rules of Hoare Logic (so far):

	(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}} TEST b THEN c1 ELSE c2 FI {{Q}}

{{P'}} c {{Q'}}
P ->> P'
Q' ->> Q	(hoare_consequence)
{{P}} c {{Q}}

Loops

Suppose we have a loop and we want to find a precondition P and a postcondition Q such that is a valid triple.

If b is false, then the loop is like SKIP: 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: But, as with if, we also know ¬ b in the postcondition:

What about when b is true? First attempt:

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

We know that b is true in the precondition of c. And this leads us to 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 importantly) 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...