# Hoare: Hoare Logic

In the past two chapters, we've begun applying the mathematical
tools developed in the first part of the course to studying the
theory of a small programming language, Imp.
In this chapter, we're going to take this idea further. We'll
develop a reasoning system called
Hoare Logic originates 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 huge variety of tools that are now being
used to specify and verify real software systems.
If we're going to talk about specifications of programs, the first
thing we'll want is a way of making

- We defined a type of
*abstract syntax trees*for Imp, together with an*evaluation relation*(a partial function on states) that specifies the*operational semantics*of programs. - We proved a number of
*metatheoretic properties*-- "meta" in the sense that they are properties of the language as a whole, rather than properties of particular programs in the language. These included:- determinacy of evaluation
- equivalence of some different ways of writing down the
definition
- guaranteed termination of certain classes of programs
- correctness (in the sense of preserving behavioral
equivalence) of a number of useful program transformations.

*types*and*type soundness*. - determinacy of evaluation
- We saw a couple of examples of
*program verification*-- using the precise definition of Imp to prove formally that certain particular programs (factorial and slow subtraction) satisfied particular specifications of their behavior.

*Floyd-Hoare Logic*-- usually, if somewhat unfairly, shortened to just*Hoare Logic*-- in which each of the syntactic constructs of Imp is equipped with a single, generic "proof rule" that can be used to reason about programs involving this construct.# Hoare Logic

## Assertions

*assertions*about properties that hold at particular points in time -- i.e., properties that may or may not be true of a given state.#### Exercise: 1 star (assertions)

Paraphrase the following assertions in English.
fun st => st X = 3

fun st => st X = x

fun st => st X <= st Y

fun st => st X = 3 \/ st X <= st Y

fun st => (st Z) * (st Z) <= x

/\ ~ (((S (st Z)) * (S (st Z))) <= x)

fun st => True

fun st => False

(Remember that one-star exercises do not need to be handed in.) ☐
fun st => st X = x

fun st => st X <= st Y

fun st => st X = 3 \/ st X <= st Y

fun st => (st Z) * (st Z) <= x

/\ ~ (((S (st Z)) * (S (st Z))) <= x)

fun st => True

fun st => False

*only*way we use states and the only way we refer to the values of variables in the current state: we never need to talk about two states at the same time, etc. So when we are writing down assertions informally, we can make some simplifications: drop the initial fun st => and write just X instead of st X. Informally, instead of

fun st => (st Z) * (st Z) <= x

/\ ~ ((S (st Z)) * (S (st Z)) <= x)

we'll write just
/\ ~ ((S (st Z)) * (S (st Z)) <= x)

Z * Z <= x

/\ ~((S Z) * (S Z) <= x).

/\ ~((S Z) * (S Z) <= x).

## Hoare Triples

- "If c is started in a state satisfying assertion P, and if c eventually terminates, then the final state is guaranteed to satisfy the assertion Q."

*Hoare Triple*. The property P is called a

*precondition*; Q is a

*postcondition*.

{{P}} c {{Q}}.

Traditionally, Hoare triples are written {P} c {Q}, but single
braces are already used for other things in Coq.
Definition hoare_triple (P:Assertion) (c:com) (Q:Assertion) : Prop :=

forall st st',

c / st ==> st' ->

P st ->

Q st'.

Notation "{{ P }} c {{ Q }}" := (hoare_triple P c Q) (at level 90) : hoare_spec_scope.

Open Scope hoare_spec_scope.

#### Exercise: 1 star (triples)

Paraphrase the following Hoare triples in English.
{{True}} c {{X = 5}}

{{X = x}} c {{X = x + 5)}}

{{X <= Y}} c {{Y <= X}}

{{True}} c {{False}}

{{X = x}}

c

{{Y = real_fact x}}.

{{True}}

c

{{(Z * Z) <= x /\ ~ (((S Z) * (S Z)) <= x)}}

☐
{{X = x}} c {{X = x + 5)}}

{{X <= Y}} c {{Y <= X}}

{{True}} c {{False}}

{{X = x}}

c

{{Y = real_fact x}}.

{{True}}

c

{{(Z * Z) <= x /\ ~ (((S Z) * (S Z)) <= x)}}

#### Exercise: 1 star (valid_triples)

Which of the following Hoare triples are*valid*-- i.e., the claimed relation between P, c, and Q is true?

{{True}} X ::= 5 {{X = 5}}

{{X = 2}} X ::= X + 1 {{X = 3}}

{{True}} X ::= 5; Y ::= 0 {{X = 5}}

{{X = 2 /\ X = 3}} X ::= 5 {{X = 0}}

{{True}} SKIP {{False}}

{{False}} SKIP {{True}}

{{True}} WHILE True DO SKIP END {{False}}

{{X = 0}}

WHILE X == 0 DO X ::= X + 1 END

{{X = 1}}

{{X = 1}}

WHILE X <> 0 DO X ::= X + 1 END

{{X = 100}}

(Note that we're using informal mathematical notations for
expressions inside of commands, for readability. We'll continue
doing so throughout the chapter.) ☐
{{X = 2}} X ::= X + 1 {{X = 3}}

{{True}} X ::= 5; Y ::= 0 {{X = 5}}

{{X = 2 /\ X = 3}} X ::= 5 {{X = 0}}

{{True}} SKIP {{False}}

{{False}} SKIP {{True}}

{{True}} WHILE True DO SKIP END {{False}}

{{X = 0}}

WHILE X == 0 DO X ::= X + 1 END

{{X = 1}}

{{X = 1}}

WHILE X <> 0 DO X ::= X + 1 END

{{X = 100}}

Theorem hoare_post_true : forall (P Q : Assertion) c,

(forall st, Q st) ->

{{P}} c {{Q}}.

Proof.

intros P Q c H. unfold hoare_triple.

intros st st' Heval HP.

apply H. Qed.

Theorem hoare_pre_false : forall (P Q : Assertion) c,

(forall st, ~(P st)) ->

{{P}} c {{Q}}.

Proof.

intros P Q c H. unfold hoare_triple.

intros st st' Heval HP.

unfold not in H. apply H in HP.

destruct HP. Qed.

## Weakest Preconditions

#### Exercise: 1 star (wp)

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

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

{{ ? }} X ::= Y {{ X = Y }}

{{ ? }}

IFB X == 0 THEN Y ::= Z + 1 ELSE Y ::= W + 2 FI

{{ Y = 5 }}

{{ ? }}

X ::= 5

{{ X = 0 }}

{{ ? }}

WHILE True DO X ::= 0 END

{{ X = 0 }}

☐
{{ ? }} X ::= Y + Z {{ X = 5 }}

{{ ? }} X ::= Y {{ X = Y }}

{{ ? }}

IFB X == 0 THEN Y ::= Z + 1 ELSE Y ::= W + 2 FI

{{ Y = 5 }}

{{ ? }}

X ::= 5

{{ X = 0 }}

{{ ? }}

WHILE True DO X ::= 0 END

{{ X = 0 }}

## Proof Rules

### Assignment

{{ Y = 1 }} X ::= Y {{ X = 1 }}

In English: if we start out in a state where the value of Y
is 1 and we assign Y to X, then we'll finish in a
state where X is 1. That is, the property of being equal
to 1 gets transferred from Y to X.
{{ Y + Z = 1 }} X ::= Y + Z {{ X = 1 }}

the same property (being equal to one) gets transferred to
X from the expression Y + Z on the right-hand side of
the assignment.
{{ a = 1 }} X ::= a {{ X = 1 }}

is a valid Hoare triple.
{{ Q(a) }} X ::= a {{ Q(X) }}

is a valid Hoare triple.
{{ Q where a is substituted for X }} X ::= a {{ Q }}

This rule looks backwards to everyone at first -- what it's
saying is that, if Q holds in an environment where X is
replaced by the value of a, then Q still holds after
executing X ::= a.
{{ X + 1 <= 5 }} X ::= X + 1 {{ X <= 5 }}

{{ 3 = 3 }} X ::= 3 {{ X = 3 }}

{{ 0 <= 3 /\ 3 <= 5 }} X ::= 3 {{ 0 <= X /\ X <= 5 }}

{{ 3 = 3 }} X ::= 3 {{ X = 3 }}

{{ 0 <= 3 /\ 3 <= 5 }} X ::= 3 {{ 0 <= X /\ X <= 5 }}

Theorem hoare_asgn_firsttry :

forall (Q : aexp -> Assertion) V a,

{{fun st => Q a st}} (V ::= a) {{fun st => Q (AId V) st}}.

But this formulation is not very nice, for two reasons.
First, it is not clear how we'd prove it is valid (we'd need
to somehow reason about all possible propositions). And
second, even if we could prove it, it would be awkward to
use.
forall (Q : aexp -> Assertion) V a,

{{fun st => Q a st}} (V ::= a) {{fun st => Q (AId V) st}}.

- For all states st, "Q where a is substituted for X" holds in the state st if and only if Q holds in the state update st X (aeval st a).

The proof rule for assignment:

{{assn_sub V a Q}} V::=a {{Q}} |

Theorem hoare_asgn : forall Q V a,

{{assn_sub V a Q}} (V ::= a) {{Q}}.

Proof.

unfold hoare_triple.

intros Q V a st st' HE HQ.

inversion HE. subst.

unfold assn_sub in HQ. assumption. Qed.

Here's a first formal proof using this rule:

Example assn_sub_example :

{{fun st => 3 = 3}} (X ::= (ANum 3)) {{fun st => st X = 3}}.

Proof.

assert ((fun st => 3 = 3) =

(assn_sub X (ANum 3) (fun st => st X = 3))).

Case "Proof of assertion".

unfold assn_sub. reflexivity.

rewrite -> H. apply hoare_asgn. Qed.

Unfortunately, the hoare_asgn rule doesn't literally apply
to the initial goal: it only works with triples whose
precondition has precisely the form assn_sub Q V a for some
Q, V, and a. So we start with asserting a little lemma
to get the goal into this form.
Doing this kind of fiddling with the goal state every time we
want to use hoare_asgn would get tiresome pretty quickly.
Fortunately, there are easier alternatives. One simple one is
to state a slightly more general theorem that introduces an
explicit equality hypothesis:

Theorem hoare_asgn_eq : forall Q Q' V a,

Q' = assn_sub V a Q ->

{{Q'}} (V ::= a) {{Q}}.

Proof.

intros Q Q' V a H. rewrite H. apply hoare_asgn. Qed.

With this version of hoare_asgn, we can do the proof much
more smoothly.

Example assn_sub_example' :

{{fun st => 3 = 3}} (X ::= (ANum 3)) {{fun st => st X = 3}}.

Proof.

apply hoare_asgn_eq. reflexivity. Qed.

#### Exercise: 2 stars (hoare_asgn_examples)

Translate these informal Hoare triples
{{ X + 1 <= 5 }} X ::= X + 1 {{ X <= 5 }}

{{ 0 <= 3 /\ 3 <= 5 }} X ::= 3 {{ 0 <= X /\ X <= 5 }}

into formal statements and use hoare_asgn_eq to prove
them.
{{ 0 <= 3 /\ 3 <= 5 }} X ::= 3 {{ 0 <= X /\ X <= 5 }}

(* FILL IN HERE *)

☐
(* FILL IN HERE *)

☐

#### Exercise: 3 stars (hoarestate2)

If the assignment rule still seems "backward", it may help to think a little about alternative "forward" rules. Here is a seemingly natural one:
{{ True }} X ::= a {{ X = a }}

Explain what is wrong with this rule.
☐

#### Exercise: 2 stars, optional (hoare_asgn_weakest)

The precondition in the rule hoare_asgn is in fact the weakest precondition.
Theorem hoare_asgn_weakest : forall P V a Q,

{{P}} (V ::= a) {{Q}} ->

forall st, P st -> assn_sub V a Q st.

Proof.

(* FILL IN HERE *) Admitted.

(* *)

{{P}} (V ::= a) {{Q}} ->

forall st, P st -> assn_sub V a Q st.

Proof.

(* FILL IN HERE *) Admitted.

(* *)

### Consequence

{{3 = 3}} X ::= 3 {{X = 3}},

is a valid Hoare triple, what we probably have in mind when
we think about the effect of this assignment is something
more like this:
{{True}} X ::= 3 {{X = 3}}.

This triple is also valid, but we can't derive it from
hoare_asgn (or hoare_asgn_eq) because True and 3 = 3
are not equal, even after simplification.
*Rule of Consequence*.

{{P'}} c {{Q'}} | |

P implies P' (in every state) | |

Q' implies Q (in every state) | |

{{P}} c {{Q}} |

{{P'}} c {{Q}} | |

P implies P' (in every state) | |

{{P}} c {{Q}} |

{{P}} c {{Q'}} | |

Q' implies Q (in every state) | |

{{P}} c {{Q}} |

Theorem hoare_consequence : forall (P P' Q Q' : Assertion) c,

{{P'}} c {{Q'}} ->

(forall st, P st -> P' st) ->

(forall st, Q' st -> Q st) ->

{{P}} c {{Q}}.

Proof.

unfold hoare_triple.

intros P P' Q Q' c Hht HPP' HQ'Q.

intros st st' Hc HP.

apply HQ'Q. apply (Hht st st'). assumption.

apply HPP'. assumption. Qed.

Theorem hoare_consequence_pre : forall (P P' Q : Assertion) c,

{{P'}} c {{Q}} ->

(forall st, P st -> P' st) ->

{{P}} c {{Q}}.

Proof.

intros P P' Q c Hhoare Himp.

apply hoare_consequence with (P' := P') (Q' := Q);

try assumption.

intros st H. apply H. Qed.

Theorem hoare_consequence_post : forall (P Q Q' : Assertion) c,

{{P}} c {{Q'}} ->

(forall st, Q' st -> Q st) ->

{{P}} c {{Q}}.

Proof.

intros P Q Q' c Hhoare Himp.

apply hoare_consequence with (P' := P) (Q' := Q');

try assumption.

intros st H. apply H. Qed.

For example, we might use (the "_pre" version of) the
consequence rule like this:

{{ True }} =>

{{ 1 = 1 }}

X ::= 1

{{ X = 1 }}

Or, formally...
{{ 1 = 1 }}

X ::= 1

{{ X = 1 }}

Example hoare_asgn_example1 :

{{fun st => True}} (X ::= (ANum 1)) {{fun st => st X = 1}}.

Proof.

apply hoare_consequence_pre

with (P' := assn_sub X (ANum 1) (fun st => st X = 1)).

apply hoare_asgn.

intros st H. unfold assn_sub. apply update_eq. Qed.

### Digression: The eapply Tactic

Example hoare_asgn_example1' :

{{fun st => True}} (X ::= (ANum 1)) {{fun st => st X = 1}}.

Proof.

eapply hoare_consequence_pre.

apply hoare_asgn.

intros st H. unfold assn_sub.

apply update_eq. Qed.

In general, eapply H tactic works just like apply H
except that, instead of failing if unifying the goal with the
conclusion of H does not determine how to instantiate all
of the variables appearing in the premises of H, eapply H
will replace these variables with
There is also an eassumption tactic that works similarly.
Since SKIP doesn't change the state, it preserves any
property P:

*existential variables*(written ?nnn) as placeholders for expressions that will be determined (by further unification) later in the proof.### Skip

{{ P }} SKIP {{ P }} |

Theorem hoare_skip : forall P,

{{P}} SKIP {{P}}.

Proof.

unfold hoare_triple. intros P st st' H HP. inversion H. subst.

assumption. Qed.

{{P}} SKIP {{P}}.

Proof.

unfold hoare_triple. intros P st st' H HP. inversion H. subst.

assumption. Qed.

### Sequencing

{{ P }} c1 {{ Q }} | |

{{ Q }} c2 {{ R }} | |

{{ P }} c1;c2 {{ R }} |

Theorem hoare_seq : forall P Q R c1 c2,

{{Q}} c2 {{R}} ->

{{P}} c1 {{Q}} ->

{{P}} c1;c2 {{R}}.

Proof.

unfold hoare_triple.

intros P Q R c1 c2 H1 H2 st st' H12 Pre.

inversion H12; subst.

apply (H1 st'0 st'); try assumption.

apply (H2 st st'0); try assumption. Qed.

{{Q}} c2 {{R}} ->

{{P}} c1 {{Q}} ->

{{P}} c1;c2 {{R}}.

Proof.

unfold hoare_triple.

intros P Q R c1 c2 H1 H2 st st' H12 Pre.

inversion H12; subst.

apply (H1 st'0 st'); try assumption.

apply (H2 st st'0); try assumption. Qed.

Note that, in the formal rule hoare_seq, the premises are
given in "backwards" order (c2 before c1). This matches
the natural flow of information in many of the situations
where we'll use the rule.
Informally, a nice way of recording a proof using this rule
is as a "decorated program" where the intermediate assertion
Q is written between c1 and c2:

{{ a = n }}

X ::= a;

{{ X = n }} <---- Q

SKIP

{{ X = n }}

X ::= a;

{{ X = n }} <---- Q

SKIP

{{ X = n }}

Example hoare_asgn_example3 : forall a n,

{{fun st => aeval st a = n}}

(X ::= a; SKIP)

{{fun st => st X = n}}.

Proof.

intros a n. eapply hoare_seq.

Case "right part of seq".

apply hoare_skip.

Case "left part of seq".

eapply hoare_consequence_pre. apply hoare_asgn.

intros st H. unfold assn_sub. subst. apply update_eq. Qed.

{{fun st => aeval st a = n}}

(X ::= a; SKIP)

{{fun st => st X = n}}.

Proof.

intros a n. eapply hoare_seq.

Case "right part of seq".

apply hoare_skip.

Case "left part of seq".

eapply hoare_consequence_pre. apply hoare_asgn.

intros st H. unfold assn_sub. subst. apply update_eq. Qed.

#### Exercise: 2 stars (hoare_asgn_example4)

Translate this decorated program into a formal proof:
{{ True }} =>

{{ 1 = 1 }}

X ::= 1;

{{ X = 1 }} =>

{{ X = 1 /\ 2 = 2 }}

Y ::= 2

{{ X = 1 /\ Y = 2 }}

{{ 1 = 1 }}

X ::= 1;

{{ X = 1 }} =>

{{ X = 1 /\ 2 = 2 }}

Y ::= 2

{{ X = 1 /\ Y = 2 }}

Example hoare_asgn_example4 :

{{fun st => True}} (X ::= (ANum 1); Y ::= (ANum 2))

{{fun st => st X = 1 /\ st Y = 2}}.

Proof.

(* FILL IN HERE *) Admitted.

{{fun st => True}} (X ::= (ANum 1); Y ::= (ANum 2))

{{fun st => st X = 1 /\ st Y = 2}}.

Proof.

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 3 stars, optional (swap_exercise)

Write an IMP program c that swaps the values of X and Y and show (in Coq) that it satisfies the following specification:
{{X <= Y}} c {{Y <= X}}

(* FILL IN HERE *)

☐

#### Exercise: 3 stars, optional (hoarestate1)

Explain why the following proposition can't be proven:
forall (a : aexp) (n : nat),

{{fun st => aeval st a = n}} (X ::= (ANum 3); Y ::= a)

{{fun st => st Y = n}}.

{{fun st => aeval st a = n}} (X ::= (ANum 3); Y ::= a)

{{fun st => st Y = n}}.

(* FILL IN HERE *)

☐
What sort of rule do we want for reasoning about conditional
commands? Certainly, if the same assertion Q holds after
executing either branch, then it holds after the whole
conditional. So we might be tempted to write:

However, this is rather weak. For example, using this rule,
we cannot show that:
But, actually, we can say something more precise. In the
"then" branch, we know that the boolean expression b
evaluates to true, and in the "else" branch, we know it
evaluates to false. Making this information available in
the premises of the lemma gives us more information to work
with when reasoning about the behavior of c1 and c2 (i.e.,
the reasons why they establish the postcondtion Q).

To interpret this rule formally, we need to do a little work.
Strictly speaking, what we've written -- P /\ b -- is the
conjunction of an assertion and a boolean expression, which
doesn't typecheck. To fix this, we need a way of formally
"lifting" any bexp b to an assertion. We'll write bassn
b for the assertion "b evaluates to true in (a given
state)."

### Conditionals

{{P}} c1 {{Q}} | |

{{P}} c2 {{Q}} | |

{{P}} IFB b THEN c1 ELSE c2 {{Q}} |

{{True}}

IFB X == 0

THEN Y ::= 2

ELSE Y ::= X + 1

FI

{{ X <= Y }}

since the rule tells us nothing about the state in which the
assignments take place in the then- and else- branches.
IFB X == 0

THEN Y ::= 2

ELSE Y ::= X + 1

FI

{{ X <= Y }}

{{P /\ b}} c1 {{Q}} | |

{{P /\ ~b}} c2 {{Q}} | |

{{P}} IFB b THEN c1 ELSE c2 FI {{Q}} |

A couple of useful facts about bassn:

Lemma bexp_eval_true : forall b st,

beval st b = true -> (bassn b) st.

Proof.

intros b st Hbe.

unfold bassn. assumption. Qed.

Lemma bexp_eval_false : forall b st,

beval st b = false -> ~ ((bassn b) st).

Proof.

intros b st Hbe contra.

unfold bassn in contra.

rewrite -> contra in Hbe. inversion Hbe. Qed.

Now we can formalize the Hoare proof rule for conditionals
(and prove it correct).

Theorem hoare_if : forall P Q b c1 c2,

{{fun st => P st /\ bassn b st}} c1 {{Q}} ->

{{fun st => P st /\ ~(bassn b st)}} c2 {{Q}} ->

{{P}} (IFB b THEN c1 ELSE c2 FI) {{Q}}.

Proof.

unfold hoare_triple.

intros P Q b c1 c2 HTrue HFalse st st' HE HP.

inversion HE; subst.

Case "b is true".

apply (HTrue st st').

assumption.

split. assumption.

apply bexp_eval_true. assumption.

Case "b is false".

apply (HFalse st st').

assumption.

split. assumption.

apply bexp_eval_false. assumption. Qed.

Here is a formal proof that the program we used to motivate the
rule satisfies the specification we gave.

Example if_example :

{{fun st => True}}

(IFB (BEq (AId X) (ANum 0))

THEN (Y ::= (ANum 2))

ELSE (Y ::= APlus (AId X) (ANum 1))

FI)

{{fun st => st X <= st Y}}.

Proof.

apply hoare_if.

Case "Then".

eapply hoare_consequence_pre. apply hoare_asgn.

unfold bassn, assn_sub, update. simpl. intros.

inversion H.

assert (st X = 0) as Heqz

by (apply beq_nat_eq; symmetry; assumption).

rewrite -> Heqz.

apply le_S; apply le_S; apply le_n.

Case "Else".

eapply hoare_consequence_pre. apply hoare_asgn.

unfold assn_sub, update; simpl; intros.

rewrite plus_comm; simpl; apply le_S; apply le_n.

Qed.

### Loops

WHILE b DO c END

and we want to find a pre-condition P and a post-condition
Q such that
{{P}} WHILE b DO c END {{Q}}

is a valid triple.
{{P}} WHILE b DO c END {{P}}.

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:
{{P}} WHILE b DO c END {{P /\ ~b}}

What about the case where the loop body *does*get executed? In order to ensure that P holds when the loop finally exits, we certainly need to make sure that the command c guarantees that P holds whenever c is finished. Moreover, since P holds at the beginning of the first execution of c, and since each execution of c re-establishes P when it finishes, we can always assume that P holds at the beginning of c. This leads us to the following rule:

{{P}} c {{P}} | |

{{P}} WHILE b DO c END {{P /\ ~b}} |

*invariant*.

{{P /\ b}} c {{P}} | |

{{P}} WHILE b DO c END {{P /\ ~b}} |

Lemma hoare_while : forall P b c,

{{fun st => P st /\ bassn b st}} c {{P}} ->

{{P}} (WHILE b DO c END) {{fun st => P st /\ ~ (bassn b st)}}.

Proof.

unfold hoare_triple.

intros P b c Hhoare st st' He HP.

(* Like we've seen before, we need to reason by induction on He,

because in the loop case its hypotheses talk about the

whole loop instead of just c *)

remember (WHILE b DO c END) as wcom.

(ceval_cases (induction He) Case); try (inversion Heqwcom); subst.

Case "E_WhileEnd".

split. assumption. apply bexp_eval_false in H. apply H.

Case "E_WhileLoop".

(* Putting both assumption and reflexivity here seems to make

the proof work in both Coq 8.1 and Coq 8.2 *)

destruct IHHe2 as [HP' Hbfalse']; try assumption; try reflexivity.

apply (Hhoare st st'); try assumption.

split. assumption. apply bexp_eval_true. assumption.

split; assumption. Qed.

## Decorated Programs

*think*when performing a correctness proof in Hoare Logic:

- the intermediate assertion for a sequential composition
c1;c2
- the "inner" assertions P' and Q' in the consequence rules
- the invariant of a while loop
- the outermost pre- and post-conditions.

*decorated program*carries with it an (informal) proof of its own correctness.

- null program:
{{ P }}

SKIP

{{ P }} - sequential composition:
{{ P }}(where c1 and c2 are decorated programs such that the postcondition of c1 is equal to the precondition of c2)

c1;

{{ Q }}

c2

{{ R }} - assignment:
{{ P where a is substituted for V }}

V ::= a

{{ P }} - conditional:
{{ P }}

IFB b THEN

{{ P /\ b }}

c1

ELSE

{{ P /\ ~b }}

c2

FI

{{ Q }}

(where [c1] and [c2] are decorated programs with the

same postcondition [Q] and such that the precondition of [c1] is

[P/\b] and the precondition of [c2] is [P/\~b]) - loop:
{{ P }}(where c1 is a decorated program with precondition P/\b and postcondition P)

WHILE b DO

{{ P /\ b }}

c1

{{ P }}

END

{{ P /\ ~b }} - consequence:
{{ P }} =>(where c is a decorated program with precondition P' and postcondition Q and where P st implies P' st for all states st) or

{{ P' }}

c

{{ Q }}{{ P }}(where c is a decorated program with precondition P and postcondition Q' and where Q' st implies Q st for all states st).

c

{{ Q' }} =>

{{ Q }}

{{ True }} =>

{{ x = x }}

X ::= x;

{{ X = x }} =>

{{ X = x /\ z = z }}

Z ::= z;

{{ X = x /\ Z = z }} =>

{{ Z - X = z - x }}

WHILE X <> 0 DO

{{ Z - X = z - x /\ X <> 0 }} =>

{{ (Z - 1) - (X - 1) = z - x }}

Z ::= Z - 1;

{{ Z - (X - 1) = z - x }}

X ::= X - 1

{{ Z - X = z - x }}

END;

{{ Z - X = z - x /\ ~ (X <> 0) }} =>

{{ Z = z - x }} =>

{{ Z + 1 = z - x + 1 }}

Z ::= Z + 1

{{ Z = z - x + 1 }}

{{ x = x }}

X ::= x;

{{ X = x }} =>

{{ X = x /\ z = z }}

Z ::= z;

{{ X = x /\ Z = z }} =>

{{ Z - X = z - x }}

WHILE X <> 0 DO

{{ Z - X = z - x /\ X <> 0 }} =>

{{ (Z - 1) - (X - 1) = z - x }}

Z ::= Z - 1;

{{ Z - (X - 1) = z - x }}

X ::= X - 1

{{ Z - X = z - x }}

END;

{{ Z - X = z - x /\ ~ (X <> 0) }} =>

{{ Z = z - x }} =>

{{ Z + 1 = z - x + 1 }}

Z ::= Z + 1

{{ Z = z - x + 1 }}

### Exercise: Hoare Rules for REPEAT

#### Exercise: 4 stars (hoare_repeat)

In this exercise, we'll add a new constructor to our language of commands: CRepeat. You will write the evaluation rule for repeat and add a new hoare logic theorem to the language for programs involving it.Inductive com : Type :=

| CSkip : com

| CAss : id -> aexp -> com

| CSeq : com -> com -> com

| CIf : bexp -> com -> com -> com

| CWhile : bexp -> com -> com

| CRepeat : com -> bexp -> com.

REPEAT behaves like WHILE, except that the loop guard is
checked

*after*each execution of the body, with the loop repeating as long as the guard stays*false*. Because of this, the body will always execute at least once.
Tactic Notation "com_cases" tactic(first) tactic(c) :=

first;

[ c "SKIP" | c "::=" | c ";" | c "IFB" | c "WHILE" | c "CRepeat"].

Notation "'SKIP'" :=

CSkip.

Notation "c1 ; c2" :=

(CSeq c1 c2) (at level 80, right associativity).

Notation "V '::=' a" :=

(CAss V a) (at level 60).

Notation "'WHILE' b 'DO' c 'END'" :=

(CWhile b c) (at level 80, right associativity).

Notation "'IFB' e1 'THEN' e2 'ELSE' e3 'FI'" :=

(CIf e1 e2 e3) (at level 80, right associativity).

Notation "'REPEAT' e1 'UNTIL' b2 'END'" :=

(CRepeat e1 b2) (at level 80, right associativity).

first;

[ c "SKIP" | c "::=" | c ";" | c "IFB" | c "WHILE" | c "CRepeat"].

Notation "'SKIP'" :=

CSkip.

Notation "c1 ; c2" :=

(CSeq c1 c2) (at level 80, right associativity).

Notation "V '::=' a" :=

(CAss V a) (at level 60).

Notation "'WHILE' b 'DO' c 'END'" :=

(CWhile b c) (at level 80, right associativity).

Notation "'IFB' e1 'THEN' e2 'ELSE' e3 'FI'" :=

(CIf e1 e2 e3) (at level 80, right associativity).

Notation "'REPEAT' e1 'UNTIL' b2 'END'" :=

(CRepeat e1 b2) (at level 80, right associativity).

Add new rules for REPEAT to ceval below. You can use the rules
for WHILE as a guide, but remember that the body of a REPEAT
should always execute at least once, and that the loop ends when
the guard becomes true. Then update the ceval_cases tactic to
handle these added cases.

Inductive ceval : state -> com -> state -> Prop :=

| E_Skip : forall st,

ceval st SKIP st

| E_Ass : forall st a1 n V,

aeval st a1 = n ->

ceval st (V ::= a1) (update st V n)

| E_Seq : forall c1 c2 st st' st'',

ceval st c1 st' ->

ceval st' c2 st'' ->

ceval st (c1 ; c2) st''

| E_IfTrue : forall st st' b1 c1 c2,

beval st b1 = true ->

ceval st c1 st' ->

ceval st (IFB b1 THEN c1 ELSE c2 FI) st'

| E_IfFalse : forall st st' b1 c1 c2,

beval st b1 = false ->

ceval st c2 st' ->

ceval st (IFB b1 THEN c1 ELSE c2 FI) st'

| E_WhileEnd : forall b1 st c1,

beval st b1 = false ->

ceval st (WHILE b1 DO c1 END) st

| E_WhileLoop : forall st st' st'' b1 c1,

beval st b1 = true ->

ceval st c1 st' ->

ceval st' (WHILE b1 DO c1 END) st'' ->

ceval st (WHILE b1 DO c1 END) st''

(* FILL IN HERE *)

.

Tactic Notation "ceval_cases" tactic(first) tactic(c) := first; [

c "E_Skip" | c "E_Ass" | c "E_Seq" | c "E_IfTrue" | c "E_IfFalse"

| c "E_WhileEnd" | c "E_WhileLoop"

(* FILL IN HERE *)

].

A couple of definitions from above, copied here so they use the
new ceval.

Notation "c1 '/' st '==>' st'" := (ceval st c1 st') (at level 40, st at level 39).

Definition hoare_triple (P:Assertion) (c:com) (Q:Assertion) : Prop :=

forall st st', (c / st ==> st') -> P st -> Q st'.

Notation "{{ P }} c {{ Q }}" := (hoare_triple P c Q) (at level 90).

Now state and prove a theorem, hoare_repeat, that expresses an
appropriate proof rule for repeat commands. Use hoare_while
as a model.

☐
Formal Hoare-logic proofs often require a bunch of small algebraic
facts, most of which we wouldn't even bother writing down in an
informal proof. This is a bit clunky in Coq (though it can be
improved quite a bit using some of the automation features we
haven't discussed yet). The best way to deal with it for now is
to break them out as separate lemmas so that they don't clutter
the main proofs. Here we collect a bunch of properties that we'll
use in the examples below.

# Using Hoare Logic to Reason About Programs

## Miscellaneous Lemmas

Lemma neq0_not_true__eq_0 : forall x,

negb (beq_nat x 0) <> true -> x = 0.

Proof.

intros x H. destruct x as [| x'].

Case "x = 0".

reflexivity.

Case "x = S x'".

simpl in H. destruct H. reflexivity.

Qed.

Lemma neq0_true__eq_S : forall n,

negb (beq_nat n 0) = true ->

exists n', n = S n'.

Proof.

intros n H. destruct n as [| n'].

Case "n = 0 (contradiction)".

inversion H.

Case "n = S n'".

exists n'. reflexivity.

Qed.

Lemma S_le__S: forall n m,

S n <= m ->

exists m', n <= m /\ m = S m'.

Proof.

intros n m H. destruct m as [| m'].

Case "m = 0 (contradiction)".

inversion H.

Case "m = S m'".

exists m'. split; try reflexivity.

apply le_S. apply le_S_n. apply H. Qed.

Lemma not_ev_ev_S_gen: forall n,

(~ ev n -> ev (S n)) /\

(~ ev (S n) -> ev (S (S n))).

Proof.

induction n as [| n'].

Case "n = 0".

split; intros H.

SCase "->".

destruct H. apply ev_0.

SCase "<-".

apply ev_SS. apply ev_0.

Case "n = S n'".

destruct IHn' as [Hn HSn]. split; intros H.

SCase "->".

apply HSn. apply H.

SCase "<-".

apply ev_SS. apply Hn. intros contra.

destruct H. apply ev_SS. apply contra. Qed.

Lemma not_ev_ev_S : forall n,

~ ev n -> ev (S n).

Proof.

intros n.

destruct (not_ev_ev_S_gen n) as [H _].

apply H.

Qed.

## Example: Slow subtraction

{{ X = x /\ Z = z }} =>

{{ Z - X = z - x }}

WHILE X <> 0 DO

{{ Z - X = z - x /\ X <> 0 }} =>

{{ (Z - 1) - (X - 1) = z - x }}

Z ::= Z - 1;

{{ Z - (X - 1) = z - x }}

X ::= X - 1

{{ Z - X = z - x }}

END

{{ Z - X = z - x /\ ~ (X <> 0) }} =>

{{ Z = z - x }}

{{ Z - X = z - x }}

WHILE X <> 0 DO

{{ Z - X = z - x /\ X <> 0 }} =>

{{ (Z - 1) - (X - 1) = z - x }}

Z ::= Z - 1;

{{ Z - (X - 1) = z - x }}

X ::= X - 1

{{ Z - X = z - x }}

END

{{ Z - X = z - x /\ ~ (X <> 0) }} =>

{{ Z = z - x }}

Definition subtract_slowly : com :=

WHILE BNot (BEq (AId X) (ANum 0)) DO

Z ::= AMinus (AId Z) (ANum 1);

X ::= AMinus (AId X) (ANum 1)

END.

Definition subtract_slowly_invariant x z :=

fun st => minus (st Z) (st X) = minus z x.

Theorem subtract_slowly_correct : forall x z,

{{fun st => st X = x /\ st Z = z}}

subtract_slowly

{{fun st => st Z = minus z x}}.

Proof.

(* Note that we do NOT unfold the definition of hoare_triple

anywhere in this proof! The goal is to use only the hoare

rules. Your proofs should do the same. *)

intros x z. unfold subtract_slowly.

(* First we need to transform the pre and postconditions so

that hoare_while will apply. In particular, the

precondition should be the loop invariant. *)

eapply hoare_consequence with (P' := subtract_slowly_invariant x z).

apply hoare_while.

Case "Loop body preserves invariant".

(* Split up the two assignments with hoare_seq - using eapply

lets us solve the second one immediately with hoare_asgn *)

eapply hoare_seq. apply hoare_asgn.

(* Now for the first assignment, transform the precondition

so we can use hoare_asgn *)

eapply hoare_consequence_pre. apply hoare_asgn.

(* Finally, we need to justify the implication generated by

hoare_consequence_pre (this bit of reasoning is elided in the

informal proof) *)

unfold subtract_slowly_invariant, assn_sub, update, bassn. simpl.

intros st [Inv GuardTrue]. apply neq0_true__eq_S in GuardTrue.

destruct GuardTrue as [n' Hn'].

rewrite Hn'. simpl. rewrite Hn' in Inv.

omega.

Case "Initial state satisfies invariant".

(* This is the subgoal generated by the precondition part of our

first use of hoare_consequence. It's the first implication

written in the decorated program (though we elided the actual

proof there). *)

unfold subtract_slowly_invariant.

intros st [HX HZ].

rewrite <- HX. rewrite HZ. reflexivity.

Case "Invariant and negated guard imply postcondition".

(* This is the subgoal generated by the postcondition part of

out first use of hoare_consequence. This implication is

the one written after the while loop in the informal proof. *)

intros st [Inv GuardFalse].

unfold subtract_slowly_invariant in Inv.

unfold bassn in GuardFalse. simpl in GuardFalse.

apply neq0_not_true__eq_0 in GuardFalse.

(* Here's another good use of the omega tactic: *)

omega. Qed.

## Exercise: Reduce to zero

{{ True }}

WHILE X <> 0 DO

{{ True /\ X <> 0 }} =>

{{ True }}

X ::= X - 1

{{ True }}

END

{{ True /\ X = 0 }} =>

{{ X = 0 }}

Your job is to translate this proof to Coq. It may help to look
at the slow_subtraction proof for ideas.
WHILE X <> 0 DO

{{ True /\ X <> 0 }} =>

{{ True }}

X ::= X - 1

{{ True }}

END

{{ True /\ X = 0 }} =>

{{ X = 0 }}

#### Exercise: 2 stars (reduce_to_zero_correct)

Definition reduce_to_zero : com :=

WHILE BNot (BEq (AId X) (ANum 0)) DO

X ::= AMinus (AId X) (ANum 1)

END.

Theorem reduce_to_zero_correct :

{{fun st => True}}

reduce_to_zero

{{fun st => st X = 0}}.

Proof.

(* FILL IN HERE *) Admitted.

WHILE BNot (BEq (AId X) (ANum 0)) DO

X ::= AMinus (AId X) (ANum 1)

END.

Theorem reduce_to_zero_correct :

{{fun st => True}}

reduce_to_zero

{{fun st => st X = 0}}.

Proof.

(* FILL IN HERE *) Admitted.

☐
The following program adds the variable X into the variable Z
by repeatedly decrementing X and incrementing Z.

## Exercise: Slow addition

Definition add_slowly : com :=

WHILE BNot (BEq (AId X) (ANum 0)) DO

Z ::= APlus (AId Z) (ANum 1);

X ::= AMinus (AId X) (ANum 1)

END.

#### Exercise: 3 stars (add_slowly_decoration)

Following the pattern of the subtract_slowly example above, pick a precondition and postcondition that give an appropriate specification of add_slowly; then (informally) decorate the program accordingly.(* FILL IN HERE *)

☐

#### Exercise: 3 stars (add_slowly_formal)

Now write down your specification of add_slowly formally, as a Coq Hoare_triple, and prove it valid.
(* FILL IN HERE *)

☐
Here's another, slightly trickier example. Make sure you
understand the decorated program completely. Understanding
all the details of the Coq proof is not required, though it
is not actually very hard -- all the required ideas are
already in the informal version, and all the required
miscellaneous facts about arithmetic are recorded above.

## Example: Parity

{{ X = x }} =>

{{ X = x /\ 0 = 0 }}

Y ::= 0;

{{ X = x /\ Y = 0 }} =>

{{ (Y=0 <-> ev (x-X)) /\ X<=x }}

WHILE X <> 0 DO

{{ (Y=0 <-> ev (x-X)) /\ X<=x /\ X<>0 }} =>

{{ (1-Y)=0 <-> ev (x-(X-1)) /\ X-1<=x }}

Y ::= 1 - Y;

{{ Y=0 <-> ev (x-(X-1)) /\ X-1<=x }}

X ::= X - 1

{{ Y=0 <-> ev (x-X) /\ X<=x }}

END

{{ (Y=0 <-> ev (x-X)) /\ X<=x /\ ~(X<>0) }} =>

{{ Y=0 <-> ev x }}

{{ X = x /\ 0 = 0 }}

Y ::= 0;

{{ X = x /\ Y = 0 }} =>

{{ (Y=0 <-> ev (x-X)) /\ X<=x }}

WHILE X <> 0 DO

{{ (Y=0 <-> ev (x-X)) /\ X<=x /\ X<>0 }} =>

{{ (1-Y)=0 <-> ev (x-(X-1)) /\ X-1<=x }}

Y ::= 1 - Y;

{{ Y=0 <-> ev (x-(X-1)) /\ X-1<=x }}

X ::= X - 1

{{ Y=0 <-> ev (x-X) /\ X<=x }}

END

{{ (Y=0 <-> ev (x-X)) /\ X<=x /\ ~(X<>0) }} =>

{{ Y=0 <-> ev x }}

Lemma minus_pred : forall n m,

(exists m', m = S m') ->

m <= n ->

minus n (pred m) = S (minus n m).

Proof.

intros n m Hnot0.

destruct Hnot0 as [m' Heq]. rewrite Heq in *.

clear Heq m. revert n.

induction m' as [| m'']; intros n Hle.

Case "m' = 0".

simpl. destruct n. inversion Hle. omega.

Case "m' = S m''".

simpl. simpl in IHm''.

destruct n as [| n'].

SCase "n = 0". inversion Hle.

SCase "n = S n'".

simpl. apply IHm''. apply le_S_n. assumption.

Qed.

Definition find_parity : com :=

Y ::= (ANum 0);

WHILE (BNot (BEq (AId X) (ANum 0))) DO

Y ::= AMinus (ANum 1) (AId Y);

X ::= AMinus (AId X) (ANum 1)

END.

Definition find_parity_invariant x :=

fun st =>

st X <= x

/\ (st Y = 0 /\ev (x - st X) \/ st Y = 1 /\ ~ev (x - st X)).

Theorem find_parity_correct : forall x,

{{fun st => st X = x}}

find_parity

{{fun st => st Y = 0 <-> ev x}}.

Proof.

intros x. unfold find_parity.

apply hoare_seq with (Q := find_parity_invariant x).

eapply hoare_consequence.

apply hoare_while with (P := find_parity_invariant x).

Case "Loop body preserves invariant".

eapply hoare_seq.

apply hoare_asgn.

eapply hoare_consequence_pre.

apply hoare_asgn.

intros st [[Inv1 Inv2] GuardTrue].

apply neq0_true__eq_S in GuardTrue.

destruct GuardTrue as [X' HX'].

unfold find_parity_invariant, bassn, assn_sub, aeval in *.

rewrite update_eq.

rewrite (update_neq Y X); auto.

rewrite (update_neq X Y); auto.

rewrite update_eq.

rewrite HX' in *; clear HX'.

split. omega.

destruct Inv2 as [[H1 H2] | [H1 H2]]; [right|left]; (split; [omega |]).

replace (S X' - 1) with X' by omega.

apply ev_not_ev_S in H2.

replace (S (x - S X')) with (x-X') in H2 by omega.

auto.

replace (S X' - 1) with X' by omega.

apply not_ev_ev_S in H2.

replace (S (x - S X')) with (x - X') in H2 by omega.

assumption.

Case "Precondition implies invariant".

intros st H. assumption.

Case "Invariant implies postcondition".

unfold bassn, find_parity_invariant. simpl.

intros st [[Inv1 Inv2] GuardFalse].

apply neq0_not_true__eq_0 in GuardFalse.

rewrite GuardFalse in Inv2.

rewrite <- minus_n_O in *.

intuition. (* what a nice tactic! *)

rewrite H0 in H. inversion H.

Case "invariant established before loop".

eapply hoare_consequence_pre.

apply hoare_asgn.

intros st H.

unfold assn_sub, find_parity_invariant, update. simpl.

subst.

split.

apply le_n.

rewrite (minus_diag (st X)).

left. split. reflexivity.

apply ev_0. Qed.

#### Exercise: 3 stars (wrong_find_parity_invariant)

A plausible first attempt at stating an invariant for find_parity is the following.
Why doesn't this work? (Hint: Don't waste time trying to answer
this exercise by attempting a formal proof and seeing where it
goes wrong. Just think about whether the loop body actually
preserves the property.)

(* FILL IN HERE *)

Definition sqrt_loop : com :=

WHILE BLe (AMult (APlus (ANum 1) (AId Z)) (APlus (ANum 1) (AId Z))) (AId X) DO

Z ::= APlus (ANum 1) (AId Z)

END.

Definition sqrt_com : com :=

Z ::= ANum 0;

sqrt_loop.

Definition sqrt_spec (x : nat) : Assertion :=

fun st =>

((st Z) * (st Z)) <= x

/\ ~ (((S (st Z)) * (S (st Z))) <= x).

Definition sqrt_inv (x : nat) : Assertion :=

fun st =>

st X = x

/\ ((st Z) * (st Z)) <= x.

Theorem random_fact_1 : forall st,

(S (st Z)) * (S (st Z)) <= st X ->

bassn (BLe (AMult (APlus (ANum 1) (AId Z)) (APlus (ANum 1) (AId Z))) (AId X)) st.

Proof.

intros st Hle. unfold bassn. simpl.

destruct (st X) as [|x'].

Case "st X = 0".

inversion Hle.

Case "st X = S x'".

simpl in Hle. apply le_S_n in Hle.

remember (ble_nat (plus (st Z) ((st Z) * (S (st Z)))) x')

as ble.

destruct ble. reflexivity.

symmetry in Heqble. apply ble_nat_false in Heqble.

unfold not in Heqble. apply Heqble in Hle. destruct Hle.

Qed.

Theorem random_fact_2 : forall st,

bassn (BLe (AMult (APlus (ANum 1) (AId Z)) (APlus (ANum 1) (AId Z))) (AId X)) st ->

(aeval st (APlus (ANum 1) (AId Z))) * (aeval st (APlus (ANum 1) (AId Z))) <= st X.

Proof.

intros st Hble. unfold bassn in Hble. simpl in *.

destruct (st X) as [| x'].

Case "st X = 0".

inversion Hble.

Case "st X = S x'".

apply ble_nat_true in Hble. omega. Qed.

Theorem sqrt_com_correct : forall x,

{{fun st => True}} (X ::= ANum x; sqrt_com) {{sqrt_spec x}}.

Proof.

intros x.

apply hoare_seq with (Q := fun st => st X = x).

Case "sqrt_com".

unfold sqrt_com.

apply hoare_seq with (Q := fun st => st X = x /\ st Z = 0).

SCase "sqrt_loop".

unfold sqrt_loop.

eapply hoare_consequence.

apply hoare_while with (P := sqrt_inv x).

SSCase "loop preserves invariant".

eapply hoare_consequence_pre.

apply hoare_asgn. intros st H.

unfold assn_sub. unfold sqrt_inv in *.

destruct H as [[HX HZ] HP]. split.

SSSCase "X is preserved".

rewrite update_neq; auto.

SSSCase "Z is updated correctly".

rewrite (update_eq (aeval st (APlus (ANum 1) (AId Z))) Z st).

subst. apply random_fact_2. assumption.

SSCase "invariant is true initially".

intros st H. destruct H as [HX HZ].

unfold sqrt_inv. split. assumption.

rewrite HZ. simpl. omega.

SSCase "after loop, spec is satisfied".

intros st H. unfold sqrt_spec.

destruct H as [HX HP].

unfold sqrt_inv in HX. destruct HX as [HX Harith].

split. assumption.

intros contra. apply HP. clear HP.

simpl. simpl in contra.

apply random_fact_1. subst x. assumption.

SCase "Z set to 0".

eapply hoare_consequence_pre. apply hoare_asgn.

intros st HX.

unfold assn_sub. split.

rewrite update_neq; auto.

apply update_eq.

Case "assignment of X".

eapply hoare_consequence_pre. apply hoare_asgn.

intros st H.

unfold assn_sub. apply update_eq. Qed.

#### Exercise: 3 stars, optional (sqrt_informal)

Write a decorated program corresponding to the above correctness proof.(* FILL IN HERE *)

Module Factorial.

Fixpoint real_fact (n:nat) : nat :=

match n with

| O => 1

| S n' => n * (real_fact n')

end.

Recall the factorial Imp program:

Definition fact_body : com :=

Y ::= AMult (AId Y) (AId Z);

Z ::= AMinus (AId Z) (ANum 1).

Definition fact_loop : com :=

WHILE BNot (BEq (AId Z) (ANum 0)) DO

fact_body

END.

Definition fact_com : com :=

Z ::= (AId X);

Y ::= ANum 1;

fact_loop.

#### Exercise: 3 stars, optional (fact_informal)

Decorate the fact_com program to show that it satisfies the specification given by the pre and postconditions below. Just as we have done above, you may elide the algebraic reasoning about arithmetic, the less-than relation, etc., that is (formally) required by the rule of consequence:
{{ X = x }}

Z ::= X;

Y ::= 1;

WHILE Z <> 0 DO

Y ::= Y * Z;

Z ::= Z - 1

END

{{ Y = real_fact x }}

☐
Z ::= X;

Y ::= 1;

WHILE Z <> 0 DO

Y ::= Y * Z;

Z ::= Z - 1

END

{{ Y = real_fact x }}

#### Exercise: 4 stars, optional (fact_formal)

Prove formally that fact_com satisfies this specification, using your informal proof as a guide. You may want to state the loop invariant separately (as we did in the examples).Theorem fact_com_correct : forall x,

{{fun st => st X = x}} fact_com

{{fun st => st Y = real_fact x}}.

Proof.

(* FILL IN HERE *) Admitted.

☐