# HoareHoare Logic, Part I

What we've done so far:
• 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)
We've dealt with a few sorts of properties of Imp programs:
• Termination
• Nontermination
• Equivalence
Overview of this chapter...
Topic:
• A systematic method for reasoning about the functional correctness of programs in Imp
Goals:
• a natural notation for program specifications and
• a compositional proof technique for program correctness
Plan:
• specifications (assertions / Hoare triples)
• proof rules
• loop invariants
• decorated programs
• examples

# Assertions

Definition Assertion := stateProp.
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

fun st ⇒ (st Z) * (st Z) ≤ m ∧
¬((S (st Z)) * (S (st Z)) ≤ m)
we'll write just
Z * Z ≤ m ∧ ~((S Z) * (S Z) ≤ m).
Given two assertions P and Q, we say that P implies Q, written P ->> Q, if, whenever P holds in some state st, Q also holds.
Definition assert_implies (P Q : Assertion) : Prop :=
st, P stQ st.

Notation "P ->> Q" := (assert_implies P Q)
(at level 80) : hoare_spec_scope.
Open Scope hoare_spec_scope.
We'll also want the "iff" variant of implication between assertions:
Notation "P <<->> Q" :=
(P ->> QQ ->> P) (at level 80) : hoare_spec_scope.

# Hoare Triples

In general, the behavior of a command is to transform one state to another, so it is natural to express claims about commands in terms of assertions that are true before and after the command executes:
• "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."
Such a claim is called a Hoare Triple. The assertion 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',
st =[ c ]⇒ 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) {{X = m}}
c
{{(Z * Z) ≤ m ∧ ¬(((S Z) * (S Z)) ≤ m)}}

Is the following Hoare triple valid — i.e., is the claimed relation between P, c, and Q true?
{{True}X ::= 5 {{X = 5}}
(1) Yes
(2) No
{{X = 2}X ::= X + 1 {{X = 3}}
(1) Yes
(2) No
{{True}X ::= 5;; Y ::= 0 {{X = 5}}
(1) Yes
(2) No
{{X = 2 ∧ X = 3}X ::= 5 {{X = 0}}
(1) Yes
(2) No
{{True}SKIP {{False}}
(1) Yes
(2) No
{{False}SKIP {{True}}
(1) Yes
(2) No
{{True}WHILE true DO SKIP END {{False}}
(1) Yes
(2) No
This one?
{{X = 0}}
WHILE X = 0 DO X ::= X + 1 END
{{X = 1}}
(1) Yes
(2) No
This one?
{{X = 1}}
WHILE ~(X = 0) DO X ::= X + 1 END
{{X = 100}}
(1) Yes
(2) No

To get us warmed up for what's coming, here are two simple facts about Hoare triples. (Make sure you understand what they mean.)
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.

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.

# Proof Rules

Plan:
• 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

The rule for assignment is the most fundamental of the Hoare logic proof rules. Here's how it works.
Consider this valid Hoare triple:
{Y = 1 }}  X ::= Y  {X = 1 }}
That is, the property of being equal to 1 gets transferred from Y to X.
Similarly, in
{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.
More generally, if a is any arithmetic expression, then
{a = 1 }}  X ::= a  {X = 1 }}
is a valid Hoare triple.
Even more generally, to conclude that an arbitrary assertion 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".
For example, these are valid applications of the assignment rule:
{{ (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 }}
To formalize the rule, we must first formalize the idea of "substituting an expression for an Imp variable in an assertion", which we refer to as assertion substitution, or assn_sub. That is, given a proposition P, a variable X, and an arithmetic expression a, we want to derive another proposition P' that is just the same as P except that P' should mention a wherever P mentions X.
Since P is an arbitrary Coq assertion, we can't directly "edit" its text. However, we can achieve the same effect by evaluating P in an updated state:
Definition assn_sub X a P : Assertion :=
fun (st : state) ⇒
P (X !-> aeval st a ; st).

Notation "P [ X > a ]" := (assn_sub X a P)
(at level 10, X at next level).
That is, P [X > a] stands for an assertion — let's call it 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
fun st ⇒
(fun st' ⇒ st' X ≤ 5)
(X !-> aeval st 3 ; st),
which simplifies to
fun st ⇒
(fun st' ⇒ st' X ≤ 5)
(X !-> 3 ; st)
and further simplifies to
fun st ⇒
((X !-> 3 ; stX) ≤ 5
and finally to
fun st ⇒
3 ≤ 5.
That is, P' is the assertion that 3 is less than or equal to 5 (as expected).
For a more interesting example, suppose P' is (X 5) [X > X + 1]. Formally, P' is the Coq expression
fun st ⇒
(fun st' ⇒ st' X ≤ 5)
(X !-> aeval st (X + 1) ; st),
which simplifies to
fun st ⇒
(X !-> aeval st (X + 1) ; stX ≤ 5
and further simplifies to
fun st ⇒
(aeval st (X + 1)) ≤ 5.
That is, P' is the assertion that X + 1 is at most 5.
Now, using the concept of substitution, we can give the precise proof rule for assignment:
 (hoare_asgn) {{Q [X ⊢> a]}} X ::= a {{Q}}
We can prove formally that this rule is indeed valid.
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.
Here's a first formal proof using this rule.
Example assn_sub_example :
{{(fun stst X < 5) [X > X + 1]}}
X ::= X + 1
{{fun stst X < 5}}.
Proof.
(* WORK IN CLASS *) Admitted.
Of course, what would be even more helpful is to prove this simpler triple:
{{X < 4}X ::= X + 1 {{X < 5}}
We will see how to do so in the next section.
Here is the assignment rule again:
{Q [X > a}X ::= a {Q }}
Is the following triple a valid instance of this rule?
{X = 5 }X ::= X + 1 {X = 6 }}
(1) Yes
(2) No

Here is the assignment rule again:
{Q [X > a}X ::= a {Q }}
Is the following triple a valid instance of this rule?
{Y < Z }X ::= Y {X < Z }}
(1) Yes
(2) No

The assignment rule again:
{Q [X > a}X ::= a {Q }}
Is the following triple a valid instance of this rule?
{X+1 < Y }X ::= X + 1 {X < Y }}
(1) Yes
(2) No

The assignment rule again:
{Q [X > a}X ::= a {Q }}
Is the following triple a valid instance of this rule?
{X < Y }X ::= X + 1 {X+1 < Y }}
(1) Yes
(2) No

The assignment rule again:
{Q [X > a}X ::= a {Q }}
Is the following triple a valid instance of this rule?
{X < Y }X ::= X + 1 {X < Y+1 }}
(1) Yes
(2) No

The assignment rule again:
{Q [X > a}X ::= a {Q }}
Is the following triple a valid instance of this rule?
{True }X ::= 3 {X = 3 }}
(1) Yes
(2) No

## Consequence

Sometimes the preconditions and postconditions we get from the Hoare rules won't quite be the ones we want in the particular situation at hand — they may be logically equivalent but have a different syntactic form that fails to unify with the goal we are trying to prove, or they actually may be logically weaker (for preconditions) or stronger (for postconditions) than what we need.
For instance, while
{{(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 can capture this observation with the following rule:
 {{P'}} c {{Q}} P <<->> P' (hoare_consequence_pre_equiv) {{P}} c {{Q}}
Taking this line of thought a bit further, we can see that strengthening the precondition or weakening the postcondition of a valid triple always produces another valid triple. This observation is captured by two 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}}
Here are the formal versions:
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.

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.
For example, we can use the first consequence rule like this:
{True }->>
{{ (X = 1) [X > 1] }}
X ::= 1
{X = 1 }}
Or, formally...
Example hoare_asgn_example1 :
{{fun stTrue}} X ::= 1 {{fun stst X = 1}}.
Proof.
(* WORK IN CLASS *) Admitted.
We can also use it to prove the example mentioned earlier.
{X < 4 }->>
{{ (X < 5)[X > X + 1] }}
X ::= X + 1
{X < 5 }}
Or, formally ...
Example assn_sub_example2 :
{{(fun stst X < 4)}}
X ::= X + 1
{{fun stst X < 5}}.
Proof.
(* WORK IN CLASS *) Admitted.
Finally, for convenience in proofs, here is a combined rule of consequence that allows us to vary both the precondition and the postcondition in one go.
 {{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.

## Skip

Since SKIP doesn't change the state, it preserves any assertion P:
 (hoare_skip) {{ P }} SKIP {{ P }}
Theorem hoare_skip : P,
{{P}} SKIP {{P}}.
Proof.
intros P st st' H HP. inversion H. subst.
assumption. Qed.

## Sequencing

More interestingly, if the command c1 takes any state where P holds to a state where Q holds, and if c2 takes any state where Q holds to one where R holds, then doing c1 followed by c2 will take any state where P holds to one where R holds:
 {{ 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.
Informally, a nice way of displaying 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 }}
Here's an example of a program involving both assignment and sequencing.
Example hoare_asgn_example3 : a n,
{{fun staeval st a = n}}
X ::= a;; SKIP
{{fun stst X = n}}.
Proof.
intros a n. eapply hoare_seq.
- (* right part of seq *)
apply hoare_skip.
- (* left part of seq *)
eapply hoare_consequence_pre. apply hoare_asgn.
intros st H. subst. reflexivity.
Qed.

## Conditionals

What sort of rule do we want for reasoning about conditional commands?
Certainly, if the same assertion Q holds after executing either of the branches, then it holds after the whole conditional. So we might be tempted to write:
 {{P}} c1 {{Q}} {{P}} c2 {{Q}} {{P}} TEST b THEN c1 ELSE c2 {{Q}}
However, this is rather weak. For example, using this rule, we cannot show
{True }}
TEST 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.
Better:
 {{P ∧   b}} c1 {{Q}} {{P ∧ ¬b}} c2 {{Q}} (hoare_if) {{P}} TEST b THEN c1 ELSE c2 FI {{Q}}
To make this formal, we need a way of formally "lifting" any bexp b to an assertion.
We'll write bassn b for the assertion "the boolean expression b evaluates to true."
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 stP stbassn b st}} c1 {{Q}} →
{{fun stP st ∧ ¬(bassn b st)}} c2 {{Q}} →
{{P}} TEST b THEN c1 ELSE c2 FI {{Q}}.
Proof.
intros P Q b c1 c2 HTrue HFalse st st' HE HP.
inversion HE; subst.
- (* b is true *)
apply (HTrue st st').
assumption.
split. assumption.
apply bexp_eval_true. assumption.
- (* b is false *)
apply (HFalse st st').
assumption.
split. assumption.
apply bexp_eval_false. assumption. Qed.

### Example

Example if_example :
{{fun stTrue}}
TEST X = 0
THEN Y ::= 2
ELSE Y ::= X + 1
FI
{{fun stst Xst Y}}.
Proof.
(* WORK IN CLASS *) Admitted.

## Recap

Idea: create a domain specific logic for reasoning about properties of Imp programs.
• This hides the low-level details of the semantics of the program
• Leads to a compositional reasoning process
The basic structure is given by Hoare triples of the form:
{{P}c {{Q}}
• P and Q are assertions about the state of the Imp program.
• "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."
The rules of Hoare Logic (so far):
 (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}} TEST b THEN c1 ELSE c2 FI {{Q}}
 {{P'}} c {{Q'}} P ->> P' Q' ->> Q (hoare_consequence) {{P}} c {{Q}}

## Loops

Suppose we have a loop
WHILE b DO c END
and we want to find a precondition P and a postcondition Q such that
{{P}WHILE b DO c END {{Q}}
is a valid triple.
If b is false, then the loop is like SKIP:
{{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: But, as with if, we also know ¬ b in the postcondition:
{{P}WHILE b DO c END {{P ∧ ¬b}}
What about when b is true?
First attempt:
 {{P}} c {{P}} {{P}} WHILE b DO c END {{P ∧ ¬b}}
This is almost the rule we want, but again it can be improved a little: at the beginning of the loop body, we know not only that P holds, but also that the guard b is true in the current state.
We know that b is true in the precondition of c. And this leads us to the final version of the rule:
 {{P ∧ b}} c {{P}} (hoare_while) {{P}} WHILE b DO c END {{P ∧ ¬b}}
The proposition P is called an invariant of the loop.
Theorem hoare_while : P b c,
{{fun stP stbassn b st}} c {{P}} →
{{P}} WHILE b DO c END {{fun stP 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

remember (WHILE b DO c END)%imp as wcom eqn:Heqwcom.
induction He;
try (inversion Heqwcom); subst; clear Heqwcom.
- (* E_WhileFalse *)
split. assumption. apply bexp_eval_false. assumption.
- (* E_WhileTrue *)
apply IHHe2. reflexivity.
apply (Hhoare st st'). assumption.
split. assumption. apply bexp_eval_true. assumption.
Qed.
Is the assertion
Y = 0
an invariant of the following loop?
WHILE X .< 100 DO X ::= X + 1 END
(1) Yes
(2) No
Is the assertion
X = 0
an invariant of the following loop?
WHILE X .< 100 DO X ::= X + 1 END
(1) Yes
(2) No
Is the assertion
X < Y
an invariant of the following loop?
WHILE true DO X ::= X + 1;; Y ::= Y + 1 END
(1) Yes
(2) No
Is the assertion
X = Y + Z
an invariant of the following loop?
WHILE Y .> 10 DO Y := Y - 1;; Z ::= Z + 1 END
(1) Yes
(2) No
One subtlety in the terminology is that calling some assertion P a "loop invariant" doesn't just mean that it is preserved by the body of the loop in question (i.e., {{P}} c {{P}}, where c is the loop body), but rather that P together with the fact that the loop's guard is true is a sufficient precondition for c to ensure P as a postcondition.
This is a slightly (but importantly) weaker requirement. For example, if P is the assertion X = 0, then P 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.
Is the assertion
X > 0
an invariant of the following loop?
WHILE X = 0 DO X ::= X - 1 END
(1) Yes
(2) No
Is the assertion
X < 100
an invariant of the following loop?
WHILE X .< 100 DO X ::= X + 1 END
(1) Yes
(2) No
Is the assertion
X > 10
an invariant of the following loop?
WHILE X .> 10 DO X ::= X + 1 END
(1) Yes
(2) No
We can use the WHILE rule to prove the following Hoare triple...
Theorem always_loop_hoare : P Q,
{{P}} WHILE true DO SKIP END {{Q}}.
Proof.
(* WORK IN CLASS *) Admitted.