# HoareHoare Logic, Part I

Require Export Imp.

What we've done so far:
This chapter:

- Formalized Imp
- identifiers and states
- abstract syntax trees
- evaluation functions (for aexps and bexps)
- evaluation relation (for commands)

- Proved some
*metatheoretic*properties- determinism of evaluation
- equivalence of some different ways of writing down the definitions (e.g. functional and relational definitions of arithmetic expression evaluation)
- guaranteed termination of certain classes of programs
- meaning-preservation of some program transformations
- behavioral equivalence of programs (Equiv)

- A systematic method for reasoning about the correctness of particular programs

# Hoare Logic

- a natural notation for
*program specifications* - a
*compositional*proof technique for program correctness

- assertions (Hoare Triples)
- proof rules
- decorated programs
- loop invariants
- examples

Definition Assertion := state → Prop.

Paraphrase the following assertions in English
(1) fun st ⇒ st X = 3
(2) fun st ⇒ st X ≤ st Y
(3) fun st ⇒ st X = 3 ∨ st X ≤ st Y
(4) fun st ⇒ st Z × st Z ≤ st X ∧
¬ (((S (st Z)) × (S (st Z))) ≤ st X)
(5) fun st ⇒ True
(6) fun st ⇒ False

Informally, instead of writing
Given two assertions P and Q, we say that P

fun st ⇒ (st Z) × (st Z) ≤ m ∧

¬ ((S (st Z)) × (S (st Z)) ≤ m)

we'll write just
¬ ((S (st Z)) × (S (st Z)) ≤ m)

Z × Z ≤ m ∧ ~((S Z) × (S Z) ≤ m).

*implies*Q, written P ⇾ Q (in ASCII, P ->> Q), if, whenever P holds in some state st, Q also holds.Definition assert_implies (P Q : Assertion) : Prop :=

∀st, P st → Q st.

Notation "P ⇾ Q" :=

(assert_implies P Q) (at level 80) : hoare_spec_scope.

Open Scope hoare_spec_scope.

We'll also have occasion to use the "iff" variant of implication
between assertions:

Notation "P ⇿ Q" :=

(P ⇾ Q ∧ Q ⇾ P) (at level 80) : hoare_spec_scope.

## Hoare Triples

- "If command c is started in a state satisfying assertion P, and if c eventually terminates in some final state, then this final state will satisfy the assertion Q."

*Hoare Triple*. The property P is called the

*precondition*of c, while Q is the

*postcondition*. Formally:

Definition hoare_triple

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

∀st st',

c / st ⇓ st' →

P st →

Q st'.

Since we'll be working a lot with Hoare triples, it's useful to
have a compact notation:

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

Notation "{{ P }} c {{ Q }}" :=

(hoare_triple P c Q) (at level 90, c at next level)

: hoare_spec_scope.

Paraphrase the following Hoare triples in English.

1) {{True}} c {{X = 5}}

2) {{X = m}} c {{X = m + 5)}}

3) {{X ≤ Y}} c {{Y ≤ X}}

4) {{True}} c {{False}}

5) {{X = m}}

c

{{Y = real_fact m}}.

6) {{True}}

c

{{(Z × Z) ≤ m ∧ ¬ (((S Z) × (S Z)) ≤ m)}}

2) {{X = m}} c {{X = m + 5)}}

3) {{X ≤ Y}} c {{Y ≤ X}}

4) {{True}} c {{False}}

5) {{X = m}}

c

{{Y = real_fact m}}.

6) {{True}}

c

{{(Z × Z) ≤ m ∧ ¬ (((S Z) × (S Z)) ≤ m)}}

Is the following Hoare triple
(1) Yes
(2) No

*valid*— i.e., the claimed relation between P, c, and Q is true?
{{True}} X ::= 5 {{X = 5}}

What about this one?
(1) Yes
(2) No

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

What about this one?
(1) Yes
(2) No

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

What about this one?
(1) Yes
(2) No

{{X = 2 ∧ X = 3}} X ::= 5 {{X = 0}}

What about this one?
(1) Yes
(2) No

{{True}} SKIP {{False}}

What about this one?
(1) Yes
(2) No

{{False}} SKIP {{True}}

What about this one?
(1) Yes
(2) No

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

What about this one?
(1) Yes
(2) No

{{X = 0}}

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

{{X = 1}}

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

{{X = 1}}

What about this one?
(1) Yes
(2) No

{{X = 1}}

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

{{X = 100}}

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

{{X = 100}}

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

(∀st, Q st) →

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

Proof.

intros P Q c H. unfold hoare_triple.

intros st st' Heval HP.

apply H. Qed.

intros P Q c H. unfold hoare_triple.

intros st st' Heval HP.

apply H. Qed.

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

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

inversion HP. Qed.

intros P Q c H. unfold hoare_triple.

intros st st' Heval HP.

unfold not in H. apply H in HP.

inversion HP. Qed.

## Proof Rules

- introduce one "proof rule" for each Imp syntactic form
- plus a couple of "structural rules" that help glue proofs together
- prove programs correct using these proof rules, without ever unfolding the definition of hoare_triple

### Assignment

{{ 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.
*any*arithmetic expression, then

{{ a = 1 }} X ::= a {{ X = 1 }}

is a valid Hoare triple.
*arbitrary*property Q holds after X ::= a, we need to assume that Q holds before X ::= a, but

*with all occurrences of*X replaced by a in Q. This leads to the Hoare rule for assignment

{{ Q [X ↦ a] }} X ::= a {{ Q }}

where "Q [X ↦ a]" is pronounced "Q where a is substituted
for X".
{{ (X ≤ 5) [X ↦ X + 1]

i.e., X + 1 ≤ 5 }}

X ::= X + 1

{{ X ≤ 5 }}

{{ (X = 3) [X ↦ 3]

i.e., 3 = 3}}

X ::= 3

{{ X = 3 }}

{{ (0 ≤ X ∧ X ≤ 5) [X ↦ 3]

i.e., (0 ≤ 3 ∧ 3 ≤ 5)}}

X ::= 3

{{ 0 ≤ X ∧ X ≤ 5 }}

i.e., X + 1 ≤ 5 }}

X ::= X + 1

{{ X ≤ 5 }}

{{ (X = 3) [X ↦ 3]

i.e., 3 = 3}}

X ::= 3

{{ X = 3 }}

{{ (0 ≤ X ∧ X ≤ 5) [X ↦ 3]

i.e., (0 ≤ 3 ∧ 3 ≤ 5)}}

X ::= 3

{{ 0 ≤ X ∧ X ≤ 5 }}

Definition assn_sub X a P : Assertion :=

fun (st : state) ⇒

P (update st X (aeval st a)).

Notation "P [ X |-> a ]" := (assn_sub X a P) (at level 10).

That is, P [X ↦ a] is an assertion P' that is just like P
except that, wherever P looks up the variable X in the current
state, P' instead uses the value of the expression a.
To see how this works, let's calculate what happens with a couple
of examples. First, suppose P' is (X ≤ 5) [X ↦ 3] — that
is, more formally, P' is the Coq expression
For a more interesting example, suppose P' is (X ≤ 5) [X ↦
X+1]. Formally, P' is the Coq expression
Now we can give the precise proof rule for assignment:

We can prove formally that this rule is indeed valid.

fun st ⇒

(fun st' ⇒ st' X ≤ 5)

(update st X (aeval st (ANum 3))),

which simplifies to
(fun st' ⇒ st' X ≤ 5)

(update st X (aeval st (ANum 3))),

fun st ⇒

(fun st' ⇒ st' X ≤ 5)

(update st X 3)

and further simplifies to
(fun st' ⇒ st' X ≤ 5)

(update st X 3)

fun st ⇒

((update st X 3) X) ≤ 5)

and by further simplification to
((update st X 3) X) ≤ 5)

fun st ⇒

(3 ≤ 5).

That is, P' is the assertion that 3 is less than or equal to
5 (as expected).
(3 ≤ 5).

fun st ⇒

(fun st' ⇒ st' X ≤ 5)

(update st X (aeval st (APlus (AId X) (ANum 1)))),

which simplifies to
(fun st' ⇒ st' X ≤ 5)

(update st X (aeval st (APlus (AId X) (ANum 1)))),

fun st ⇒

(((update st X (aeval st (APlus (AId X) (ANum 1))))) X) ≤ 5

and further simplifies to
(((update st X (aeval st (APlus (AId X) (ANum 1))))) X) ≤ 5

fun st ⇒

(aeval st (APlus (AId X) (ANum 1))) ≤ 5.

That is, P' is the assertion that X+1 is at most 5.
(aeval st (APlus (AId X) (ANum 1))) ≤ 5.

(hoare_asgn) | |

{{Q [X ↦ a]}} X ::= a {{Q}} |

Theorem hoare_asgn : ∀Q X a,

{{Q [X ↦ a]}} (X ::= a) {{Q}}.

Proof.

unfold hoare_triple.

intros Q X a st st' HE HQ.

inversion HE. subst.

unfold assn_sub in HQ. assumption. Qed.

unfold hoare_triple.

intros Q X 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 ⇒ st X = 3) [X ↦ ANum 3]}}

(X ::= (ANum 3))

{{fun st ⇒ st X = 3}}.

Proof.

apply hoare_asgn. Qed.

### Consequence

{{(X = 3) [X ↦ 3]}} X ::= 3 {{X = 3}},

follows directly from the assignment rule,
{{True}} X ::= 3 {{X = 3}}.

does not. This triple is valid, but it is not an instance of
hoare_asgn because True and (X = 3) [X ↦ 3] are not
syntactically equal assertions. However, they are logically
equivalent, so if one triple is valid, then the other must
certainly be as well. We might capture this observation with the
following rule:
{{P'}} c {{Q}} | |

P ⇿ P' | (hoare_consequence_pre_equiv) |

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

*Rules of Consequence*.

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

P ⇾ P' | (hoare_consequence_pre) |

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

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

Q' ⇾ Q | (hoare_consequence_post) |

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

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

{{P'}} c {{Q}} →

P ⇾ P' →

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

Proof.

intros P P' Q c Hhoare Himp.

intros st st' Hc HP. apply (Hhoare st st').

assumption. apply Himp. assumption. Qed.

intros P P' Q c Hhoare Himp.

intros st st' Hc HP. apply (Hhoare st st').

assumption. apply Himp. assumption. Qed.

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

{{P}} c {{Q'}} →

Q' ⇾ Q →

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

Proof.

intros P Q Q' c Hhoare Himp.

intros st st' Hc HP.

apply Himp.

apply (Hhoare st st').

assumption. assumption. Qed.

intros P Q Q' c Hhoare Himp.

intros st st' Hc HP.

apply Himp.

apply (Hhoare st st').

assumption. assumption. Qed.

For example, we might use the first 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' := (fun st ⇒ st X = 1) [X ↦ ANum 1]).

apply hoare_asgn.

intros st H. unfold assn_sub, update. simpl. reflexivity.

Qed.

Finally, for convenience in some proofs, we can state a "combined"
rule of consequence that allows us to vary both the precondition
and the postcondition.

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

P ⇾ P' | |

Q' ⇾ Q | (hoare_consequence) |

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

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

{{P'}} c {{Q'}} →

P ⇾ P' →

Q' ⇾ Q →

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

Proof.

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

apply hoare_consequence_pre with (P' := P').

apply hoare_consequence_post with (Q' := Q').

assumption. assumption. assumption. Qed.

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

apply hoare_consequence_pre with (P' := P').

apply hoare_consequence_post with (Q' := Q').

assumption. assumption. assumption. 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. reflexivity. 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 so-called

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

(hoare_skip) | |

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

Theorem hoare_skip : ∀P,

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

Proof.

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

assumption. Qed.

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

assumption. Qed.

### Sequencing

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

{{ Q }} c2 {{ R }} | (hoare_seq) |

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

Theorem hoare_seq : ∀P Q R c1 c2,

{{Q}} c2 {{R}} →

{{P}} c1 {{Q}} →

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

Proof.

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); assumption. Qed.

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); assumption. Qed.

Informally, a nice way of recording a proof using the sequencing
rule is as a "decorated program" where the intermediate assertion
Q is written between c1 and c2:

{{ a = n }}

X ::= a;;

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

SKIP

{{ X = n }}

X ::= a;;

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

SKIP

{{ X = n }}

Example hoare_asgn_example3 : ∀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. subst. reflexivity. Qed.

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. subst. reflexivity. Qed.

### 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}} | (hoare_if) |

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

Definition bassn b : Assertion :=

fun st ⇒ (beval st b = true).

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

Theorem hoare_if : ∀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.

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.

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.

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.

(* WORK IN CLASS *) Admitted.

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

{{P ∧ b}} c {{P}} | (hoare_while) |

{{P}} WHILE b DO c END {{P ∧ ~b}} |

*invariant*of the loop.

*together with the fact that the loop's guard is true*is a sufficient precondition for c to ensure P as a postcondition.

*is*an invariant of the loop

WHILE X = 2 DO X := 1 END

although it is clearly *not*preserved by the body of the loop.

Lemma hoare_while : ∀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.

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 "keep looping" case, its hypotheses

talk about the whole loop instead of just c *)

remember (WHILE b DO c END) as wcom eqn:Heqwcom.

ceval_cases (induction He) Case;

try (inversion Heqwcom); subst; clear Heqwcom.

Case "E_WhileEnd".

split. assumption. apply bexp_eval_false. assumption.

Case "E_WhileLoop".

apply IHHe2. reflexivity.

apply (Hhoare st st'). assumption.

split. assumption. apply bexp_eval_true. assumption.

Qed.

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 "keep looping" case, its hypotheses

talk about the whole loop instead of just c *)

remember (WHILE b DO c END) as wcom eqn:Heqwcom.

ceval_cases (induction He) Case;

try (inversion Heqwcom); subst; clear Heqwcom.

Case "E_WhileEnd".

split. assumption. apply bexp_eval_false. assumption.

Case "E_WhileLoop".

apply IHHe2. reflexivity.

apply (Hhoare st st'). assumption.

split. assumption. apply bexp_eval_true. assumption.

Qed.

Is the assertion
(1) Yes
(2) No

X = 0

an invariant of the following loop?
WHILE X<100 DO X ::= X+1 END

Is the assertion

Y = 0

an invariant of the following loop?
WHILE X<100 DO X ::= X+1 END

Is the assertion

X > 0

an invariant of the following loop?
WHILE X<100 DO X ::= X+1 END

Is the assertion

X > 0

an invariant of the following loop?
WHILE X = 0 DO X ::= X+1 END

Is the assertion

X > 10

an invariant of the following loop?
WHILE X>10 DO X ::= X+1 END

Is the assertion

X = Y + Z

an invariant of the following loop?
WHILE Y>10 DO Y := Y-1; Z ::= Z+1 END

We can use the while rule to prove the following Hoare triple,
which may seem surprising at first...

Theorem always_loop_hoare : ∀P Q,

{{P}} WHILE BTrue DO SKIP END {{Q}}.

Proof.

(* WORK IN CLASS *) Admitted.

## Review

(hoare_asgn) | |

{{Q [X ↦ a]}} X::=a {{Q}} |

(hoare_skip) | |

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

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

{{ Q }} c2 {{ R }} | (hoare_seq) |

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

{{P ∧ b}} c1 {{Q}} | |

{{P ∧ ~b}} c2 {{Q}} | (hoare_if) |

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

{{P ∧ b}} c {{P}} | (hoare_while) |

{{P}} WHILE b DO c END {{P ∧ ~b}} |

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

P ⇾ P' | |

Q' ⇾ Q | (hoare_consequence) |

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