# Hoare2Hoare Logic, Part II

Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".

From Coq Require Import Strings.String.

From PLF Require Import Maps.

From Coq Require Import Bool.Bool.

From Coq Require Import Arith.Arith.

From Coq Require Import Arith.EqNat.

From Coq Require Import Arith.PeanoNat. Import Nat.

From Coq Require Import Lia.

From PLF Require Export Imp.

From PLF Require Import Hoare.

Definition FILL_IN_HERE := <{True}>.

From Coq Require Import Strings.String.

From PLF Require Import Maps.

From Coq Require Import Bool.Bool.

From Coq Require Import Arith.Arith.

From Coq Require Import Arith.EqNat.

From Coq Require Import Arith.PeanoNat. Import Nat.

From Coq Require Import Lia.

From PLF Require Export Imp.

From PLF Require Import Hoare.

Definition FILL_IN_HERE := <{True}>.

# Decorated Programs

*structure-guided*: the structure of proofs exactly follows the structure of programs.

*decorated program*carries within itself an argument for its own correctness.

X := m;

Z := p;

while X ≠ 0 do

Z := Z - 1;

X := X - 1

end Here is one possible specification for this program, in the form of a Hoare triple:

{{ True }}

X := m;

Z := p;

while X ≠ 0 do

Z := Z - 1;

X := X - 1

end

{{ Z = p - m }} (Note the

*parameters*m and p, which stand for fixed-but-arbitrary numbers. Formally, they are simply Coq variables of type nat.)

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

*find*a proof for a given specification, and for this we need to discover the right assertions. This can be done in an almost mechanical way, with the exception of finding loop invariants. In the remainder of this section we explain in detail how to construct decorations for several short programs, all of which are loop-free or have simple loop invariants. We'll return finding more interesting loop invariants later in the chapter.

## Example: Swapping

X := X + Y;

Y := X - Y;

X := X - Y We can give a proof, in the form of decorations, that this program is correct -- i.e., it really swaps X and Y -- as follows.

(1) {{ X = m ∧ Y = n }} ->>

(2) {{ (X + Y) - ((X + Y) - Y) = n ∧ (X + Y) - Y = m }}

X := X + Y

(3) {{ X - (X - Y) = n ∧ X - Y = m }};

Y := X - Y

(4) {{ X - Y = n ∧ Y = m }};

X := X - Y

(5) {{ X = n ∧ Y = m }}

- We begin with the undecorated program (the unnumbered lines).
- We add the specification -- i.e., the outer precondition (1)
and postcondition (5). In the precondition, we use parameters
m and n to remember the initial values of variables X
and Y so that we can refer to them in the postcondition (5).
- We work backwards, mechanically, starting from (5) and proceeding until we get to (2). At each step, we obtain the precondition of the assignment from its postcondition by substituting the assigned variable with the right-hand-side of the assignment. For instance, we obtain (4) by substituting X with X - Y in (5), and we obtain (3) by substituting Y with X - Y in (4).

## Example: Simple Conditionals

(1) {{ True }}

if X ≤ Y then

(2) {{ True ∧ X ≤ Y }} ->>

(3) {{ (Y - X) + X = Y ∨ (Y - X) + Y = X }}

Z := Y - X

(4) {{ Z + X = Y ∨ Z + Y = X }}

else

(5) {{ True ∧ ~(X ≤ Y) }} ->>

(6) {{ (X - Y) + X = Y ∨ (X - Y) + Y = X }}

Z := X - Y

(7) {{ Z + X = Y ∨ Z + Y = X }}

end

(8) {{ Z + X = Y ∨ Z + Y = X }} These decorations can be constructed as follows:

- We start with the outer precondition (1) and postcondition (8).
- Following the format dictated by the hoare_if rule, we copy the
postcondition (8) to (4) and (7). We conjoin the precondition (1)
with the guard of the conditional to obtain (2). We conjoin (1)
with the negated guard of the conditional to obtain (5).
- In order to use the assignment rule and obtain (3), we substitute
Z by Y - X in (4). To obtain (6) we substitute Z by X - Y
in (7).
- Finally, we verify that (2) implies (3) and (5) implies (6). Both
of these implications crucially depend on the ordering of X and
Y obtained from the guard. For instance, knowing that X ≤ Y
ensures that subtracting X from Y and then adding back X
produces Y, as required by the first disjunct of (3). Similarly,
knowing that ¬ (X ≤ Y) ensures that subtracting Y from X
and then adding back Y produces X, as needed by the second
disjunct of (6). Note that n - m + m = n does
*not*hold for arbitrary natural numbers n and m (for example, 3 - 5 + 5 = 5).

#### Exercise: 2 stars, standard, optional (if_minus_plus_reloaded)

N.b.: Although this exercise is marked optional, it is an excellent warm-up for the (non-optional) if_minus_plus_correct exercise below!
(*

{{ True }}

if X <= Y then

{{ }} ->>

{{ }}

Z := Y - X

{{ }}

else

{{ }} ->>

{{ }}

Y := X + Z

{{ }}

end

{{ Y = X + Z }}

*)

{{ True }}

if X <= Y then

{{ }} ->>

{{ }}

Z := Y - X

{{ }}

else

{{ }} ->>

{{ }}

Y := X + Z

{{ }}

end

{{ Y = X + Z }}

*)

Briefly justify each use of ->>.
☐

## Example: Reduce to Zero

(1) {{ True }}

while X ≠ 0 do

(2) {{ True ∧ X ≠ 0 }} ->>

(3) {{ True }}

X := X - 1

(4) {{ True }}

end

(5) {{ True ∧ ~(X ≠ 0) }} ->>

(6) {{ X = 0 }} The decorations can be constructed as follows:

- Start with the outer precondition (1) and postcondition (6).
- Following the format dictated by the hoare_while rule, we copy
(1) to (4). We conjoin (1) with the guard to obtain (2). We also
conjoin (1) with the negation of the guard to obtain (5).
- Because the final postcondition (6) does not syntactically match (5),
we add an implication between them.
- Using the assignment rule with assertion (4), we trivially substitute
and obtain assertion (3).
- We add the implication between (2) and (3).

## Example: Division

X := m;

Y := 0;

while n ≤ X do

X := X - n;

Y := Y + 1

end; If 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.

(1) {{ True }} ->>

(2) {{ n × 0 + m = m }}

X := m;

(3) {{ n × 0 + X = m }}

Y := 0;

(4) {{ n × Y + X = m }}

while n ≤ X do

(5) {{ n × Y + X = m ∧ n ≤ X }} ->>

(6) {{ n × (Y + 1) + (X - n) = m }}

X := X - n;

(7) {{ n × (Y + 1) + X = m }}

Y := Y + 1

(8) {{ n × Y + X = m }}

end

(9) {{ n × Y + X = m ∧ ¬(n ≤ X) }} ->>

(10) {{ n × Y + X = m ∧ X < n }} Assertions (4), (5), (8), and (9) are derived mechanically from the invariant and the loop's guard. Assertions (8), (7), and (6) are derived using the assignment rule going backwards from (8) to (6). Assertions (4), (3), and (2) are again backwards applications of the assignment rule.

- (1) ->> (2): trivial, by algebra.
- (5) ->> (6): because n ≤ X, we are guaranteed that the subtraction in (6) does not get zero-truncated. We can therefore rewrite (6) as n × Y + n + X - n and cancel the ns, which results in the left conjunct of (5).
- (9) ->> (10): if ¬ (n ≤ X) then X < n. That's straightforward from high-school algebra.

## From Decorated Programs to Formal Proofs

*not*unfold the definition of hoare_triple anywhere in this proof: the point of the game is to use the Hoare rules as a self-contained logic for reasoning about programs.

Definition reduce_to_zero' : com :=

<{ while X ≠ 0 do

X := X - 1

end }>.

Theorem reduce_to_zero_correct' :

{{True}}

reduce_to_zero'

{{X = 0}}.

Proof.

unfold reduce_to_zero'.

(* First we need to transform the postcondition so

that hoare_while will apply. *)

eapply hoare_consequence_post.

- apply hoare_while.

+ (* Loop body preserves invariant *)

(* Massage precondition so hoare_asgn applies *)

eapply hoare_consequence_pre.

× apply hoare_asgn.

× (* Proving trivial implication (2) ->> (3) *)

unfold assn_sub, "->>". simpl. intros.

exact I.

- (* Invariant and negated guard imply post *)

intros st [Inv GuardFalse].

unfold bassn in GuardFalse. simpl in GuardFalse.

rewrite not_true_iff_false in GuardFalse.

rewrite negb_false_iff in GuardFalse.

apply eqb_eq in GuardFalse.

apply GuardFalse.

Qed.

<{ while X ≠ 0 do

X := X - 1

end }>.

Theorem reduce_to_zero_correct' :

{{True}}

reduce_to_zero'

{{X = 0}}.

Proof.

unfold reduce_to_zero'.

(* First we need to transform the postcondition so

that hoare_while will apply. *)

eapply hoare_consequence_post.

- apply hoare_while.

+ (* Loop body preserves invariant *)

(* Massage precondition so hoare_asgn applies *)

eapply hoare_consequence_pre.

× apply hoare_asgn.

× (* Proving trivial implication (2) ->> (3) *)

unfold assn_sub, "->>". simpl. intros.

exact I.

- (* Invariant and negated guard imply post *)

intros st [Inv GuardFalse].

unfold bassn in GuardFalse. simpl in GuardFalse.

rewrite not_true_iff_false in GuardFalse.

rewrite negb_false_iff in GuardFalse.

apply eqb_eq in GuardFalse.

apply GuardFalse.

Qed.

In Hoare we introduced a series of tactics named
assn_auto to automate proofs involving assertions.
The following declaration introduces a more sophisticated tactic
that will help with proving assertions throughout the rest of this
chapter. You don't need to understand the details, but briefly:
it uses split repeatedly to turn all the conjunctions into
separate subgoals, tries to use several theorems about booleans
and (in)equalities, then uses eauto and lia to finish off as
many subgoals as possible. What's left after verify_assn does
its thing should be just the "interesting parts" of the proof --
which, if we're lucky, might be nothing at all!

Ltac verify_assn :=

repeat split;

simpl;

unfold assert_implies;

unfold ap in *; unfold ap

unfold bassn in *; unfold beval in *; unfold aeval in *;

unfold assn_sub; intros;

repeat (simpl in *;

rewrite t_update_eq ||

(try rewrite t_update_neq;

[| (intro X; inversion X; fail)]));

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;

simpl in *;

repeat

match goal with

[st : state ⊢ _] ⇒

match goal with

| [H : st _ = _ ⊢ _] ⇒

rewrite → H in *; clear H

| [H : _ = st _ ⊢ _] ⇒

rewrite <- H in *; clear H

end

end;

try eauto;

try lia.

repeat split;

simpl;

unfold assert_implies;

unfold ap in *; unfold ap

_{2}in *;unfold bassn in *; unfold beval in *; unfold aeval in *;

unfold assn_sub; intros;

repeat (simpl in *;

rewrite t_update_eq ||

(try rewrite t_update_neq;

[| (intro X; inversion X; fail)]));

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;

simpl in *;

repeat

match goal with

[st : state ⊢ _] ⇒

match goal with

| [H : st _ = _ ⊢ _] ⇒

rewrite → H in *; clear H

| [H : _ = st _ ⊢ _] ⇒

rewrite <- H in *; clear H

end

end;

try eauto;

try lia.

This makes it pretty easy to verify reduce_to_zero':

Theorem reduce_to_zero_correct''' :

{{True}}

reduce_to_zero'

{{X = 0}}.

Proof.

unfold reduce_to_zero'.

eapply hoare_consequence_post.

- apply hoare_while.

+ eapply hoare_consequence_pre.

× apply hoare_asgn.

× verify_assn.

- verify_assn.

Qed.

{{True}}

reduce_to_zero'

{{X = 0}}.

Proof.

unfold reduce_to_zero'.

eapply hoare_consequence_post.

- apply hoare_while.

+ eapply hoare_consequence_pre.

× apply hoare_asgn.

× verify_assn.

- verify_assn.

Qed.

This example shows that it is conceptually straightforward to read
off the main elements of a formal proof from a decorated program.
Indeed, the process is so straightforward that it can be
automated, as we show next.

# Formal Decorated Programs

## Syntax

*decorated commands*, or dcoms.

{{P}} ({{P}} skip {{P}}) ; ({{P}} skip {{P}}) {{P}} with pre- and post-conditions around each skip, plus identical pre- and post-conditions on the semicolon!

- The skip command is decorated only with its postcondition

skip {{ Q }} on the assumption that the precondition will be provided by the context.

- Sequences d
_{1}; d_{2}need no additional decorations._{2}there will be a postcondition; this serves as the postcondition of d_{1};d_{2}. Inside d_{1}there will also be a postcondition, which additionally serves as the precondition for d_{2}.

- An assignment X := a is decorated only with its postcondition:

X := a {{ Q }}

- A conditional if b then d
_{1}else d_{2}is decorated with a postcondition for the entire statement, as well as preconditions for each branch:

if b then {{ P_{1}}} d_{1}else {{ P_{2}}} d_{2}end {{ Q }}

- A loop while b do d end is decorated with its postcondition
and a precondition for the body:

while b do {{ P }} d end {{ Q }} The postcondition embedded in d serves as the loop invariant.

- Implications ->> can be added as decorations either for a
precondition

->> {{ P }} d or for a postcondition

d ->> {{ Q }} The former is waiting for another precondition to eventually be supplied (e.g., {{ P'}} ->> {{ P }} d); the latter relies on the postcondition already embedded in d.

Inductive dcom : Type :=

| DCSkip (Q : Assertion)

(* skip {{ Q }} *)

| DCSeq (d

(* d

| DCAsgn (X : string) (a : aexp) (Q : Assertion)

(* X := a {{ Q }} *)

| DCIf (b : bexp) (P

(P

(* if b then {{ P

| DCWhile (b : bexp) (P : Assertion) (d : dcom)

(Q : Assertion)

(* while b do {{ P }} d end {{ Q }} *)

| DCPre (P : Assertion) (d : dcom)

(* ->> {{ P }} d *)

| DCPost (d : dcom) (Q : Assertion)

(* d ->> {{ Q }} *).

| DCSkip (Q : Assertion)

(* skip {{ Q }} *)

| DCSeq (d

_{1}d_{2}: dcom)(* d

_{1}; d_{2}*)| DCAsgn (X : string) (a : aexp) (Q : Assertion)

(* X := a {{ Q }} *)

| DCIf (b : bexp) (P

_{1}: Assertion) (d_{1}: dcom)(P

_{2}: Assertion) (d_{2}: dcom) (Q : Assertion)(* if b then {{ P

_{1}}} d_{1}else {{ P_{2}}} d_{2}end {{ Q }} *)| DCWhile (b : bexp) (P : Assertion) (d : dcom)

(Q : Assertion)

(* while b do {{ P }} d end {{ Q }} *)

| DCPre (P : Assertion) (d : dcom)

(* ->> {{ P }} d *)

| DCPost (d : dcom) (Q : Assertion)

(* d ->> {{ Q }} *).

To provide the initial precondition that goes at the very top of a
decorated program, we introduce a new type decorated:

To avoid clashing with the existing Notations for ordinary
commands, we introduce these notations in a new grammar scope
called dcom.

Declare Scope dcom_scope.

Notation "'skip' {{ P }}"

:= (DCSkip P)

(in custom com at level 0, P constr) : dcom_scope.

Notation "l ':=' a {{ P }}"

:= (DCAsgn l a P)

(in custom com at level 0, l constr at level 0,

a custom com at level 85, P constr, no associativity) : dcom_scope.

Notation "'while' b 'do' {{ Pbody }} d 'end' {{ Ppost }}"

:= (DCWhile b Pbody d Ppost)

(in custom com at level 89, b custom com at level 99,

Pbody constr, Ppost constr) : dcom_scope.

Notation "'if' b 'then' {{ P }} d 'else' {{ P' }} d' 'end' {{ Q }}"

:= (DCIf b P d P' d' Q)

(in custom com at level 89, b custom com at level 99,

P constr, P' constr, Q constr) : dcom_scope.

Notation "'->>' {{ P }} d"

:= (DCPre P d)

(in custom com at level 12, right associativity, P constr) : dcom_scope.

Notation "d '->>' {{ P }}"

:= (DCPost d P)

(in custom com at level 10, right associativity, P constr) : dcom_scope.

Notation " d ; d' "

:= (DCSeq d d')

(in custom com at level 90, right associativity) : dcom_scope.

Notation "{{ P }} d"

:= (Decorated P d)

(in custom com at level 91, P constr) : dcom_scope.

Local Open Scope dcom_scope.

Example dec0 :=

<{ skip {{ True }} }>.

Example dec1 :=

<{ while true do {{ True }} skip {{ True }} end

{{ True }} }>.

Notation "'skip' {{ P }}"

:= (DCSkip P)

(in custom com at level 0, P constr) : dcom_scope.

Notation "l ':=' a {{ P }}"

:= (DCAsgn l a P)

(in custom com at level 0, l constr at level 0,

a custom com at level 85, P constr, no associativity) : dcom_scope.

Notation "'while' b 'do' {{ Pbody }} d 'end' {{ Ppost }}"

:= (DCWhile b Pbody d Ppost)

(in custom com at level 89, b custom com at level 99,

Pbody constr, Ppost constr) : dcom_scope.

Notation "'if' b 'then' {{ P }} d 'else' {{ P' }} d' 'end' {{ Q }}"

:= (DCIf b P d P' d' Q)

(in custom com at level 89, b custom com at level 99,

P constr, P' constr, Q constr) : dcom_scope.

Notation "'->>' {{ P }} d"

:= (DCPre P d)

(in custom com at level 12, right associativity, P constr) : dcom_scope.

Notation "d '->>' {{ P }}"

:= (DCPost d P)

(in custom com at level 10, right associativity, P constr) : dcom_scope.

Notation " d ; d' "

:= (DCSeq d d')

(in custom com at level 90, right associativity) : dcom_scope.

Notation "{{ P }} d"

:= (Decorated P d)

(in custom com at level 91, P constr) : dcom_scope.

Local Open Scope dcom_scope.

Example dec0 :=

<{ skip {{ True }} }>.

Example dec1 :=

<{ while true do {{ True }} skip {{ True }} end

{{ True }} }>.

Recall that you can Set Printing All to see how all that
notation is desugared.

An example decorated program that decrements X to 0:

Example dec_while : decorated :=

<{

{{ True }}

while X ≠ 0

do

{{ True ∧ (X ≠ 0) }}

X := X - 1

{{ True }}

end

{{ True ∧ X = 0}} ->>

{{ X = 0 }} }>.

<{

{{ True }}

while X ≠ 0

do

{{ True ∧ (X ≠ 0) }}

X := X - 1

{{ True }}

end

{{ True ∧ X = 0}} ->>

{{ 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 _ ⇒ CSkip

| DCSeq d

| DCAsgn X a _ ⇒ CAsgn X a

| DCIf b _ d

| DCWhile b _ d _ ⇒ CWhile b (extract d)

| DCPre _ d ⇒ extract d

| DCPost d _ ⇒ extract d

end.

Definition extract_dec (dec : decorated) : com :=

match dec with

| Decorated P d ⇒ extract d

end.

Example extract_while_ex :

extract_dec dec_while

= <{while X ≠ 0 do X := X - 1 end}>.

Proof.

unfold dec_while.

reflexivity.

Qed.

match d with

| DCSkip _ ⇒ CSkip

| DCSeq d

_{1}d_{2}⇒ CSeq (extract d_{1}) (extract d_{2})| DCAsgn X a _ ⇒ CAsgn X a

| DCIf b _ d

_{1}_ d_{2}_ ⇒ CIf b (extract d_{1}) (extract d_{2})| DCWhile b _ d _ ⇒ CWhile b (extract d)

| DCPre _ d ⇒ extract d

| DCPost d _ ⇒ extract d

end.

Definition extract_dec (dec : decorated) : com :=

match dec with

| Decorated P d ⇒ extract d

end.

Example extract_while_ex :

extract_dec dec_while

= <{while X ≠ 0 do X := X - 1 end}>.

Proof.

unfold dec_while.

reflexivity.

Qed.

It is also straightforward to extract the precondition and
postcondition from a decorated program.

Definition pre_dec (dec : decorated) : Assertion :=

match dec with

| Decorated P d ⇒ P

end.

Fixpoint post (d : dcom) : Assertion :=

match d with

| DCSkip P ⇒ P

| DCSeq _ d

| DCAsgn _ _ Q ⇒ Q

| DCIf _ _ _ _ _ Q ⇒ Q

| DCWhile _ _ _ Q ⇒ Q

| DCPre _ d ⇒ post d

| DCPost _ Q ⇒ Q

end.

Definition post_dec (dec : decorated) : Assertion :=

match dec with

| Decorated P d ⇒ post d

end.

Example pre_dec_while : pre_dec dec_while = True.

Proof. reflexivity. Qed.

Example post_dec_while : post_dec dec_while = (X = 0)%assertion.

Proof. reflexivity. Qed.

match dec with

| Decorated P d ⇒ P

end.

Fixpoint post (d : dcom) : Assertion :=

match d with

| DCSkip P ⇒ P

| DCSeq _ d

_{2}⇒ post d_{2}| DCAsgn _ _ Q ⇒ Q

| DCIf _ _ _ _ _ Q ⇒ Q

| DCWhile _ _ _ Q ⇒ Q

| DCPre _ d ⇒ post d

| DCPost _ Q ⇒ Q

end.

Definition post_dec (dec : decorated) : Assertion :=

match dec with

| Decorated P d ⇒ post d

end.

Example pre_dec_while : pre_dec dec_while = True.

Proof. reflexivity. Qed.

Example post_dec_while : post_dec dec_while = (X = 0)%assertion.

Proof. reflexivity. Qed.

We can then express what it means for a decorated program to
be correct as follows:

Definition outer_triple_valid (dec : decorated) :=

{{pre_dec dec}} extract_dec dec {{post_dec dec}}.

Example dec_while_triple_correct :

outer_triple_valid dec_while

=

{{ True }}

while X ≠ 0 do X := X - 1 end

{{ X = 0 }}.

{{pre_dec dec}} extract_dec dec {{post_dec dec}}.

Example dec_while_triple_correct :

outer_triple_valid dec_while

=

{{ True }}

while X ≠ 0 do X := X - 1 end

{{ X = 0 }}.

Proof. reflexivity. Qed.

Remember that the outer Hoare triple of a decorated program is
just a Prop; thus, to show that it is
We will do this by extracting "proof obligations" from the
decorations sprinkled through the program.
These obligations are often called
The function verification_conditions takes a decorated command
d together with a precondition P and returns a

{{P}} (extract d) {{post d}} is valid.
It does this by walking over d and generating a big conjunction
that includes

*valid*, we need to produce a proof of this proposition.*verification conditions*, because they are the facts that must be verified to see that the decorations are locally consistent and thus constitute a proof of correctness.## Extracting Verification Conditions

*proposition*that, if it can be proved, implies that the triple{{P}} (extract d) {{post d}} is valid.

- local consistency checks for each form of command, plus
- uses of ->> to bridge the gap between the assertions found inside a decorated command and the assertions imposed by its context; these uses correspond to applications of the consequence rule.

- The decorated command

skip {{Q}} is locally consistent with respect to a precondition P if P ->> Q.

- The sequential composition of d
_{1}and d_{2}is locally consistent with respect P if d_{1}is locally consistent with respect to P and d_{2}is locally consistent with respect to the postcondition of d_{1}.

- An assignment

X := a {{Q}} is locally consistent with respect to a precondition P if:

P ->> Q [X ⊢> a]

- A conditional

if b then {{P_{1}}} d_{1}else {{P_{2}}} d_{2}end is locally consistent with respect to precondition P if_{1}_{2}_{1}is locally consistent with respect to P_{1}_{2}is locally consistent with respect to P_{2}

- A loop

while b do {{Q}} d end {{R}} is locally consistent with respect to precondition P if:

- A command with an extra assertion at the beginning

--> {{Q}} d is locally consistent with respect to a precondition P if:

- A command with an extra assertion at the end

d ->> {{Q}} is locally consistent with respect to a precondition P if:

Fixpoint verification_conditions (P : Assertion) (d : dcom) : Prop :=

match d with

| DCSkip Q ⇒

(P ->> Q)

| DCSeq d

verification_conditions P d

∧ verification_conditions (post d

| DCAsgn X a Q ⇒

(P ->> Q [X ⊢> a])

| DCIf b P

((P ∧ b) ->> P

∧ ((P ∧ ¬ b) ->> P

∧ (post d

∧ verification_conditions P

∧ verification_conditions P

| DCWhile b Pbody d Ppost ⇒

(* post d is the loop invariant and the initial

precondition *)

(P ->> post d)

∧ ((post d ∧ b) ->> Pbody)%assertion

∧ ((post d ∧ ¬ b) ->> Ppost)%assertion

∧ verification_conditions Pbody d

| DCPre P' d ⇒

(P ->> P')

∧ verification_conditions P' d

| DCPost d Q ⇒

verification_conditions P d

∧ (post d ->> Q)

end.

match d with

| DCSkip Q ⇒

(P ->> Q)

| DCSeq d

_{1}d_{2}⇒verification_conditions P d

_{1}∧ verification_conditions (post d

_{1}) d_{2}| DCAsgn X a Q ⇒

(P ->> Q [X ⊢> a])

| DCIf b P

_{1}d_{1}P_{2}d_{2}Q ⇒((P ∧ b) ->> P

_{1})%assertion∧ ((P ∧ ¬ b) ->> P

_{2})%assertion∧ (post d

_{1}->> Q) ∧ (post d_{2}->> Q)∧ verification_conditions P

_{1}d_{1}∧ verification_conditions P

_{2}d_{2}| DCWhile b Pbody d Ppost ⇒

(* post d is the loop invariant and the initial

precondition *)

(P ->> post d)

∧ ((post d ∧ b) ->> Pbody)%assertion

∧ ((post d ∧ ¬ b) ->> Ppost)%assertion

∧ verification_conditions Pbody d

| DCPre P' d ⇒

(P ->> P')

∧ verification_conditions P' d

| DCPost d Q ⇒

verification_conditions P d

∧ (post d ->> Q)

end.

The key theorem states 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}}.

verification_conditions P d → {{P}} extract d {{post d}}.

Proof.

induction d; intros; simpl in ×.

- (* Skip *)

eapply hoare_consequence_pre.

+ apply hoare_skip.

+ assumption.

- (* Seq *)

destruct H as [H

eapply hoare_seq.

+ apply IHd2. apply H

+ apply IHd1. apply H

- (* Asgn *)

eapply hoare_consequence_pre.

+ apply hoare_asgn.

+ assumption.

- (* If *)

destruct H as [HPre1 [HPre2 [Hd

apply IHd1 in HThen. clear IHd1.

apply IHd2 in HElse. clear IHd2.

apply hoare_if.

+ eapply hoare_consequence; eauto.

+ eapply hoare_consequence; eauto.

- (* While *)

destruct H as [Hpre [Hbody1 [Hpost1 Hd] ] ].

eapply hoare_consequence; eauto.

apply hoare_while.

eapply hoare_consequence_pre; eauto.

- (* Pre *)

destruct H as [HP Hd].

eapply hoare_consequence_pre; eauto.

- (* Post *)

destruct H as [Hd HQ].

eapply hoare_consequence_post; eauto.

Qed.

induction d; intros; simpl in ×.

- (* Skip *)

eapply hoare_consequence_pre.

+ apply hoare_skip.

+ assumption.

- (* Seq *)

destruct H as [H

_{1}H_{2}].eapply hoare_seq.

+ apply IHd2. apply H

_{2}.+ apply IHd1. apply H

_{1}.- (* Asgn *)

eapply hoare_consequence_pre.

+ apply hoare_asgn.

+ assumption.

- (* If *)

destruct H as [HPre1 [HPre2 [Hd

_{1}[Hd_{2}[HThen HElse] ] ] ] ].apply IHd1 in HThen. clear IHd1.

apply IHd2 in HElse. clear IHd2.

apply hoare_if.

+ eapply hoare_consequence; eauto.

+ eapply hoare_consequence; eauto.

- (* While *)

destruct H as [Hpre [Hbody1 [Hpost1 Hd] ] ].

eapply hoare_consequence; eauto.

apply hoare_while.

eapply hoare_consequence_pre; eauto.

- (* Pre *)

destruct H as [HP Hd].

eapply hoare_consequence_pre; eauto.

- (* Post *)

destruct H as [Hd HQ].

eapply hoare_consequence_post; eauto.

Qed.

Now that all the pieces are in place, we can define what it means
to verify an entire program.

Definition verification_conditions_dec

(dec : decorated) : Prop :=

match dec with

| Decorated P d ⇒ verification_conditions P d

end.

Corollary verification_correct_dec : ∀ dec,

verification_conditions_dec dec →

outer_triple_valid dec.

(dec : decorated) : Prop :=

match dec with

| Decorated P d ⇒ verification_conditions P d

end.

Corollary verification_correct_dec : ∀ dec,

verification_conditions_dec dec →

outer_triple_valid dec.

## Automation

Eval simpl in verification_conditions_dec dec_while.

(* ==>

((fun _ : state => True) ->>

(fun _ : state => True)) /\

((fun st : state => True /\ negb (st X =? 0) = true) ->>

(fun st : state => True /\ st X <> 0)) /\

((fun st : state => True /\ negb (st X =? 0) <> true) ->>

(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)

: Prop

*)

(* ==>

((fun _ : state => True) ->>

(fun _ : state => True)) /\

((fun st : state => True /\ negb (st X =? 0) = true) ->>

(fun st : state => True /\ st X <> 0)) /\

((fun st : state => True /\ negb (st X =? 0) <> true) ->>

(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)

: Prop

*)

Fortunately, our verify_assn tactic can generally take care of
most or all of them.

To automate the overall process of verification, we can use
verification_correct to extract the verification conditions, use
verify_assn to verify them as much as it can, and finally tidy
up any remaining bits by hand.

Here's the final, formal proof that dec_while is correct.

Similarly, here is the formal decorated program for the "swapping
by adding and subtracting" example that we saw earlier.

Definition swap_dec (m n:nat) : decorated :=

<{

{{ X = m ∧ Y = n}} ->>

{{ (X + Y) - ((X + Y) - Y) = n ∧ (X + Y) - Y = m }}

X := X + Y

{{ X - (X - Y) = n ∧ X - Y = m }};

Y := X - Y

{{ X - Y = n ∧ Y = m }};

X := X - Y

{{ X = n ∧ Y = m}}

}>.

Theorem swap_correct : ∀ m n,

outer_triple_valid (swap_dec m n).

Proof. verify. Qed.

<{

{{ X = m ∧ Y = n}} ->>

{{ (X + Y) - ((X + Y) - Y) = n ∧ (X + Y) - Y = m }}

X := X + Y

{{ X - (X - Y) = n ∧ X - Y = m }};

Y := X - Y

{{ X - Y = n ∧ Y = m }};

X := X - Y

{{ X = n ∧ Y = m}}

}>.

Theorem swap_correct : ∀ m n,

outer_triple_valid (swap_dec m n).

Proof. verify. Qed.

And here is the formal decorated version of the "positive
difference" program from earlier:

Definition positive_difference_dec :=

<{

{{True}}

if X ≤ Y then

{{True ∧ X ≤ Y}} ->>

{{(Y - X) + X = Y

∨ (Y - X) + Y = X}}

Z := Y - X

{{Z + X = Y ∨ Z + Y = X}}

else

{{True ∧ ~(X ≤ Y)}} ->>

{{(X - Y) + X = Y

∨ (X - Y) + Y = X}}

Z := X - Y

{{Z + X = Y ∨ Z + Y = X}}

end

{{Z + X = Y ∨ Z + Y = X}}

}>.

Theorem positive_difference_correct :

outer_triple_valid positive_difference_dec.

Proof. verify. Qed.

<{

{{True}}

if X ≤ Y then

{{True ∧ X ≤ Y}} ->>

{{(Y - X) + X = Y

∨ (Y - X) + Y = X}}

Z := Y - X

{{Z + X = Y ∨ Z + Y = X}}

else

{{True ∧ ~(X ≤ Y)}} ->>

{{(X - Y) + X = Y

∨ (X - Y) + Y = X}}

Z := X - Y

{{Z + X = Y ∨ Z + Y = X}}

end

{{Z + X = Y ∨ Z + Y = X}}

}>.

Theorem positive_difference_correct :

outer_triple_valid positive_difference_dec.

Proof. verify. Qed.

#### Exercise: 2 stars, standard, especially useful (if_minus_plus_correct)

Here is a skeleton of the formal decorated version of the if_minus_plus program that we saw earlier. Replace all occurrences of FILL_IN_HERE with appropriate assertions and fill in the proof (which should be just as straightforward as in the examples above).
Definition if_minus_plus_dec :=

<{

{{True}}

if (X ≤ Y) then

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

Z := Y - X

{{ FILL_IN_HERE }}

else

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

Y := X + Z

{{ FILL_IN_HERE }}

end

{{ Y = X + Z}} }>.

Theorem if_minus_plus_correct :

outer_triple_valid if_minus_plus_dec.

Proof.

(* FILL IN HERE *) Admitted.

☐

<{

{{True}}

if (X ≤ Y) then

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

Z := Y - X

{{ FILL_IN_HERE }}

else

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

Y := X + Z

{{ FILL_IN_HERE }}

end

{{ Y = X + Z}} }>.

Theorem if_minus_plus_correct :

outer_triple_valid if_minus_plus_dec.

Proof.

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 2 stars, standard, optional (div_mod_outer_triple_valid)

Fill in appropriate assertions for the division program from above.
Definition div_mod_dec (a b : nat) : decorated :=

<{

{{ True }} ->>

{{ FILL_IN_HERE }}

X := a

{{ FILL_IN_HERE }};

Y := 0

{{ FILL_IN_HERE }};

while b ≤ X do

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

X := X - b

{{ FILL_IN_HERE }};

Y := Y + 1

{{ FILL_IN_HERE }}

end

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }} }>.

Theorem div_mod_outer_triple_valid : ∀ a b,

outer_triple_valid (div_mod_dec a b).

Proof.

(* FILL IN HERE *) Admitted.

☐

<{

{{ True }} ->>

{{ FILL_IN_HERE }}

X := a

{{ FILL_IN_HERE }};

Y := 0

{{ FILL_IN_HERE }};

while b ≤ X do

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

X := X - b

{{ FILL_IN_HERE }};

Y := Y + 1

{{ FILL_IN_HERE }}

end

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }} }>.

Theorem div_mod_outer_triple_valid : ∀ a b,

outer_triple_valid (div_mod_dec a b).

Proof.

(* FILL IN HERE *) Admitted.

☐

# Finding Loop Invariants

- Strengthening a
*loop invariant*means that you have a stronger assumption to work with when trying to establish the postcondition of the loop body, but it also means that the loop body's postcondition is stronger and thus harder to prove. - Strengthening an
*induction hypothesis*means that you have a stronger assumption to work with when trying to complete the induction step of the proof, but it also means that the statement being proved inductively is stronger and thus harder to prove.

## Example: Slow Subtraction

{{ X = m ∧ Y = n }}

while X ≠ 0 do

Y := Y - 1;

X := X - 1

end

{{ Y = n - m }}

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

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

(1) {{ X = m ∧ Y = n }} ->> (a - OK)

(2) {{ True }}

while X ≠ 0 do

(3) {{ True ∧ X ≠ 0 }} ->> (c - OK)

(4) {{ True }}

Y := Y - 1;

(5) {{ True }}

X := X - 1

(6) {{ True }}

end

(7) {{ True ∧ ~(X ≠ 0) }} ->> (b - WRONG!)

(8) {{ Y = n - m }} While conditions (a) and (c) are trivially satisfied, (b) is wrong: it is not the case that True ∧ X = 0 (7) implies Y = n - m (8). In fact, the two assertions are completely unrelated, so it is very easy to find a counterexample to the implication (say, Y = X = m = 0 and n = 1).

*be*the postcondition. So let's return to our skeleton, instantiate Inv with Y = n - m, and try checking conditions (a) to (c) again.

(1) {{ X = m ∧ Y = n }} ->> (a - WRONG!)

(2) {{ Y = n - m }}

while X ≠ 0 do

(3) {{ Y = n - m ∧ X ≠ 0 }} ->> (c - WRONG!)

(4) {{ Y - 1 = n - m }}

Y := Y - 1;

(5) {{ Y = n - m }}

X := X - 1

(6) {{ Y = n - m }}

end

(7) {{ Y = n - m ∧ ~(X ≠ 0) }} ->> (b - OK)

(8) {{ Y = n - m }} This time, condition (b) holds trivially, but (a) and (c) are broken. Condition (a) requires that (1) X = m ∧ Y = n implies (2) Y = n - m. If we substitute Y by n we have to show that n = n - m for arbitrary m and n, which is not the case (for instance, when m = n = 1). Condition (c) requires that n - m - 1 = n - m, which fails, for instance, for n = 1 and m = 0. So, although Y = n - m holds at the end of the loop, it does not hold from the start, and it doesn't hold on each iteration; it is not a correct invariant.

(1) {{ X = m ∧ Y = n }} ->> (a - OK)

(2) {{ Y - X = n - m }}

while X ≠ 0 do

(3) {{ Y - X = n - m ∧ X ≠ 0 }} ->> (c - OK)

(4) {{ (Y - 1) - (X - 1) = n - m }}

Y := Y - 1;

(5) {{ Y - (X - 1) = n - m }}

X := X - 1

(6) {{ Y - X = n - m }}

end

(7) {{ Y - X = n - m ∧ ~(X ≠ 0) }} ->> (b - OK)

(8) {{ Y = n - m }} Success! Conditions (a), (b) and (c) all hold now. (To verify (c), we need to check that, under the assumption that X ≠ 0, we have Y - X = (Y - 1) - (X - 1); this holds for all natural numbers X and Y.)

Example subtract_slowly_dec (m : nat) (p : nat) : decorated :=

<{

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

Theorem subtract_slowly_outer_triple_valid : ∀ m p,

outer_triple_valid (subtract_slowly_dec m p).

Proof.

(* FILL IN HERE *) Admitted.

<{

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

Theorem subtract_slowly_outer_triple_valid : ∀ m p,

outer_triple_valid (subtract_slowly_dec m p).

Proof.

(* FILL IN HERE *) Admitted.

## Exercise: Slow Assignment

#### Exercise: 2 stars, standard (slow_assignment)

A roundabout way of assigning a number currently stored in X to the variable Y is to start Y at 0, then decrement X until it hits 0, incrementing Y at each step. Here is a program that implements this idea. Fill in decorations and prove the decorated program correct. (The proof should be very simple.)
Example slow_assignment_dec (m : nat) : decorated :=

<{

{{ X = m }}

Y := 0

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }} ;

while X ≠ 0 do

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

X := X - 1

{{ FILL_IN_HERE }} ;

Y := Y + 1

{{ FILL_IN_HERE }}

end

{{ FILL_IN_HERE }} ->>

{{ Y = m }}

}>.

Theorem slow_assignment : ∀ m,

outer_triple_valid (slow_assignment_dec m).

Proof. (* FILL IN HERE *) Admitted.

☐

<{

{{ X = m }}

Y := 0

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }} ;

while X ≠ 0 do

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

X := X - 1

{{ FILL_IN_HERE }} ;

Y := Y + 1

{{ FILL_IN_HERE }}

end

{{ FILL_IN_HERE }} ->>

{{ Y = m }}

}>.

Theorem slow_assignment : ∀ m,

outer_triple_valid (slow_assignment_dec m).

Proof. (* FILL IN HERE *) Admitted.

☐

## Example: Parity

{{ X = m }}

while 2 ≤ X do

X := X - 2

end

{{ X = parity m }} The parity function used in the specification is defined in Coq as follows:

The postcondition does not hold at the beginning of the loop,
since m = parity m does not hold for an arbitrary m, so we
cannot hope to use that as an invariant. To find an invariant that works,
let's think a bit about what this loop does. On each iteration it
decrements X by 2, which preserves the parity of X. So the
parity of X does not change, i.e., it is invariant. The initial
value of X is m, so the parity of X is always equal to the
parity of m. Using parity X = parity m as an invariant we
obtain the following decorated program:

{{ X = m }} ->> (a - OK)

{{ parity X = parity m }}

while 2 ≤ X do

{{ parity X = parity m ∧ 2 ≤ X }} ->> (c - OK)

{{ parity (X-2) = parity m }}

X := X - 2

{{ parity X = parity m }}

end

{{ parity X = parity m ∧ ~(2 ≤ X) }} ->> (b - OK)

{{ X = parity m }} With this invariant, conditions (a), (b), and (c) are all satisfied. For verifying (b), we observe that, when X < 2, we have parity X = X (we can easily see this in the definition of parity). For verifying (c), we observe that, when 2 ≤ X, we have parity X = parity (X-2).
Hint: There are actually several possible loop invariants that all
lead to good proofs; one that leads to a particularly simple proof
is parity X = parity m ∧ 2 ≤ X -- or more formally, using the
ap operator to lift the application of the parity function
into the syntax of assertions, {{ ap parity X = parity m ∧ 2 ≤
X }}.

{{ X = m }} ->> (a - OK)

{{ parity X = parity m }}

while 2 ≤ X do

{{ parity X = parity m ∧ 2 ≤ X }} ->> (c - OK)

{{ parity (X-2) = parity m }}

X := X - 2

{{ parity X = parity m }}

end

{{ parity X = parity m ∧ ~(2 ≤ X) }} ->> (b - OK)

{{ X = parity m }} With this invariant, conditions (a), (b), and (c) are all satisfied. For verifying (b), we observe that, when X < 2, we have parity X = X (we can easily see this in the definition of parity). For verifying (c), we observe that, when 2 ≤ X, we have parity X = parity (X-2).

#### Exercise: 3 stars, standard, optional (parity_formal)

Translate the above informal decorated program into a formal one and prove it correct.
Definition parity_dec (m:nat) : decorated :=

<{

{{ X = m }} ->>

{{ FILL_IN_HERE }}

while 2 ≤ X do

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

X := X - 2

{{ FILL_IN_HERE }}

end

{{ FILL_IN_HERE }} ->>

{{ X = parity m }} }>.

<{

{{ X = m }} ->>

{{ FILL_IN_HERE }}

while 2 ≤ X do

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

X := X - 2

{{ FILL_IN_HERE }}

end

{{ FILL_IN_HERE }} ->>

{{ X = parity m }} }>.

If you use the suggested invariant, you may find the following
lemmas helpful (as well as leb_complete and leb_correct).

Lemma parity_ge_2 : ∀ x,

2 ≤ x →

parity (x - 2) = parity x.

Lemma parity_lt_2 : ∀ x,

¬ 2 ≤ x →

parity x = x.

Theorem parity_outer_triple_valid : ∀ m,

outer_triple_valid (parity_dec m).

Proof.

(* FILL IN HERE *) Admitted.

☐

2 ≤ x →

parity (x - 2) = parity x.

Proof.

induction x; intros; simpl.

- reflexivity.

- destruct x.

+ lia.

+ inversion H; subst; simpl.

× reflexivity.

× rewrite sub_0_r. reflexivity.

Qed.

induction x; intros; simpl.

- reflexivity.

- destruct x.

+ lia.

+ inversion H; subst; simpl.

× reflexivity.

× rewrite sub_0_r. reflexivity.

Qed.

Lemma parity_lt_2 : ∀ x,

¬ 2 ≤ x →

parity x = x.

Proof.

induction x; intros; simpl.

- reflexivity.

- destruct x.

+ reflexivity.

+ lia.

Qed.

induction x; intros; simpl.

- reflexivity.

- destruct x.

+ reflexivity.

+ lia.

Qed.

Theorem parity_outer_triple_valid : ∀ m,

outer_triple_valid (parity_dec m).

Proof.

(* FILL IN HERE *) Admitted.

☐

## Example: Finding Square Roots

{{ X=m }}

Z := 0;

while (Z+1)*(Z+1) ≤ X do

Z := Z+1

end

{{ Z×Z≤m ∧ m<(Z+1)*(Z+1) }}

(1) {{ X=m }} ->> (a - second conjunct of (2) WRONG!)

(2) {{ 0*0 ≤ m ∧ m<(0+1)*(0+1) }}

Z := 0

(3) {{ Z×Z ≤ m ∧ m<(Z+1)*(Z+1) }};

while (Z+1)*(Z+1) ≤ X do

(4) {{ Z×Z≤m ∧ (Z+1)*(Z+1)<=X }} ->> (c - WRONG!)

(5) {{ (Z+1)*(Z+1)<=m ∧ m<((Z+1)+1)*((Z+1)+1) }}

Z := Z+1

(6) {{ Z×Z≤m ∧ m<(Z+1)*(Z+1) }}

end

(7) {{ Z×Z≤m ∧ m<(Z+1)*(Z+1) ∧ ~((Z+1)*(Z+1)<=X) }} ->> (b - OK)

(8) {{ Z×Z≤m ∧ m<(Z+1)*(Z+1) }} This didn't work very well: conditions (a) and (c) both failed. Looking at condition (c), we see that the second conjunct of (4) is almost the same as the first conjunct of (5), except that (4) mentions X while (5) mentions m. But note that X is never assigned in this program, so we should always have X=m. We didn't propagate this information from (1) into the loop invariant, but we could!

{{ X=m }} ->> (a - OK)

{{ X=m ∧ 0*0 ≤ m }}

Z := 0

{{ X=m ∧ Z×Z ≤ m }};

while (Z+1)*(Z+1) ≤ X do

{{ X=m ∧ Z×Z≤m ∧ (Z+1)*(Z+1)<=X }} ->> (c - OK)

{{ X=m ∧ (Z+1)*(Z+1)<=m }}

Z := Z + 1

{{ X=m ∧ Z×Z≤m }}

end

{{ X=m ∧ Z×Z≤m ∧ ~((Z+1)*(Z+1)<=X) }} ->> (b - OK)

{{ Z×Z≤m ∧ m<(Z+1)*(Z+1) }} This works, since conditions (a), (b), and (c) are now all trivially satisfied.

#### Exercise: 3 stars, standard, optional (sqrt_formal)

Translate the above informal decorated program into a formal one and prove it correct.
Definition sqrt_dec (m:nat) : decorated :=

<{

{{ X = m }} ->>

{{ FILL_IN_HERE }}

Z := 0

{{ FILL_IN_HERE }};

while ((Z+1)×(Z+1) ≤ X) do

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

Z := Z + 1

{{ FILL_IN_HERE }}

end

{{ FILL_IN_HERE }} ->>

{{ Z×Z≤m ∧ m<(Z+1)*(Z+1) }}

}>.

Theorem sqrt_correct : ∀ m,

outer_triple_valid (sqrt_dec m).

Proof. (* FILL IN HERE *) Admitted.

<{

{{ X = m }} ->>

{{ FILL_IN_HERE }}

Z := 0

{{ FILL_IN_HERE }};

while ((Z+1)×(Z+1) ≤ X) do

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

Z := Z + 1

{{ FILL_IN_HERE }}

end

{{ FILL_IN_HERE }} ->>

{{ Z×Z≤m ∧ m<(Z+1)*(Z+1) }}

}>.

Theorem sqrt_correct : ∀ m,

outer_triple_valid (sqrt_dec m).

Proof. (* FILL IN HERE *) Admitted.

## Example: Squaring

{{ X = m }}

Y := 0;

Z := 0;

while Y ≠ X do

Z := Z + X;

Y := Y + 1

end

{{ Z = m×m }}

{{ X = m }} ->> (a - WRONG)

{{ 0 = m×m ∧ X = m }}

Y := 0

{{ 0 = m×m ∧ X = m }};

Z := 0

{{ Z = m×m ∧ X = m }};

while Y ≠ X do

{{ Z = m×m ∧ X = m ∧ Y ≠ X }} ->> (c - WRONG)

{{ Z+X = m×m ∧ X = m }}

Z := Z + X

{{ Z = m×m ∧ X = m }};

Y := Y + 1

{{ Z = m×m ∧ X = m }}

end

{{ Z = m×m ∧ X = m ∧ ~(Y ≠ X) }} ->> (b - OK)

{{ Z = m×m }}

{{ X = m }} ->> (a - OK)

{{ 0 = 0*m ∧ X = m }}

Y := 0;

{{ 0 = Y×m ∧ X = m }}

Z := 0;

{{ Z = Y×m ∧ X = m }}

while Y ≠ X do

{{ Z = Y×m ∧ X = m ∧ Y ≠ X }} ->> (c - OK)

{{ Z+X = (Y+1)*m ∧ X = m }}

Z := Z + X;

{{ Z = (Y+1)*m ∧ X = m }}

Y := Y + 1

{{ Z = Y×m ∧ X = m }}

end

{{ Z = Y×m ∧ X = m ∧ ~(Y ≠ X) }} ->> (b - OK)

{{ Z = m×m }}

## Exercise: Factorial

#### Exercise: 4 stars, advanced (factorial_correct)

Recall that n! denotes the factorial of n (i.e., n! = 1*2*...*n). Formally, the factorial function is defined recursively in the Coq standard library in a way that is equivalent to the following:Fixpoint fact (n : nat) : nat :=

match n with

| O ⇒ 1

| S n' ⇒ n × (fact n')

end.

First, write the Imp program factorial that calculates the factorial
of the number initially stored in the variable X and puts it in
the variable Y.
Using your definition factorial and slow_assignment_dec as a
guide, write a formal decorated program factorial_dec that
implements the factorial function. Hint: recall the use of ap
in assertions to apply a function to an Imp variable.
Fill in the blanks and finish the proof of correctness. Bear in mind
that we are working with natural numbers, for which both division
and subtraction can behave differently than with real numbers.
Excluding both operations from your loop invariant is advisable!
Then state a theorem named factorial_outer_triple_valid that says
factorial_dec is correct, and prove the theorem. If all goes
well, verify will leave you with just two subgoals, each of
which requires establishing some mathematical property of fact,
rather than proving anything about your program.
Hint: if those two subgoals become tedious to prove, give some
though to how you could restate your assertions such that the
mathematical operations are more amenable to manipulation in Coq.
For example, recall that 1 + ... is easier to work with than
... + 1.

Example factorial_dec (m:nat) : decorated

(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

(* FILL IN HERE *)

Theorem factorial_correct: ∀ m,

outer_triple_valid (factorial_dec m).

Proof. (* FILL IN HERE *) Admitted.

☐

(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

(* FILL IN HERE *)

Theorem factorial_correct: ∀ m,

outer_triple_valid (factorial_dec m).

Proof. (* FILL IN HERE *) Admitted.

☐

## Exercise: Minimum

#### Exercise: 3 stars, standard (minimum_correct)

Fill in decorations for the following program and prove them correct. As with factorial, be careful about natural numbers, especially subtraction._{2}to be parsed correctly. E.g., min a b needs to be written ap

_{2}min a b in an assertion.

Definition minimum_dec (a b : nat) : decorated :=

<{

{{ True }} ->>

{{ FILL_IN_HERE }}

X := a

{{ FILL_IN_HERE }};

Y := b

{{ FILL_IN_HERE }};

Z := 0

{{ FILL_IN_HERE }};

while X ≠ 0 && Y ≠ 0 do

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

X := X - 1

{{ FILL_IN_HERE }};

Y := Y - 1

{{ FILL_IN_HERE }};

Z := Z + 1

{{ FILL_IN_HERE }}

end

{{ FILL_IN_HERE }} ->>

{{ Z = min a b }}

}>.

(* HIDE

- The first implication holds by substitution and algebra.

- The second holds because:

+ by lemma2 we can rewrite Z+1 + min (X-1) (Y-1) as

Z+1 + (min x y) - 1

+ by lemma1 and X<>0 ∧ Y<>0, min x y ≠ 0,

so (min x y) - 1 is not zero-truncated.

+ so we can rewrite Z+1 + (min x y) - 1 as Z + min x y.

- The third holds because the second conjunct implies X and Y

are both 0. *)

Theorem minimum_correct : ∀ a b,

outer_triple_valid (minimum_dec a b).

Proof. (* FILL IN HERE *) Admitted.

☐

<{

{{ True }} ->>

{{ FILL_IN_HERE }}

X := a

{{ FILL_IN_HERE }};

Y := b

{{ FILL_IN_HERE }};

Z := 0

{{ FILL_IN_HERE }};

while X ≠ 0 && Y ≠ 0 do

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

X := X - 1

{{ FILL_IN_HERE }};

Y := Y - 1

{{ FILL_IN_HERE }};

Z := Z + 1

{{ FILL_IN_HERE }}

end

{{ FILL_IN_HERE }} ->>

{{ Z = min a b }}

}>.

(* HIDE

- The first implication holds by substitution and algebra.

- The second holds because:

+ by lemma2 we can rewrite Z+1 + min (X-1) (Y-1) as

Z+1 + (min x y) - 1

+ by lemma1 and X<>0 ∧ Y<>0, min x y ≠ 0,

so (min x y) - 1 is not zero-truncated.

+ so we can rewrite Z+1 + (min x y) - 1 as Z + min x y.

- The third holds because the second conjunct implies X and Y

are both 0. *)

Theorem minimum_correct : ∀ a b,

outer_triple_valid (minimum_dec a b).

Proof. (* FILL IN HERE *) Admitted.

☐

## Exercise: Two Loops

#### Exercise: 3 stars, standard (two_loops)

Here is a pretty inefficient way of adding 3 numbers:X := 0;

Y := 0;

Z := c;

while X ≠ a do

X := X + 1;

Z := Z + 1

end;

while Y ≠ b do

Y := Y + 1;

Z := Z + 1

end Show that it does what it should by completing the following decorated program.

Definition two_loops_dec (a b c : nat) : decorated :=

<{

{{ True }} ->>

{{ FILL_IN_HERE }}

X := 0

{{ FILL_IN_HERE }};

Y := 0

{{ FILL_IN_HERE }};

Z := c

{{ FILL_IN_HERE }};

while X ≠ a do

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

X := X + 1

{{ FILL_IN_HERE }};

Z := Z + 1

{{ FILL_IN_HERE }}

end

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }};

while Y ≠ b do

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

Y := Y + 1

{{ FILL_IN_HERE }};

Z := Z + 1

{{ FILL_IN_HERE }}

end

{{ FILL_IN_HERE }} ->>

{{ Z = a + b + c }}

}>.

Theorem two_loops : ∀ a b c,

outer_triple_valid (two_loops_dec a b c).

Proof.

(* FILL IN HERE *) Admitted.

☐

<{

{{ True }} ->>

{{ FILL_IN_HERE }}

X := 0

{{ FILL_IN_HERE }};

Y := 0

{{ FILL_IN_HERE }};

Z := c

{{ FILL_IN_HERE }};

while X ≠ a do

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

X := X + 1

{{ FILL_IN_HERE }};

Z := Z + 1

{{ FILL_IN_HERE }}

end

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }};

while Y ≠ b do

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

Y := Y + 1

{{ FILL_IN_HERE }};

Z := Z + 1

{{ FILL_IN_HERE }}

end

{{ FILL_IN_HERE }} ->>

{{ Z = a + b + c }}

}>.

Theorem two_loops : ∀ a b c,

outer_triple_valid (two_loops_dec a b c).

Proof.

(* FILL IN HERE *) Admitted.

☐

## Exercise: Power Series

#### Exercise: 4 stars, standard, optional (dpow2)

Here is a program that computes the series: 1 + 2 + 2^2 + ... + 2^m = 2^(m+1) - 1X := 0;

Y := 1;

Z := 1;

while X ≠ m do

Z := 2 × Z;

Y := Y + Z;

X := X + 1

end Turn this into a decorated program and prove it correct.

Fixpoint pow2 n :=

match n with

| 0 ⇒ 1

| S n' ⇒ 2 × (pow2 n')

end.

Definition dpow2_dec (n : nat) :=

<{

{{ True }} ->>

{{ FILL_IN_HERE }}

X := 0

{{ FILL_IN_HERE }};

Y := 1

{{ FILL_IN_HERE }};

Z := 1

{{ FILL_IN_HERE }};

while X ≠ n do

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

Z := 2 × Z

{{ FILL_IN_HERE }};

Y := Y + Z

{{ FILL_IN_HERE }};

X := X + 1

{{ FILL_IN_HERE }}

end

{{ FILL_IN_HERE }} ->>

{{ Y = pow2 (n+1) - 1 }}

}>.

match n with

| 0 ⇒ 1

| S n' ⇒ 2 × (pow2 n')

end.

Definition dpow2_dec (n : nat) :=

<{

{{ True }} ->>

{{ FILL_IN_HERE }}

X := 0

{{ FILL_IN_HERE }};

Y := 1

{{ FILL_IN_HERE }};

Z := 1

{{ FILL_IN_HERE }};

while X ≠ n do

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

Z := 2 × Z

{{ FILL_IN_HERE }};

Y := Y + Z

{{ FILL_IN_HERE }};

X := X + 1

{{ FILL_IN_HERE }}

end

{{ FILL_IN_HERE }} ->>

{{ Y = pow2 (n+1) - 1 }}

}>.

Some lemmas that you may find useful...

Lemma pow2_plus_1 : ∀ n,

pow2 (n+1) = pow2 n + pow2 n.

Proof. induction n; simpl. reflexivity. lia. Qed.

Lemma pow2_le_1 : ∀ n, pow2 n ≥ 1.

Proof. induction n. simpl. constructor. simpl. lia. Qed.

pow2 (n+1) = pow2 n + pow2 n.

Proof. induction n; simpl. reflexivity. lia. Qed.

Lemma pow2_le_1 : ∀ n, pow2 n ≥ 1.

Proof. induction n. simpl. constructor. simpl. lia. Qed.

The main correctness theorem:

Theorem dpow2_down_correct : ∀ n,

outer_triple_valid (dpow2_dec n).

Proof.

(* FILL IN HERE *) Admitted.

☐

outer_triple_valid (dpow2_dec n).

Proof.

(* FILL IN HERE *) Admitted.

☐

# Weakest Preconditions (Optional)

{{ False }} X := Y + 1 {{ X ≤ 5 }} is

*not*very interesting: although it is perfectly valid , it tells us nothing useful. Since the precondition isn't satisfied by any state, it doesn't describe any situations where we can use the command X := Y + 1 to achieve the postcondition X ≤ 5.

{{ Y ≤ 4 ∧ Z = 0 }} X := Y + 1 {{ X ≤ 5 }} has a useful precondition: it tells us that, if we can somehow create a situation in which we know that Y ≤ 4 ∧ Z = 0, then running this command will produce a state satisfying the postcondition. However, this precondition is not as useful as it could be, because the Z = 0 clause in the precondition actually has nothing to do with the postcondition X ≤ 5.

*most*useful precondition for this command is this one:

{{ Y ≤ 4 }} X := Y + 1 {{ X ≤ 5 }} The assertion Y ≤ 4 is called the

*weakest precondition*of X := Y + 1 with respect to the postcondition X ≤ 5.

*weakest precondition*of command X := Y + 1 with respect to postcondition X ≤ 5. Think of

*weakest*here as meaning "easiest to satisfy": a weakest precondition is one that as many states as possible can satisfy.

- P is a precondition, that is, {{P}} c {{Q}}; and
- P is at least as weak as all other preconditions, that is, if {{P'}} c {{Q}} then P' ->> P.

#### Exercise: 1 star, standard, optional (wp)

What are weakest preconditions of the following commands for the following postconditions?1) {{ ? }} skip {{ X = 5 }}

2) {{ ? }} X := Y + Z {{ X = 5 }}

3) {{ ? }} X := Y {{ X = Y }}

4) {{ ? }}

if X = 0 then Y := Z + 1 else Y := W + 2 end

{{ Y = 5 }}

5) {{ ? }}

X := 5

{{ X = 0 }}

6) {{ ? }}

while true do X := 0 end

{{ X = 0 }}

(* FILL IN HERE *)

☐

☐

#### Exercise: 3 stars, advanced, optional (is_wp_formal)

Prove formally, using the definition of hoare_triple, that Y ≤ 4 is indeed a weakest precondition of X := Y + 1 with respect to postcondition X ≤ 5.#### Exercise: 2 stars, advanced, optional (hoare_asgn_weakest)

Show that the precondition in the rule hoare_asgn is in fact the weakest precondition.
Theorem hoare_asgn_weakest : ∀ Q X a,

is_wp (Q [X ⊢> a]) <{ X := a }> Q.

Proof.

(* FILL IN HERE *) Admitted.

☐

is_wp (Q [X ⊢> a]) <{ X := a }> Q.

Proof.

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 2 stars, advanced, optional (hoare_havoc_weakest)

Show that your havoc_pre function from the himp_hoare exercise in the Hoare chapter returns a weakest precondition.
Module Himp2.

Import Himp.

Lemma hoare_havoc_weakest : ∀ (P Q : Assertion) (X : string),

{{ P }} havoc X {{ Q }} →

P ->> havoc_pre X Q.

Proof.

(* FILL IN HERE *) Admitted.

Import Himp.

Lemma hoare_havoc_weakest : ∀ (P Q : Assertion) (X : string),

{{ P }} havoc X {{ Q }} →

P ->> havoc_pre X Q.

Proof.

(* FILL IN HERE *) Admitted.

☐

Fixpoint fib n :=

match n with

| 0 ⇒ 1

| 1 ⇒ 1

| _ ⇒ fib (pred n) + fib (pred (pred n))

end. This doesn't pass Coq's termination checker, but here is a slightly clunkier definition that does:

#### Exercise: 2 stars, advanced, optional (fib_eqn)

The Fibonacci function is usually written like this:Fixpoint fib n :=

match n with

| 0 ⇒ 1

| 1 ⇒ 1

| _ ⇒ fib (pred n) + fib (pred (pred n))

end. This doesn't pass Coq's termination checker, but here is a slightly clunkier definition that does:

Fixpoint fib n :=

match n with

| 0 ⇒ 1

| S n' ⇒ match n' with

| 0 ⇒ 1

| S n'' ⇒ fib n' + fib n''

end

end.

match n with

| 0 ⇒ 1

| S n' ⇒ match n' with

| 0 ⇒ 1

| S n'' ⇒ fib n' + fib n''

end

end.

Prove that fib satisfies the following equation. You will need this
as a lemma in the next exercise.

Lemma fib_eqn : ∀ n,

n > 0 →

fib n + fib (pred n) = fib (1 + n).

Proof.

(* FILL IN HERE *) Admitted.

☐

n > 0 →

fib n + fib (pred n) = fib (1 + n).

Proof.

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 4 stars, advanced, optional (fib)

The following Imp program leaves the value of fib n in the variable Y when it terminates:X := 1;

Y := 1;

Z := 1;

while X ≠ 1 + n do

T := Z;

Z := Z + Y;

Y := T;

X := 1 + X

end Fill in the following definition of dfib and prove that it satisfies this specification:

{{ True }} dfib {{ Y = fib n }} You will need many uses of ap in your assertions. If all goes well, your proof will be very brief.

Definition T : string := "T".

Definition dfib (n : nat) : decorated :=

<{

{{ True }} ->>

{{ FILL_IN_HERE }}

X := 1

{{ FILL_IN_HERE }} ;

Y := 1

{{ FILL_IN_HERE }} ;

Z := 1

{{ FILL_IN_HERE }} ;

while X ≠ 1 + n do

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

T := Z

{{ FILL_IN_HERE }};

Z := Z + Y

{{ FILL_IN_HERE }};

Y := T

{{ FILL_IN_HERE }};

X := 1 + X

{{ FILL_IN_HERE }}

end

{{ FILL_IN_HERE }} ->>

{{ Y = fib n }}

}>.

Theorem dfib_correct : ∀ n,

outer_triple_valid (dfib n).

(* FILL IN HERE *) Admitted.

☐

Definition dfib (n : nat) : decorated :=

<{

{{ True }} ->>

{{ FILL_IN_HERE }}

X := 1

{{ FILL_IN_HERE }} ;

Y := 1

{{ FILL_IN_HERE }} ;

Z := 1

{{ FILL_IN_HERE }} ;

while X ≠ 1 + n do

{{ FILL_IN_HERE }} ->>

{{ FILL_IN_HERE }}

T := Z

{{ FILL_IN_HERE }};

Z := Z + Y

{{ FILL_IN_HERE }};

Y := T

{{ FILL_IN_HERE }};

X := 1 + X

{{ FILL_IN_HERE }}

end

{{ FILL_IN_HERE }} ->>

{{ Y = fib n }}

}>.

Theorem dfib_correct : ∀ n,

outer_triple_valid (dfib n).

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 5 stars, advanced, optional (improve_dcom)

The formal decorated programs defined in this section are intended to look as similar as possible to the informal ones defined earlier. If we drop this requirement, we can eliminate almost all annotations, just requiring final postconditions and loop invariants to be provided explicitly. Do this -- i.e., define a new version of dcom with as few annotations as possible and adapt the rest of the formal development leading up to the verification_correct theorem.
(* FILL IN HERE *)

☐

☐

(* 2022-09-20 16:43 *)