# Hoare2Hoare Logic, Part II

On a piece of paper, write down a specification (as a Hoare triple) for the following program:
X ::= 2;;
Y ::= X + X

Write down a (useful) specification for the following program:
X ::= X + 1;; Y ::= X + 1

Write down a (useful) specification for the following program:
TEST X ≤ Y
THEN SKIP
ELSE
Z ::= X;;
X ::= Y;;
Y ::= Z
FI

Write down a (useful) specification for the following program:
X ::= m;;
Z ::= 0;;
WHILE ~(X = 0) DO
X ::= X - 2;;
Z ::= Z + 1
END

# Decorated Programs

The beauty of Hoare Logic is that it is compositional: the structure of proofs exactly follows the structure of programs.
This suggests that we can record the essential ideas of a proof (informally, and leaving out some low-level calculational details) by "decorating" a program with appropriate assertions on each of its commands.
Such a decorated program carries within it an argument for its own correctness.
For example, consider the program:
X ::= m;;
Z ::= p;
WHILE ~(X = 0) DO
Z ::= Z - 1;;
X ::= X - 1
END
(Note the parameters m and p, which stand for fixed-but-arbitrary numbers. Formally, they are simply Coq variables of type nat.) Here is one possible specification for this program:
{True }}
X ::= m;;
Z ::= p;
WHILE ~(X = 0) DO
Z ::= Z - 1;;
X ::= X - 1
END
{Z = p - m }}
Here is a decorated version of the program, embodying a proof of this specification:
{True }->>
{m = m }}
X ::= m;;
{X = m }->>
{X = m ∧ p = p }}
Z ::= p;
{X = m ∧ Z = p }->>
{Z - X = p - m }}
WHILE ~(X = 0) DO
{Z - X = p - m ∧ X ≠ 0 }->>
{{ (Z - 1) - (X - 1) = p - m }}
Z ::= Z - 1;;
{Z - (X - 1) = p - m }}
X ::= X - 1
{Z - X = p - m }}
END
{Z - X = p - m ∧ ¬(X ≠ 0) }->>
{Z = p - m }}
Concretely, a decorated program consists of the program text interleaved with assertions (either a single assertion or possibly two assertions separated by an implication).
To check that a decorated program represents a valid proof, we check that each individual command is locally consistent with its nearby assertions in the following sense:
• SKIP is locally consistent if its precondition and postcondition are the same:
{P }SKIP {P }}
• The sequential composition of c1 and c2 is locally consistent (with respect to assertions P and R) if c1 is locally consistent (with respect to P and Q) and c2 is locally consistent (with respect to Q and R):
{P }c1;; {Q }c2 {R }}
• An assignment is locally consistent if its precondition is the appropriate substitution of its postcondition:
{P [X > a}}
X ::= a
{P }}
• A conditional is locally consistent (with respect to assertions P and Q) if the assertions at the top of its "then" and "else" branches are exactly P b and P ¬b and if its "then" branch is locally consistent (with respect to P b and Q) and its "else" branch is locally consistent (with respect to P ¬b and Q):
{P }}
TEST b THEN
{P ∧ b }}
c1
{Q }}
ELSE
{P ∧ ¬b }}
c2
{Q }}
FI
{Q }}
• A while loop with precondition P is locally consistent if its postcondition is P ¬b, if the pre- and postconditions of its body are exactly P b and P, and if its body is locally consistent:
{P }}
WHILE b DO
{P ∧ b }}
c1
{P }}
END
{P ∧ ¬b }}
• A pair of assertions separated by ->> is locally consistent if the first implies the second:
{P }->>
{P' }}
This corresponds to the application of hoare_consequence, and it is the only place in a decorated program where checking whether decorations are correct is not fully mechanical and syntactic, but rather may involve logical and/or arithmetic reasoning.

## Example: Swapping Using Addition and Subtraction

Here is a program that swaps the values of two variables using addition and subtraction (instead of by assigning to a temporary variable).
X ::= X + Y;;
Y ::= X - Y;;
X ::= X - Y
We can prove (informally) using decorations that this program is correct — i.e., it always swaps the values of variables X and Y.
(* WORK IN CLASS *)

## Example: Simple Conditionals

Here's a simple program using conditionals, with a possible specification:
{True }}
TEST X ≤ Y THEN
Z ::= Y - X
ELSE
Z ::= X - Y
FI
{Z + X = Y ∨ Z + Y = X }}
Let's turn it into a decorated program...
(* WORK IN CLASS *)

## Example: Division

The following Imp program calculates the integer quotient and remainder of two numbers m and n that are arbitrary constants in the program.
X ::= m;;
Y ::= 0;;
WHILE n ≤ X DO
X ::= X - n;;
Y ::= Y + 1
END;
In we replace m and n by concrete numbers and execute the program, it will terminate with the variable X set to the remainder when m is divided by n and Y set to the quotient. Here's a possible specification:
{True }}
X ::= m;;
Y ::= 0;;
WHILE n ≤ X DO
X ::= X - n;;
Y ::= Y + 1
END
{n * Y + X = m ∧ X < n }}
(* WORK IN CLASS *)

# Finding Loop Invariants

Once the outer pre- and postcondition are chosen, the only creative part in verifying programs using Hoare Logic is finding the right loop invariants...

## Example: Slow Subtraction

The following program subtracts the value of X from the value of Y by repeatedly decrementing both X and Y. We want to verify its correctness with respect to the pre- and postconditions shown:
{X = m ∧ Y = n }}
WHILE ~(X = 0) DO
Y ::= Y - 1;;
X ::= X - 1
END
{Y = n - m }}
To verify this program, we need to find an invariant Inv for the loop. As a first step we can leave Inv as an unknown and build a skeleton for the proof by applying the rules for local consistency (working from the end of the program to the beginning, as usual, and without any thinking at all yet).
This leads to the following skeleton:
(1)      {X = m ∧ Y = n }}  ->>             (a)
(2)      {Inv }}
WHILE ~(X = 0) DO
(3)        {Inv ∧ X ≠ 0 }}  ->>              (c)
(4)        {Inv [X > X-1] [Y > Y-1] }}
Y ::= Y - 1;;
(5)        {Inv [X > X-1] }}
X ::= X - 1
(6)        {Inv }}
END
(7)      {Inv ∧ ¬(X ≠ 0) }}  ->>            (b)
(8)      {Y = n - m }}
By examining this skeleton, we can see that any valid Inv will have to respect three conditions:
• (a) it must be weak enough to be implied by the loop's precondition, i.e., (1) must imply (2);
• (b) it must be strong enough to imply the program's postcondition, i.e., (7) must imply (8);
• (c) it must be preserved by each iteration of the loop (given that the loop guard evaluates to true), i.e., (3) must imply (4).
(* WORK IN CLASS *)

## Example: Parity

Here is a cute little program for computing the parity of the value initially stored in X (due to Daniel Cristofani).
{X = m }}
WHILE 2 ≤ X DO
X ::= X - 2
END
{X = parity m }}
The mathematical parity function used in the specification is defined in Coq as follows:
Fixpoint parity x :=
match x with
| 0 ⇒ 0
| 1 ⇒ 1
| S (S x') ⇒ parity x'
end.

(* WORK IN CLASS *)

## Example: Finding Square Roots

The following program computes the (integer) square root of X by naive iteration:
{X=m }}
Z ::= 0;;
WHILE (Z+1)*(Z+1) ≤ X DO
Z ::= Z+1
END
{Z*Zm ∧ m<(Z+1)*(Z+1) }}
(* WORK IN CLASS *)

## Example: Squaring

Here is a program that squares X by repeated addition:
{X = m }}
Y ::= 0;;
Z ::= 0;;
WHILE ~(Y = X)  DO
Z ::= Z + X;;
Y ::= Y + 1
END
{Z = m*m }}
(* WORK IN CLASS *)

# Formal Decorated Programs

With a little more work, we can formalize the definition of well-formed decorated programs and mostly automate the mechanical steps when filling in decorations...

## Syntax

Decorated commands have contain additional assertions as postconditions, not preconditions.
The alternative—decorating every command with both a pre- and postcondition—would be too heavyweight. E.g., SKIP;; SKIP would become:
{{P}} ({{P}SKIP {{P}}) ;; ({{P}SKIP {{P}}) {{P}},
Inductive dcom : Type :=
| DCSkip : Assertiondcom
| DCSeq : dcomdcomdcom
| DCAsgn : stringaexpAssertiondcom
| DCIf : bexpAssertiondcomAssertiondcom
→ Assertiondcom
| DCWhile : bexpAssertiondcomAssertiondcom
| DCPre : Assertiondcomdcom
| DCPost : dcomAssertiondcom.
DCPre is used to provide the weakened precondition from the rule of consequence. To provide the initial precondition at the very top of the program, we use Decorated:
Inductive decorated : Type :=
| Decorated : Assertiondcomdecorated.
To avoid clashing with the existing Notation definitions for ordinary commands, we introduce these notations in a special scope called dcom_scope, and we Open this scope for the remainder of the file.
Delimit Scope default with default.

Notation "'SKIP' {{ P }}"
:= (DCSkip P)
(at level 10) : dcom_scope.
Notation "l '::=' a {{ P }}"
:= (DCAsgn l a P)
(at level 60, a at next level) : dcom_scope.
Notation "'WHILE' b 'DO' {{ Pbody }} d 'END' {{ Ppost }}"
:= (DCWhile b Pbody d Ppost)
(at level 80, right associativity) : dcom_scope.
Notation "'TEST' b 'THEN' {{ P }} d 'ELSE' {{ P' }} d' 'FI' {{ Q }}"
:= (DCIf b P d P' d' Q)
(at level 80, right associativity) : dcom_scope.
Notation "'->>' {{ P }} d"
:= (DCPre P d)
(at level 90, right associativity) : dcom_scope.
Notation "d '->>' {{ P }}"
:= (DCPost d P)
(at level 80, right associativity) : dcom_scope.
Notation " d ;; d' "
:= (DCSeq d d')
(at level 80, right associativity) : dcom_scope.
Notation "{{ P }} d"
:= (Decorated P d)
(at level 90) : dcom_scope.

Delimit Scope dcom_scope with dcom.
Open Scope dcom_scope.

Example dec0 :=
SKIP {{ fun stTrue }}.
Example dec1 :=
WHILE true DO {{ fun stTrue }} SKIP {{ fun stTrue }} END
{{ fun stTrue }}.
An example decorated program that decrements X to 0:
Example dec_while : decorated :=
{{ fun stTrue }}
WHILE ~(X = 0)
DO
{{ fun stTruest X ≠ 0}}
X ::= X - 1
{{ fun _True }}
END
{{ fun stTruest X = 0}} ->>
{{ fun stst X = 0 }}.
It is easy to go from a dcom to a com by erasing all annotations.
Fixpoint extract (d : dcom) : com :=
match d with
| DCSkip _SKIP
| DCSeq d1 d2 ⇒ (extract d1 ;; extract d2)
| DCAsgn X a _X ::= a
| DCIf b _ d1 _ d2 _TEST b THEN extract d1 ELSE extract d2 FI
| DCWhile b _ d _WHILE b DO extract d END
| DCPre _ dextract d
| DCPost d _extract d
end.

Definition extract_dec (dec : decorated) : com :=
match dec with
| Decorated P dextract d
end.

Print dec_while.
(*
dec_while =
{{fun _ : state => True}} (WHILE ~ X = 0
DO {{fun st : state => True /\ st X <> 0}
X ::= X - 1 {{fun _ : state => True}}
END {{fun st : state => True /\ st X = 0}}) ->>
{{fun st : state => st X = 0}}
: decorated
*)

Compute (extract_dec dec_while).
(*
= (WHILE ~ "X"%string = 0 DO "X" ::= "X"%string - 1 END)%imp
: com
*)

It is straightforward to extract the precondition and postcondition from a decorated program.
Fixpoint post (d : dcom) : Assertion :=
match d with
| DCSkip PP
| DCSeq d1 d2post d2
| DCAsgn X a QQ
| DCIf _ _ d1 _ d2 QQ
| DCWhile b Pbody c PpostPpost
| DCPre _ dpost d
| DCPost c QQ
end.

Definition pre_dec (dec : decorated) : Assertion :=
match dec with
| Decorated P dP
end.

Definition post_dec (dec : decorated) : Assertion :=
match dec with
| Decorated P dpost d
end.

Print dec_while.
(*
dec_while =
{{fun _ : state => True}} (WHILE ~ X = 0
DO {{fun st : state => True /\ st X <> 0}
X ::= X - 1 {{fun _ : state => True}}
END {{fun st : state => True /\ st X = 0}}) ->>
{{fun st : state => st X = 0}}
: decorated
*)

Compute pre_dec dec_while.
(*
= fun _ : state => True
: Assertion
*)

Compute post_dec dec_while.
(*
= fun x : state => x "X"%string = 0
: Assertion
*)

When is a decorated program correct?
Definition dec_correct (dec : decorated) :=
{{pre_dec dec}} (extract_dec dec) {{post_dec dec}}.

Example dec_while_triple_correct :
dec_correct dec_while
= {{ fun stTrue }}
(WHILE ~(X = 0) DO X ::= X - 1 END)%imp
{{ fun stst X = 0 }}.
Proof. reflexivity. Qed.
To check whether this Hoare triple is valid, we need a way to extract the "proof obligations" from a decorated program. These obligations are often called verification conditions, because they are the facts that must be verified to see that the decorations are logically consistent and thus constitute a proof of correctness.

## Extracting Verification Conditions

The function verification_conditions takes a dcom d together with a precondition P and returns a proposition that, if it can be proved, implies that the triple {{P}} (extract d) {{post d}} is valid.
Fixpoint verification_conditions (P : Assertion) (d : dcom) : Prop :=
match d with
| DCSkip Q
(P ->> Q)
| DCSeq d1 d2
verification_conditions P d1
∧ verification_conditions (post d1) d2
| DCAsgn X a Q
(P ->> Q [X > a])
| DCIf b P1 d1 P2 d2 Q
((fun stP stbassn b st) ->> P1)
∧ ((fun stP st ∧ ¬(bassn b st)) ->> P2)
∧ (post d1 ->> Q) ∧ (post d2 ->> Q)
∧ verification_conditions P1 d1
∧ verification_conditions P2 d2
| DCWhile b Pbody d Ppost
(* post d is the loop invariant and the initial
precondition *)

(P ->> post d)
∧ ((fun stpost d stbassn b st) ->> Pbody)
∧ ((fun stpost d st ∧ ~(bassn b st)) ->> Ppost)
∧ verification_conditions Pbody d
| DCPre P' d
(P ->> P') ∧ verification_conditions P' d
| DCPost d Q
verification_conditions P d ∧ (post d ->> Q)
end.
And now the key theorem, stating that verification_conditions does its job correctly. Not surprisingly, we need to use each of the Hoare Logic rules at some point in the proof.
Theorem verification_correct : d P,
verification_conditions P d{{P}} (extract d) {{post d}}.
Proof.
induction d; intros P H; simpl in *.
- (* Skip *)
eapply hoare_consequence_pre.
apply hoare_skip.
assumption.
- (* Seq *)
destruct H as [H1 H2].
eapply hoare_seq.
apply IHd2. apply H2.
apply IHd1. apply H1.
- (* Asgn *)
eapply hoare_consequence_pre.
apply hoare_asgn.
assumption.
- (* If *)
destruct H as [HPre1 [HPre2 [Hd1 [Hd2 [HThen HElse]]]]].
apply IHd1 in HThen. clear IHd1.
apply IHd2 in HElse. clear IHd2.
apply hoare_if.
+ eapply hoare_consequence_post with (Q':=post d1); eauto.
eapply hoare_consequence_pre; eauto.
+ eapply hoare_consequence_post with (Q':=post d2); eauto.
eapply hoare_consequence_pre; eauto.
- (* While *)
destruct H as [Hpre [Hbody1 [Hpost1 Hd]]].
eapply hoare_consequence_pre; eauto.
eapply hoare_consequence_post; eauto.
apply hoare_while.
eapply hoare_consequence_pre; eauto.
- (* Pre *)
destruct H as [HP Hd].
eapply hoare_consequence_pre. apply IHd. apply Hd. assumption.
- (* Post *)
destruct H as [Hd HQ].
eapply hoare_consequence_post. apply IHd. apply Hd. assumption.
Qed.
Now that all the pieces are in place, we can verify an entire program.
Definition verification_conditions_dec (dec : decorated) : Prop :=
match dec with
| Decorated P dverification_conditions P d
end.

Corollary verification_correct_dec : dec,
verification_conditions_dec decdec_correct dec.
Proof.
intros [P d]. apply verification_correct.
Qed.
The propositions generated by verification_conditions are fairly big, and they contain many conjuncts that are essentially trivial.
Eval simpl in (verification_conditions_dec dec_while).
===>
(((fun _ : state ⇒ True->> (fun _ : state ⇒ True)) ∧
((fun st : state ⇒ True ∧ bassn (~(X = 0)) st->>
(fun st : state ⇒ True ∧ st X ≠ 0)) ∧
((fun st : state ⇒ True ∧ ¬bassn (~(X = 0)) st->>
(fun st : state ⇒ True ∧ st X = 0)) ∧
(fun st : state ⇒ True ∧ st X ≠ 0) ->>
(fun _ : state ⇒ True) [X > X - 1]) ∧
(fun st : state ⇒ True ∧ st X = 0) ->>
(fun st : state ⇒ st X = 0)

## Automation

Automation to the rescue!
Tactic Notation "verify" :=
apply verification_correct;
repeat split;
simpl; unfold assert_implies;
unfold bassn in *; unfold beval in *; unfold aeval in *;
unfold assn_sub; intros;
repeat rewrite t_update_eq;
repeat (rewrite t_update_neq; [| (intro X; inversion X)]);
simpl in *;
repeat match goal with [H : ___] ⇒ destruct H end;
repeat rewrite not_true_iff_false in *;
repeat rewrite not_false_iff_true in *;
repeat rewrite negb_true_iff in *;
repeat rewrite negb_false_iff in *;
repeat rewrite eqb_eq in *;
repeat rewrite eqb_neq in *;
repeat rewrite leb_iff in *;
repeat rewrite leb_iff_conv in *;
try subst;
repeat
match goal with
[st : state_] ⇒
match goal with
[H : st _ = __] ⇒ rewriteH in *; clear H
| [H : _ = st __] ⇒ rewrite <- H in *; clear H
end
end;
try eauto; try omega.
What's left after verify does its thing is "just the interesting parts" of checking that the decorations are correct. For very simple examples, verify sometimes even immediately solves the goal (provided that the annotations are correct!).
Theorem dec_while_correct :
dec_correct dec_while.
Proof. verify. Qed.

## Examples

In this section, we use the automation developed above to verify formal decorated programs corresponding to most of the informal ones we have seen.

### Slow Subtraction

Example subtract_slowly_dec (m : nat) (p : nat) : decorated :=
{{ fun stst X = mst Z = p }} ->>
{{ fun stst Z - st X = p - m }}
WHILE ~(X = 0)
DO {{ fun stst Z - st X = p - mst X ≠ 0 }} ->>
{{ fun st ⇒ (st Z - 1) - (st X - 1) = p - m }}
Z ::= Z - 1
{{ fun stst Z - (st X - 1) = p - m }} ;;
X ::= X - 1
{{ fun stst Z - st X = p - m }}
END
{{ fun stst Z - st X = p - mst X = 0 }} ->>
{{ fun stst Z = p - m }}.

Theorem subtract_slowly_dec_correct : m p,
dec_correct (subtract_slowly_dec m p).
Proof. intros m p. verify. (* this grinds for a bit! *) Qed.

### Swapping Using Addition and Subtraction

Definition swap : com :=
X ::= X + Y;;
Y ::= X - Y;;
X ::= X - Y.

Definition swap_dec m n : decorated :=
{{ fun stst X = mst Y = n}} ->>
{{ fun st ⇒ (st X + st Y) - ((st X + st Y) - st Y) = n
∧ (st X + st Y) - st Y = m }}
X ::= X + Y
{{ fun stst X - (st X - st Y) = nst X - st Y = m }};;
Y ::= X - Y
{{ fun stst X - st Y = nst Y = m }};;
X ::= X - Y
{{ fun stst X = nst Y = m}}.

Theorem swap_correct : m n,
dec_correct (swap_dec m n).
Proof. intros; verify. Qed.
See the full version of the chapter for the rest...