Acknowledgements
This material is taken verbatim from Software Foundations V4.0
Copyright (c) 2016
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
THE SOFTWARE.
Assumed Knowledge:
* TODO
Learning Outcomes:
* TODO
In the past couple of 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.
 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.
The language we defined, though small, captures some of the key
features of fullblown languages like C, C++, and Java,
including the fundamental notion of mutable state and some
common control structures.
 We proved a number of metatheoretic properties — "meta" in
the sense that they are properties of the language as a whole,
rather than of particular programs in the language. These
included:
 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
 correctness (in the sense of preserving meaning) of a number
of useful program transformations
 behavioral equivalence of programs (in the Equiv chapter).
If we stopped here, we would already have something useful: a set
of tools for defining and discussing programming languages and
language features that are mathematically precise, flexible, and
easy to work with, applied to a set of key properties. All of
these properties are things that language designers, compiler
writers, and users might care about knowing. Indeed, many of them
are so fundamental to our understanding of the programming
languages we deal with that we might not consciously recognize
them as "theorems." But properties that seem intuitively obvious
can sometimes be quite subtle (sometimes also subtly wrong!).
We'll return to the theme of metatheoretic properties of whole
languages later in the book when we discuss
types and
type
soundness. In this chapter, though, we turn to a different set
of issues.
Our goal is to carry out some simple examples of
program
verification — i.e., to use the precise definition of Imp to
prove formally that particular programs satisfy particular
specifications of their behavior. We'll develop a reasoning
system called
FloydHoare Logic — often shortened to just
Hoare Logic — in which each of the syntactic constructs of Imp
is equipped with a generic "proof rule" that can be used to reason
compositionally about the correctness of programs involving this
construct.
Hoare Logic originated 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 multitude of tools that are being used in
academia and industry to specify and verify real software
systems.
Hoare Logic combines two beautiful ideas: a natural way of
writing down
specifications of programs, and a
compositional
proof technique for proving that programs are correct with
respect to such specifications — where by "compositional" we mean
that the structure of proofs directly mirrors the structure of the
programs that they are about.
Assertions
To talk about specifications of programs, the first thing we
need is a way of making
assertions about properties that hold at
particular points during a program's execution — i.e., claims
about the current state of the memory when execution reaches that
point. Formally, an assertion is just a family of propositions
indexed by a
state.
Exercise: 1 star, optional (assertions)
Paraphrase the following assertions in English (or your favorite
natural language).
☐
This way of writing assertions can be a little bit heavy,
for two reasons: (1) every single assertion that we ever write is
going to begin with
fun st ⇒ ; and (2) this state
st is the
only one that we ever use to look up variables in assertions (we
will never need to talk about two different memory states at the
same time). For discussing examples informally, we'll adopt some
simplifying conventions: we'll drop the initial
fun st ⇒, and
we'll write just
X to mean
st X. Thus, instead of writing
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 (in ASCII,
P >> Q), if, whenever
P
holds in some state
st,
Q also holds.
(The
hoare_spec_scope annotation here tells Coq that this
notation is not global but is intended to be used in particular
contexts. The
Open Scope tells Coq that this file is one such
context.)
We'll also want the "iff" variant of implication between
assertions:
Notation "P ⇿ Q" :=
(P ⇾ Q ∧ Q ⇾ P) (at level 80) : hoare_spec_scope.
Hoare Triples
Next, we need a way of making formal claims about the
behavior of commands.
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 property
P is
called the
precondition of
c, while
Q is the
postcondition. Formally:
Since we'll be working a lot with Hoare triples, it's useful to
have a compact notation:
(The traditional notation is
{P} c {Q}, but single braces
are already used for other things in Coq.)
Notation "
{{ P
}} c
{{ Q
}}" :=
(
hoare_triple P c Q) (
at level 90,
c at next level)
:
hoare_spec_scope.
Exercise: 1 star, optional (triples)
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)
}}
☐
Exercise: 1 star, optional (valid_triples)
Which of the following Hoare triples are
valid — i.e., the
claimed relation between
P,
c, and
Q is true?
1)
{{
True}}
X ::= 5
{{
X = 5
}}
2)
{{
X = 2
}}
X ::=
X + 1
{{
X = 3
}}
3)
{{
True}}
X ::= 5;
Y ::= 0
{{
X = 5
}}
4)
{{
X = 2
∧ X = 3
}}
X ::= 5
{{
X = 0
}}
5)
{{
True}}
SKIP {{
False}}
6)
{{
False}}
SKIP {{
True}}
7)
{{
True}}
WHILE True DO SKIP END {{
False}}
8)
{{
X = 0
}}
WHILE X == 0
DO X ::=
X + 1
END
{{
X = 1
}}
9)
{{
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, rather than their
formal
aexp and
bexp encodings. We'll continue doing so
throughout the chapter.)
To get us warmed up for what's coming, here are two simple
facts about Hoare triples.
Proof Rules
The goal of Hoare logic is to provide a
compositional
method for proving the validity of specific Hoare triples. That
is, we want the structure of a program's correctness proof to
mirror the structure of the program itself. To this end, in the
sections below, we'll introduce a rule for reasoning about each of
the different syntactic forms of commands in Imp — one for
assignment, one for sequencing, one for conditionals, etc. — plus
a couple of "structural" rules for gluing things together. We
will then be able to 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
}}
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.
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 righthand side of
the assignment.
More generally, if
a is
any arithmetic expression, then
{{
a = 1
}}
X ::=
a {{
X = 1
}}
is a valid Hoare triple.
This can be made even more general. To conclude that an
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".
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."
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, wherever
P
mentions
X,
P' should instead mention
a.
Since
P is an arbitrary Coq proposition, we can't directly
"edit" its text. Instead, we can achieve the effect we want by
evaluating
P in an updated state:
That is,
P [X ↦ a] is 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)
(
t_update st X (
aeval st (
ANum 3))),
which simplifies to
fun st ⇒
(
fun st' ⇒
st' X ≤ 5)
(
t_update st X 3)
and further simplifies to
fun st ⇒
((
t_update st X 3)
X) ≤ 5)
and by further simplification to
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)
(
t_update st X (
aeval st (
APlus (
AId X) (
ANum 1)))),
which simplifies to
fun st ⇒
(((
t_update st X (
aeval st (
APlus (
AId X) (
ANum 1)))))
X) ≤ 5
and further simplifies to
fun st ⇒
(
aeval st (
APlus (
AId X) (
ANum 1))) ≤ 5.
That is,
P' is the assertion that
X+1 is at most
5.
Now 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.
Here's a first formal proof using this rule.
Exercise: 2 stars (hoare_asgn_examples)
Translate these informal Hoare triples...
1)
{{ (
X ≤ 5) [
X ↦ X + 1]
}}
X ::=
X + 1
{{
X ≤ 5
}}
2)
{{ (0 ≤
X ∧ X ≤ 5) [
X ↦ 3]
}}
X ::= 3
{{ 0 ≤
X ∧ X ≤ 5
}}
...into formal statements (use the names
assn_sub_ex_{1}
and
assn_sub_ex_{2}) and use
hoare_asgn to prove them.
☐
Exercise: 2 stars (hoare_asgn_wrong)
The assignment rule looks backward to almost everyone the first
time they see it. If it still seems puzzling, it may help
to think a little about alternative "forward" rules. Here is a
seemingly natural one:

(hoare_asgn_wrong)


{{ True }} X ::= a {{ X = a }} 

Give a counterexample showing that this rule is incorrect and
argue informally that it is really a counterexample. (Hint:
The rule universally quantifies over the arithmetic expression
a, and your counterexample needs to exhibit an
a for which
the rule doesn't work.)
☐
Exercise: 3 stars, advanced (hoare_asgn_fwd)
However, by using an auxiliary variable
m to remember the
original value of
X we can define a Hoare rule for assignment
that does, intuitively, "work forwards" rather than backwards.

(hoare_asgn_fwd)


{{fun st ⇒ P st ∧ st X = m}} 

X ::= a 

{{fun st ⇒ P st' ∧ st X = aeval st' a }} 

(where st' = t_update st X m) 

Note that we use the original value of
X to reconstruct the
state
st' before the assignment took place. Prove that this rule
is correct (the first hypothesis is the functional extensionality
axiom, which you will need at some point). Also note that this
rule is more complicated than
hoare_asgn.
☐
Exercise: 2 stars, advanced (hoare_asgn_fwd_exists)
Another way to define a forward rule for assignment is to
existentially quantify over the previous value of the assigned
variable.

(hoare_asgn_fwd_exists)


{{fun st ⇒ P st}} 

X ::= a 

{{fun st ⇒ ∃m, P (t_update st X m) ∧ 

st X = aeval (t_update st X m) a }} 

☐
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 }}
⇾
{{ 1 = 1
}}
X ::= 1
{{
X = 1
}}
Or, formally...
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 at the same time.
{{P'}} c {{Q'}} 

P ⇾ P' 

Q' ⇾ Q 
(hoare_consequence)


{{P}} c {{Q}} 

Digression: The eapply Tactic
This is a good moment to introduce another convenient feature of
Coq. We had to write "
with (P' := ...)" explicitly in the proof
of
hoare_asgn_example1 and
hoare_consequence above, to make
sure that all of the metavariables in the premises to the
hoare_consequence_pre rule would be set to specific
values. (Since
P' doesn't appear in the conclusion of
hoare_consequence_pre, the process of unifying the conclusion
with the current goal doesn't constrain
P' to a specific
assertion.)
This is annoying, both because the assertion is a bit long and
also because, in
hoare_asgn_example1, the very next thing we are
going to do — applying the
hoare_asgn rule — will tell us
exactly what it should be! We can use
eapply instead of
apply
to tell Coq, essentially, "Be patient: The missing part is going
to be filled in later in the proof."
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
existential variables (written
?nnn), which
function as placeholders for expressions that will be
determined (by further unification) later in the proof.
In order for
Qed to succeed, all existential variables need to
be determined by the end of the proof. Otherwise Coq
will (rightly) refuse to accept the proof. Remember that the Coq
tactics build proof objects, and proof objects containing
existential variables are not complete.
Lemma silly1 :
∀(
P :
nat → nat → Prop) (
Q :
nat → Prop),
(
∀x y :
nat,
P x y)
→
(
∀x y :
nat,
P x y → Q x)
→
Q 42.
Proof.
intros P Q HP HQ.
eapply HQ.
apply HP.
Coq gives a warning after apply HP. (The warnings look
different between Coq 8.4 and Coq 8.5. In 8.4, the warning says
"No more subgoals but noninstantiated existential variables." In
8.5, it says "All the remaining goals are on the shelf," meaning
that we've finished all our toplevel proof obligations but along
the way we've put some aside to be done later, and we have not
finished those.) Trying to close the proof with Qed gives an
error.
Abort.
An additional constraint is that existential variables cannot be
instantiated with terms containing ordinary variables that did not
exist at the time the existential variable was created. (The
reason for this technical restriction is that allowing such
instantiation would lead to inconsistency of Coq's logic.)
Lemma silly2 :
∀(
P :
nat → nat → Prop) (
Q :
nat → Prop),
(
∃y,
P 42
y)
→
(
∀x y :
nat,
P x y → Q x)
→
Q 42.
Proof.
intros P Q HP HQ.
eapply HQ.
destruct HP as [
y HP'].
Doing
apply HP' above fails with the following error:
Error:
Impossible to unify "?175"
with "y".
In this case there is an easy fix: doing
destruct HP before
doing
eapply HQ.
Abort.
Lemma silly2_fixed :
∀(
P :
nat → nat → Prop) (
Q :
nat → Prop),
(
∃y,
P 42
y)
→
(
∀x y :
nat,
P x y → Q x)
→
Q 42.
Proof.
intros P Q HP HQ.
destruct HP as [
y HP'].
eapply HQ.
apply HP'.
Qed.
The
apply HP' in the last step unifies the existential variable
in the goal with the variable
y.
Note that the
assumption tactic doesn't work in this case, since
it cannot handle existential variables. However, Coq also
provides an
eassumption tactic that solves the goal if one of
the premises matches the goal up to instantiations of existential
variables. We can use it instead of
apply HP' if we like.
Lemma silly2_eassumption :
∀(
P :
nat → nat → Prop) (
Q :
nat → Prop),
(
∃y,
P 42
y)
→
(
∀x y :
nat,
P x y → Q x)
→
Q 42.
Proof.
intros P Q HP HQ.
destruct HP as [
y HP'].
eapply HQ.
eassumption.
Qed.
Exercise: 2 stars (hoare_asgn_examples_2)
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 (name them
assn_sub_ex_{1}' and
assn_sub_ex_{2}') and use
hoare_asgn and
hoare_consequence_pre
to prove them.
☐
Skip
Since
SKIP doesn't change the state, it preserves any
property
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
c_{1} takes any state where
P holds to a state where
Q holds, and if
c_{2} takes any
state where
Q holds to one where
R holds, then doing
c_{1}
followed by
c_{2} will take any state where
P holds to one
where
R holds:
{{ P }} c_{1} {{ Q }} 

{{ Q }} c_{2} {{ R }} 
(hoare_seq)


{{ P }} c_{1};;c_{2} {{ R }} 

Theorem hoare_seq :
∀P Q R c_{1} c_{2},
{{
Q}}
c_{2} {{
R}}
→
{{
P}}
c_{1} {{
Q}}
→
{{
P}}
c_{1};;
c_{2} {{
R}}.
Proof.
intros P Q R c_{1} c_{2} H_{1} H_{2} st st' H_{12} Pre.
inversion H_{12}; subst.
apply (H_{1} st'0 st'); try assumption.
apply (H_{2} st st'0); assumption. Qed.
Note that, in the formal rule
hoare_seq, the premises are
given in backwards order (
c_{2} before
c_{1}). This matches the
natural flow of information in many of the situations where we'll
use the rule, since the natural way to construct a Hoarelogic
proof is to begin at the end of the program (with the final
postcondition) and push postconditions backwards through commands
until we reach the beginning.
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
c_{1} and
c_{2}:
{{
a =
n }}
X ::=
a;;
{{
X =
n }} <
decoration for Q
SKIP
{{
X =
n }}
Here's an example of a program involving both assignment and
sequencing.
We typically use
hoare_seq in conjunction with
hoare_consequence_pre and the
eapply tactic, as in this
example.
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
}}
☐
Exercise: 3 stars (swap_exercise)
Write an Imp program
c that swaps the values of
X and
Y and
show that it satisfies the following specification:
☐
Exercise: 3 stars (hoarestate1)
Explain why the following proposition can't be proven:
∀(
a :
aexp) (
n :
nat),
{{
fun st ⇒
aeval st a =
n}}
(
X ::= (
ANum 3);;
Y ::=
a)
{{
fun st ⇒
st Y =
n}}.
☐
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}} c_{1} {{Q}} 

{{P}} c_{2} {{Q}} 


{{P}} IFB b THEN c_{1} ELSE c_{2} {{Q}} 

However, this is rather weak. For example, using this rule,
we cannot show
{{
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.
Fortunately, 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 rule gives
us more information to work with when reasoning about the behavior
of
c_{1} and
c_{2} (i.e., the reasons why they establish the
postcondition
Q).
{{P ∧ b}} c_{1} {{Q}} 

{{P ∧ ~b}} c_{2} {{Q}} 
(hoare_if)


{{P}} IFB b THEN c_{1} ELSE c_{2} FI {{Q}} 

To interpret this rule formally, we need to do a little work.
Strictly speaking, the assertion we've written,
P ∧ b, is the
conjunction of an assertion and a boolean expression — i.e., it
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 "the boolean expression
b evaluates to
true (in
the given state)."
A couple of useful facts about bassn:
Now we can formalize the Hoare proof rule for conditionals
and prove it correct.
Theorem hoare_if :
∀P Q b c_{1} c_{2},
{{
fun st ⇒
P st ∧ bassn b st}}
c_{1} {{
Q}}
→
{{
fun st ⇒
P st ∧ ~(
bassn b st)
}}
c_{2} {{
Q}}
→
{{
P}} (
IFB b THEN c_{1} ELSE c_{2} FI)
{{
Q}}.
Proof.
intros P Q b c_{1} c_{2} HTrue HFalse st st' HE HP.
inversion HE;
subst.

apply (
HTrue st st').
assumption.
split.
assumption.
apply bexp_eval_true.
assumption.

apply (
HFalse st st').
assumption.
split.
assumption.
apply bexp_eval_false.
assumption.
Qed.
Example
Here is a formal proof that the program we used to motivate the
rule satisfies the specification we gave.
Exercise: 2 stars (if_minus_plus)
Prove the following hoare triple using
hoare_if:
Exercise: Onesided conditionals
Exercise: 4 stars (if1_hoare)
In this exercise we consider extending Imp with "onesided
conditionals" of the form
IF_{1} b THEN c FI. Here
b is a
boolean expression, and
c is a command. If
b evaluates to
true, then command
c is evaluated. If
b evaluates to
false, then
IF_{1} b THEN c FI does nothing.
We recommend that you do this exercise before the ones that
follow, as it should help solidify your understanding of the
material.
The first step is to extend the syntax of commands and introduce
the usual notations. (We've done this for you. We use a separate
module to prevent polluting the global name space.)
Module If_{1}.
Inductive com :
Type :=

CSkip :
com

CAss :
id → aexp → com

CSeq :
com → com → com

CIf :
bexp → com → com → com

CWhile :
bexp → com → com

CIf1 :
bexp → com → com.
Notation "'SKIP'" :=
CSkip.
Notation "c
_{1} ;; c
_{2}" :=
(
CSeq c_{1} c_{2}) (
at level 80,
right associativity).
Notation "X '::=' a" :=
(
CAss X a) (
at level 60).
Notation "'WHILE' b 'DO' c 'END'" :=
(
CWhile b c) (
at level 80,
right associativity).
Notation "'IFB' e
_{1} 'THEN' e
_{2} 'ELSE' e
_{3} 'FI'" :=
(
CIf e_{1} e_{2} e_{3}) (
at level 80,
right associativity).
Notation "'IF
_{1}' b 'THEN' c 'FI'" :=
(
CIf1 b c) (
at level 80,
right associativity).
Next we need to extend the evaluation relation to accommodate
IF_{1} branches. This is for you to do... What rule(s) need to be
added to ceval to evaluate onesided conditionals?
Now we repeat (verbatim) the definition and notation of Hoare triples.
Finally, we (i.e., you) need to state and prove a theorem,
hoare_if_{1}, that expresses an appropriate Hoare logic proof rule
for onesided conditionals. Try to come up with a rule that is
both sound and as precise as possible.
For full credit, prove formally
hoare_if1_good that your rule is
precise enough to show the following valid Hoare triple:
{{
X +
Y =
Z }}
IF_{1} Y ≠ 0
THEN
X ::=
X +
Y
FI
{{
X =
Z }}
Hint: Your proof of this triple may need to use the other proof
rules also. Because we're working in a separate module, you'll
need to copy here the rules you find necessary.
☐
Loops
Finally, we need a rule for reasoning about while loops.
Suppose we have a loop
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.
First of all, let's think about the case where
b is false at the
beginning — i.e., let's assume that the loop body never executes
at all. In this case, the loop behaves like
SKIP, so we might
be tempted to write:
{{
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
reestablishes
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}} 

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. This gives us a little more information to use in
reasoning about
c (showing that it establishes the invariant by
the time it finishes). This gives us 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.
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.
remember (
WHILE b DO c END)
as wcom eqn:
Heqwcom.
induction He;
try (
inversion Heqwcom);
subst;
clear Heqwcom.

split.
assumption.
apply bexp_eval_false.
assumption.

apply IHHe2.
reflexivity.
apply (
Hhoare st st').
assumption.
split.
assumption.
apply bexp_eval_true.
assumption.
Qed.
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 significantly) 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.
We can use the while rule to prove the following Hoare triple,
which may seem surprising at first...
Of course, this result is not surprising if we remember that
the definition of
hoare_triple asserts that the postcondition
must hold
only when the command terminates. If the command
doesn't terminate, we can prove anything we like about the
postcondition.
Hoare rules that only talk about terminating commands are
often said to describe a logic of "partial" correctness. It is
also possible to give Hoare rules for "total" correctness, which
build in the fact that the commands terminate. However, in this
course we will only talk about partial correctness.
Exercise: REPEAT
Exercise: 4 stars, advanced (hoare_repeat)
In this exercise, we'll add a new command to our language of
commands:
REPEAT c
UNTIL a
END. You will write the
evaluation rule for
repeat and add a new Hoare rule to
the language for programs involving it.
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.
Notation "'SKIP'" :=
CSkip.
Notation "c
_{1} ;; c
_{2}" :=
(
CSeq c_{1} c_{2}) (
at level 80,
right associativity).
Notation "X '::=' a" :=
(
CAsgn X a) (
at level 60).
Notation "'WHILE' b 'DO' c 'END'" :=
(
CWhile b c) (
at level 80,
right associativity).
Notation "'IFB' e
_{1} 'THEN' e
_{2} 'ELSE' e
_{3} 'FI'" :=
(
CIf e_{1} e_{2} e_{3}) (
at level 80,
right associativity).
Notation "'REPEAT' e
_{1} 'UNTIL' b
_{2} 'END'" :=
(
CRepeat e_{1} b_{2}) (
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.
A couple of definitions from above, copied here so they use the
new ceval.
To make sure you've got the evaluation rules for REPEAT right,
prove that ex1_repeat evaluates correctly.
Now state and prove a theorem, hoare_repeat, that expresses an
appropriate proof rule for repeat commands. Use hoare_while
as a model, and try to make your rule as precise as possible.
For full credit, make sure (informally) that your rule can be used
to prove the following valid Hoare triple:
{{
X > 0
}}
REPEAT
Y ::=
X;;
X ::=
X  1
UNTIL X = 0
END
{{
X = 0
∧ Y > 0
}}
☐
Summary
So far, we've introduced Hoare Logic as a tool for reasoning about
Imp programs. In the reminder of this chapter we'll explore a
systematic way to use Hoare Logic to prove properties about
programs. The rules of Hoare Logic are:

(hoare_asgn)


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


(hoare_skip)


{{ P }} SKIP {{ P }} 

{{ P }} c_{1} {{ Q }} 

{{ Q }} c_{2} {{ R }} 
(hoare_seq)


{{ P }} c_{1};;c_{2} {{ R }} 

{{P ∧ b}} c_{1} {{Q}} 

{{P ∧ ~b}} c_{2} {{Q}} 
(hoare_if)


{{P}} IFB b THEN c_{1} ELSE c_{2} 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}} 

In the next chapter, we'll see how these rules are used to prove
that programs satisfy specifications of their behavior.
Additional Exercises
Exercise: 3 stars (himp_hoare)
In this exercise, we will derive proof rules for the
HAVOC
command, which we studied in the last chapter.
First, we enclose this work in a separate module, and recall the
syntax and bigstep semantics of Himp commands.
Module Himp.
Inductive com :
Type :=

CSkip :
com

CAsgn :
id → aexp → com

CSeq :
com → com → com

CIf :
bexp → com → com → com

CWhile :
bexp → com → com

CHavoc :
id → com.
Notation "'SKIP'" :=
CSkip.
Notation "X '::=' a" :=
(
CAsgn X a) (
at level 60).
Notation "c
_{1} ;; c
_{2}" :=
(
CSeq c_{1} c_{2}) (
at level 80,
right associativity).
Notation "'WHILE' b 'DO' c 'END'" :=
(
CWhile b c) (
at level 80,
right associativity).
Notation "'IFB' e
_{1} 'THEN' e
_{2} 'ELSE' e
_{3} 'FI'" :=
(
CIf e_{1} e_{2} e_{3}) (
at level 80,
right associativity).
Notation "'HAVOC' X" := (
CHavoc X) (
at level 60).
Reserved Notation "c
_{1} '/' st '
⇓' st'" (
at level 40,
st at level 39).
Inductive ceval :
com → state → state → Prop :=

E_Skip :
∀st :
state,
SKIP /
st ⇓ st

E_Ass :
∀(
st :
state) (
a_{1} :
aexp) (
n :
nat) (
X :
id),
aeval st a_{1} =
n → (
X ::=
a_{1}) /
st ⇓ t_update st X n

E_Seq :
∀(
c_{1} c_{2} :
com) (
st st' st'' :
state),
c_{1} /
st ⇓ st' → c_{2} /
st' ⇓ st'' → (
c_{1} ;;
c_{2}) /
st ⇓ st''

E_IfTrue :
∀(
st st' :
state) (
b_{1} :
bexp) (
c_{1} c_{2} :
com),
beval st b_{1} =
true →
c_{1} /
st ⇓ st' → (
IFB b_{1} THEN c_{1} ELSE c_{2} FI) /
st ⇓ st'

E_IfFalse :
∀(
st st' :
state) (
b_{1} :
bexp) (
c_{1} c_{2} :
com),
beval st b_{1} =
false →
c_{2} /
st ⇓ st' → (
IFB b_{1} THEN c_{1} ELSE c_{2} FI) /
st ⇓ st'

E_WhileEnd :
∀(
b_{1} :
bexp) (
st :
state) (
c_{1} :
com),
beval st b_{1} =
false → (
WHILE b_{1} DO c_{1} END) /
st ⇓ st

E_WhileLoop :
∀(
st st' st'' :
state) (
b_{1} :
bexp) (
c_{1} :
com),
beval st b_{1} =
true →
c_{1} /
st ⇓ st' →
(
WHILE b_{1} DO c_{1} END) /
st' ⇓ st'' →
(
WHILE b_{1} DO c_{1} END) /
st ⇓ st''

E_Havoc :
∀(
st :
state) (
X :
id) (
n :
nat),
(
HAVOC X) /
st ⇓ t_update st X n
where "c
_{1} '/' st '
⇓' st'" := (
ceval c_{1} st st').
The definition of Hoare triples is exactly as before. Unlike our
notion of program equivalence, which had subtle consequences with
occassionally nonterminating commands (exercise havoc_diverge),
this definition is still fully satisfactory. Convince yourself of
this before proceeding.
Complete the Hoare rule for HAVOC commands below by defining
havoc_pre and prove that the resulting rule is correct.