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

An assertion is a claim about the current state of memory. We will use assertions to write program specifications.

For example,

• fun st ⇒ st X = 3 holds if the value of X according to st is 3,
• fun st ⇒ True always holds, and
• fun st ⇒ False never holds.

Informally, instead of writing
      fun st ⇒ st X = m

we'll 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:

Our convention can be implemented uses Coq coercions and anotation scopes (much as we did with %imp in Imp) to automatically lift aexps, numbers, and Props into Assertions when they appear in the %assertion scope or when Coq knows the type of an expression is Assertion.

Lift functions to operate on assertion expressions.

Hoare Triples, Informally

A Hoare triple is a claim about the state before and after executing a command. A 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 in other ways 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 would transform a state in which X = 0 to a state in which X = 1.
• {{X = m}} X ::= X + 1 {{X = m + 1}}, is also a valid Hoare triple. It's even more descriptive of the exact behavior of that command than the previous example.

Hoare Triples, Formally

We can formalize Hoare triples and their notation in Coq as follows:

Exercise: 1 star, standard (hoare_post_true)

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

Exercise: 1 star, standard (hoare_pre_false)

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

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

How can we complete this triple?
       {{ ??? }} X ::= Y {{ X = 1 }}

One possibility is:
       {{ Y = 1 }} X ::= Y {{ X = 1 }}

The precondition is just the postcondition, but with X replaced by Y.

Another example:
       {{ ??? }} 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 "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 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 that idea of replacing occurrences: let Q [X ⊢> a] mean "Q where a is substituted for X". That yields the Hoare logic rule for assignment:
      {{ Q [X ⊢> a] }} X ::= a {{ Q }}

One way of reading that 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 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 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
    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.

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:
      {{X < 4}} X ::= X + 1 {{X < 5}}

We will see how to do so in the next section.