Total correctness, Informally

Total correctness 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,
• then c terminates in some final state which satisfies the assertion Q.

Like for Hoare triples, assertion P is called the precondition, and Q is the postcondition. Notice that Total Correctness is a stronger claim than a Hoare triple since for total correctness we need to prove that the program c terminates and that the final state satisfies the post-condition, while for Hoare triples the post-condition only holds if the program terminates. This is why Hoare Triples are also called Partial correctness. Because single and double brackets are already used for other things, we'll write Total Correctness with vertical bars:
       |P| c |Q| For example, |X = 0| X := X + 1 |X = 1| is valid Total Correctness judgement, stating when executed in a state in which X = 0, command X := X + 1 terminates in a state with X = 1

Exercise: 1 star, standard, optional (total)

Paraphrase the following Total Correctness statement in English, and tell if there are valid -- i.e., is the claimed relation between P, c, and Q true?
   1) |True| c |X = 5|

   2) |X ≤ Y| c |Y ≤ X|

   3) |True| c |False|

   4) |False| skip |True|

   5) |True| while true do skip end |False|

   6) |X = 0|
        while X = 0 do X := X + 1 end
      |X = 1|

Total correctness, Formally

We can formalize valid Total Correctness in Coq as follows:

And add a notation for Total Correctness

We start by proving that Total Correctness is equivalent to having both a Hoare Triple {P} c {Q} and a proof that the program terminates under the assumption that the precondition P holds.

Proof Rules

The goal of Total Correctness is, like for Hoare Logic, to provide a compositional method for proving the validity of specific triples. 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. Most rules are close to the rules of Hoare Logic, differing only in notation. Only the rule for while will require some thinking and new concepts. This is to be expected, since the while instruction is the only instruction in the Imp language which can introduce non-termination.

Skip

Since skip doesn't change the state, it preserves any assertion P and is anyway terminating:

	(total_skip)
| P | skip | P |

Sequencing

If command c₁ is executed in a state where P holds and terminates in a state where Q holds, and command c₂ is execuetd in a state where Q holds and terminates in a state where R holds, then executing c₁ followed by c₂ in a state where P holds will terminate in a state where R holds:

| P | c1 | Q |
| Q | c2 | R |	(total_seq)
| P | c1;c2 | R |

Assignment

Since the evaluation of an expression and memory update always terminate, X:=a will always terminate. Moreover, like for Hoare Logic we can use the substitution operation for the the proof rule for assignment:

	(total_asgn)
| P[X ⊢> a] | X:= a | P |

Consequence

Like for Hoare Logic, we need for Total Correctness a rule that allows weakening the precondition and strengthening the postcondition.

|P'| c |Q'|
P ->> P     Q' ->> Q	(total_conseq)
|P| c |Q|

The proof of this rule is done in three steps. First, we prove the rule for weakening the preconditon. Second, we prove the rule for strengthening the postcondition. Lastly, we combine the two previous rules into one rule.

Conditionals

If command c₁ is executed in a state where P ∧ b holds and terminates in a state where Q holds, and, command c₂ is execuetd in a state where P ∧ ¬b holds and terminates in a state where Q holds, then executing the conditon in a state where P holds will terminate in a state where R holds:

|P /\ b| c1 |Q|
|P /\~b| c2 |Q|	(total_If)
|P| if b then c1 else c2 |Q|

While Loops

This is the hard case. In this rule, in addition to prove that the loop invariant is preseved by the loop body, one also proves that the loop terminates. To prove termination we will use a so called termination measure. The value m of the measure must strictly decreases with respect to a well-founded relation < on some domain set D during each iteration of the loop. Since < is well-founded, a strictly decreasing chain of members of D can have only finite length. Therefore, the loop cannot keep decreasing forever. Example of well-founded relation, is the usual order < on natural numbers N. However, the usual order < is not well-founded neither on the integers Z nor on positive real numbers R+. Using the measure m we can give a prove rule for the loop command of Imp. To keep track of the value of the measure in the initial state, we introduce a variable z and assign it to the mesure in the precondition. In the postcondition we ensure that the value of the measure in the resulting state satisfies the relation < with respect to the value of the measure in the initial state (z).

forall z, |P /\ b /\ z = m | c |P /\ m < z|	(total_while)
|P| while b do c end |P /\ ~b|

For simplicity, we will consider the domain of natural numbers and define the measure as a function from state to natural numbers.

The measure can be seen as a natural number we assign to a state at every iteration of the loop. If we make sure that this value strictly decreases with each iteration, we can be sure that the loop terminates i.e. the loop can only do a finate number of iteration. This means, that after a certain number of iteration the loop condition must be false. We will use this fact in the proof of correctness of the while rule by defining a unroll function which unroll the loop. By selecting the right number of unrolling we will be able to show that the loop condition will get false and thus the loop terminate, otherwise we have a contradition. The following definition of the unroll function may look not natural, but is convenient for proofs by induction.

We can prove certain properties of the unroll function that will be important for what follows. One of these properties is that if the loop body terminates, preserves the loop invariant P, and a measure decreases, then the command produced by unroll terminates and preserves the invariant P. In addition, after the command produced by unroll if the loop condition is true, the measure of the resulting state is smaller then the measure of the inital state minus the number of unrolling. This is very important for the proof by contradiction.

forall z, |P /\ b /\ z = m | c |P /\ m < z|
forall z, |P /\ m = z /\ b| unroll n b c |P /\ (b -> m <= z - n)|

We can define an auxiliary lemma aux that avoids making an assertion in the proof, and making the proof shorter.

A second property we want to show about the unroll function is stated in terms of the operational semantics: Adding the unroll function in front of a while loop with the same body and condition will not influence the resulting state:

Using the previous two lemmas, we can prove the Total Correctness rule for while. The proof is done in two steps:

• First, we use lemma hoare_total to split the proof in two parts. The first case is the Hoare rule for while, so we apply the lemma we proved in the previous chapter. It remains to prove that the loop terminates.
• To prove that the loop terminates, we use lemma unroll_while_while to add as many iterations of the loop as the value of measure. Then, we perform a case analysis on the last condition. If the condition is true, we have a contraction, since we have m < 0. If the condition is false, we apply lemma E_WhileFalse from the Imp chapter.

Examples

For the first formal proof using the total_while rule, we can prove the following example from the previous Chapter. The is increment location X while the location is small or equal to 2. We want to proof that if the program is executed in a state where X ≤ 3 holds then it terminates in a state where X = 3 holds. If the inital state satisfies X ≤ 3, the loop will require at most 3 iteration. Therefore the measure function will be (fun s ⇒ 3 - (s X)).

In the following example, we prove that the program computes the greatest common divisor and terminates. For the functional correctness part, we take a mathematical definition of gcd from the standard library as a reference implementation and proof that location Z contains the greatest common divisor of X and Y. For the termination part, we can notice that the number of iteration of the loop can be bounded by X + Y. This is an over-approximation of the maximum number of iteration of the loop, but has the advantage of being simple.