# HoareHoare Logic, Part I

Require Export Imp.

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'll return to the theme of metatheoretic properties of whole
languages later in the course when we discuss
Our goal is to see how to carry out some simple examples of
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 multitude of tools that are being used in
academia and industry to specify and verify real software
systems.

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

- determinism of evaluation

*types*and*type soundness*. In this chapter, though, we'll turn to a different set of issues.*program verification*— i.e., using the precise definition of Imp to prove formally that particular programs satisfy particular specifications of their behavior. We'll develop a reasoning system called*Floyd-Hoare Logic*— often 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 compositionally about the correctness of programs involving this construct.# Hoare Logic

*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

*assertions*about properties that hold at particular points during a program's execution — i.e., claims about the current state of the memory when program execution reaches that point. Formally, an assertion is just a family of propositions indexed by a state.

Definition Assertion := state → Prop.

Paraphrase the following assertions in English.

Definition as1 : Assertion := fun st ⇒ st X = 3.

Definition as2 : Assertion := fun st ⇒ st X ≤ st Y.

Definition as3 : Assertion :=

fun st ⇒ st X = 3 ∨ st X ≤ st Y.

Definition as4 : Assertion :=

fun st ⇒ st Z × st Z ≤ st X ∧

¬ (((S (st Z)) × (S (st Z))) ≤ st X).

Definition as5 : Assertion := fun st ⇒ True.

Definition as6 : Assertion := fun st ⇒ False.

(* FILL IN HERE *)

☐

## Notation for Assertions

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

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

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

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

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

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

(* FILL IN HERE *)

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

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

*compositional*method for proving the validity of Hoare triples. That is, the structure of a program's correctness proof should mirror the structure of the program itself. To this end, in the sections below, we'll introduce one 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 that are useful for gluing things together. We will 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.

#### 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 and use hoare_asgn to prove them.
X ::= X + 1

{{ X ≤ 5 }}

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

X ::= 3

{{ 0 ≤ X ∧ X ≤ 5 }}

(* FILL IN HERE *)

☐

Give a counterexample showing that this rule is incorrect
(informally). 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: 2 stars (hoare_asgn_wrong)

The assignment rule looks backward to almost everyone the first time they see it. If it still seems backward to you, 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 }} |

(* FILL IN HERE *)

☐

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: 3 stars, advanced (hoare_asgn_fwd)

However, 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' = update st X m) |

Theorem hoare_asgn_fwd :

(∀{X Y: Type} {f g : X → Y},

(∀(x: X), f x = g x) → f = g) →

∀m a P,

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

X ::= a

{{fun st ⇒ P (update st X m) ∧ st X = aeval (update st X m) a }}.

Proof.

intros functional_extensionality m a P.

(* FILL IN HERE *) Admitted.

☐

#### 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 (update st X m) ∧ | |

st X = aeval (update st X m) a }} |

(* This rule was proposed by Nick Giannarakis and Zoe Paraskevopoulou. *)

Theorem hoare_asgn_fwd_exists :

(∀{X Y: Type} {f g : X → Y},

(∀(x: X), f x = g x) → f = g) →

∀a P,

{{fun st ⇒ P st}}

X ::= a

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

st X = aeval (update st X m) a }}.

Proof.

intros functional_extensionality a P.

(* FILL IN HERE *) Admitted.

Theorem hoare_asgn_fwd_exists :

(∀{X Y: Type} {f g : X → Y},

(∀(x: X), f x = g x) → f = g) →

∀a P,

{{fun st ⇒ P st}}

X ::= a

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

st X = aeval (update st X m) a }}.

Proof.

intros functional_extensionality a P.

(* FILL IN HERE *) Admitted.

☐

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

*existential variables*(written ?nnn) as placeholders for expressions that will be determined (by further unification) later in the proof.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:

No more subgoals but non-instantiated existential variables:

Existential 1 =

?171 : [P : nat → nat → Prop

Q : nat → Prop

HP : ∀x y : nat, P x y

HQ : ∀x y : nat, P x y → Q x ⊢ nat]

(dependent evars: ?171 open,)

You can use Grab Existential Variables.

Trying to finish the proof with Qed gives an error:
Existential 1 =

?171 : [P : nat → nat → Prop

Q : nat → Prop

HP : ∀x y : nat, P x y

HQ : ∀x y : nat, P x y → Q x ⊢ nat]

(dependent evars: ?171 open,)

You can use Grab Existential Variables.

Error: Attempt to save a proof with existential variables still non-instantiated

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.

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.

In the last step we did apply HP' which unifies the existential
variable in the goal with the variable y. 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'.

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 and use hoare_asgn and
hoare_consequence_pre to prove them.
{{ 0 ≤ 3 ∧ 3 ≤ 5 }} X ::= 3 {{ 0 ≤ X ∧ X ≤ 5 }}

(* FILL IN HERE *)

☐

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

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: the natural way to construct a Hoare-logic 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 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.

You will most often use hoare_seq and
hoare_consequence_pre in conjunction with the eapply tactic,
as done above.

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

☐

#### Exercise: 3 stars (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}}

Definition swap_program : com :=

(* FILL IN HERE *) admit.

Theorem swap_exercise :

{{fun st ⇒ st X ≤ st Y}}

swap_program

{{fun st ⇒ st Y ≤ st X}}.

Proof.

(* FILL IN HERE *) Admitted.

☐

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

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

(X ::= (ANum 3);; Y ::= a)

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

(* FILL IN HERE *)

☐

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

A couple of useful facts about bassn:

Lemma bexp_eval_true : ∀b st,

beval st b = true → (bassn b) st.

Proof.

intros b st Hbe.

unfold bassn. assumption. Qed.

intros b st Hbe.

unfold bassn. assumption. Qed.

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

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

# Hoare Logic: So Far

*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

*Hoare triples*of the form:

{{P}} c {{Q}}

- P and Q are predicates 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."

## Hoare Logic Rules (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}} IFB b THEN c1 ELSE c2 FI {{Q}} |

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

P ⇾ P' | |

Q' ⇾ Q | (hoare_consequence) |

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

### Example

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.

(* WORKED IN CLASS *)

apply hoare_if.

Case "Then".

eapply hoare_consequence_pre. apply hoare_asgn.

unfold bassn, assn_sub, update, assert_implies.

simpl. intros st [_ H].

apply beq_nat_true in H.

rewrite H. omega.

Case "Else".

eapply hoare_consequence_pre. apply hoare_asgn.

unfold assn_sub, update, assert_implies.

simpl; intros st _. omega.

Qed.

(* WORKED IN CLASS *)

apply hoare_if.

Case "Then".

eapply hoare_consequence_pre. apply hoare_asgn.

unfold bassn, assn_sub, update, assert_implies.

simpl. intros st [_ H].

apply beq_nat_true in H.

rewrite H. omega.

Case "Else".

eapply hoare_consequence_pre. apply hoare_asgn.

unfold assn_sub, update, assert_implies.

simpl; intros st _. omega.

Qed.

Theorem if_minus_plus :

{{fun st ⇒ True}}

IFB (BLe (AId X) (AId Y))

THEN (Z ::= AMinus (AId Y) (AId X))

ELSE (Y ::= APlus (AId X) (AId Z))

FI

{{fun st ⇒ st Y = st X + st Z}}.

Proof.

(* FILL IN HERE *) Admitted.

### Exercise: One-sided conditionals

#### Exercise: 4 stars (if1_hoare)

Module If1.

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.

Tactic Notation "com_cases" tactic(first) ident(c) :=

first;

[ Case_aux c "SKIP" | Case_aux c "::=" | Case_aux c ";"

| Case_aux c "IFB" | Case_aux c "WHILE" | Case_aux c "CIF1" ].

Notation "'SKIP'" :=

CSkip.

Notation "c1 ;; c2" :=

(CSeq c1 c2) (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' e1 'THEN' e2 'ELSE' e3 'FI'" :=

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

Notation "'IF1' b 'THEN' c 'FI'" :=

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

Next we need to extend the evaluation relation to accommodate
IF1 branches. This is for you to do... What rule(s) need to be
added to ceval to evaluate one-sided conditionals?

Reserved Notation "c1 '/' 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) (a1 : aexp) (n : nat) (X : id),

aeval st a1 = n → (X ::= a1) / st ⇓ update st X n

| E_Seq : ∀(c1 c2 : com) (st st' st'' : state),

c1 / st ⇓ st' → c2 / st' ⇓ st'' → (c1 ;; c2) / st ⇓ st''

| E_IfTrue : ∀(st st' : state) (b1 : bexp) (c1 c2 : com),

beval st b1 = true →

c1 / st ⇓ st' → (IFB b1 THEN c1 ELSE c2 FI) / st ⇓ st'

| E_IfFalse : ∀(st st' : state) (b1 : bexp) (c1 c2 : com),

beval st b1 = false →

c2 / st ⇓ st' → (IFB b1 THEN c1 ELSE c2 FI) / st ⇓ st'

| E_WhileEnd : ∀(b1 : bexp) (st : state) (c1 : com),

beval st b1 = false → (WHILE b1 DO c1 END) / st ⇓ st

| E_WhileLoop : ∀(st st' st'' : state) (b1 : bexp) (c1 : com),

beval st b1 = true →

c1 / st ⇓ st' →

(WHILE b1 DO c1 END) / st' ⇓ st'' →

(WHILE b1 DO c1 END) / st ⇓ st''

(* FILL IN HERE *)

where "c1 '/' st '⇓' st'" := (ceval c1 st st').

Tactic Notation "ceval_cases" tactic(first) ident(c) :=

first;

[ Case_aux c "E_Skip" | Case_aux c "E_Ass" | Case_aux c "E_Seq"

| Case_aux c "E_IfTrue" | Case_aux c "E_IfFalse"

| Case_aux c "E_WhileEnd" | Case_aux c "E_WhileLoop"

(* FILL IN HERE *)

].

Now we repeat (verbatim) the definition and notation of Hoare triples.

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

∀st st',

c / st ⇓ st' →

P st →

Q st'.

Notation "{{ P }} c {{ Q }}" := (hoare_triple P c Q)

(at level 90, c at next level)

: hoare_spec_scope.

Finally, we (i.e., you) need to state and prove a theorem,
hoare_if1, that expresses an appropriate Hoare logic proof rule
for one-sided conditionals. Try to come up with a rule that is
both sound and as precise as possible.

(* FILL IN HERE *)

For full credit, prove formally that your rule is precise enough
to show the following valid Hoare triple:
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.

{{ X + Y = Z }}

IF1 Y ≠ 0 THEN

X ::= X + Y

FI

{{ X = Z }}

IF1 Y ≠ 0 THEN

X ::= X + Y

FI

{{ X = Z }}

Lemma hoare_if1_good :

{{ fun st ⇒ st X + st Y = st Z }}

IF1 BNot (BEq (AId Y) (ANum 0)) THEN

X ::= APlus (AId X) (AId Y)

FI

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

Proof. (* FILL IN HERE *) Admitted.

End If1.

☐

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

{{P}} WHILE b DO c END {{P ∧ ¬b}}

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

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.

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
This is a slightly (but significantly) weaker requirement. For
example, if P is the assertion X = 0, then P

*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.Example while_example :

{{fun st ⇒ st X ≤ 3}}

WHILE (BLe (AId X) (ANum 2))

DO X ::= APlus (AId X) (ANum 1) END

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

Proof.

eapply hoare_consequence_post.

apply hoare_while.

eapply hoare_consequence_pre.

apply hoare_asgn.

unfold bassn, assn_sub, assert_implies, update. simpl.

intros st [H1 H2]. apply ble_nat_true in H2. omega.

unfold bassn, assert_implies. intros st [Hle Hb].

simpl in Hb. destruct (ble_nat (st X) 2) eqn : Heqle.

apply ex_falso_quodlibet. apply Hb; reflexivity.

apply ble_nat_false in Heqle. omega.

Qed.

eapply hoare_consequence_post.

apply hoare_while.

eapply hoare_consequence_pre.

apply hoare_asgn.

unfold bassn, assn_sub, assert_implies, update. simpl.

intros st [H1 H2]. apply ble_nat_true in H2. omega.

unfold bassn, assert_implies. intros st [Hle Hb].

simpl in Hb. destruct (ble_nat (st X) 2) eqn : Heqle.

apply ex_falso_quodlibet. apply Hb; reflexivity.

apply ble_nat_false in Heqle. omega.

Qed.

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

(* WORKED IN CLASS *)

intros P Q.

apply hoare_consequence_pre with (P' := fun st : state ⇒ True).

eapply hoare_consequence_post.

apply hoare_while.

Case "Loop body preserves invariant".

apply hoare_post_true. intros st. apply I.

Case "Loop invariant and negated guard imply postcondition".

simpl. intros st [Hinv Hguard].

apply ex_falso_quodlibet. apply Hguard. reflexivity.

Case "Precondition implies invariant".

intros st H. constructor. Qed.

(* WORKED IN CLASS *)

intros P Q.

apply hoare_consequence_pre with (P' := fun st : state ⇒ True).

eapply hoare_consequence_post.

apply hoare_while.

Case "Loop body preserves invariant".

apply hoare_post_true. intros st. apply I.

Case "Loop invariant and negated guard imply postcondition".

simpl. intros st [Hinv Hguard].

apply ex_falso_quodlibet. apply Hguard. reflexivity.

Case "Precondition implies invariant".

intros st H. constructor. Qed.

Of course, this result is not surprising if we remember that
the definition of hoare_triple asserts that the postcondition
must hold
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.

*only*when the command terminates. If the command doesn't terminate, we can prove anything we like about the post-condition.Module RepeatExercise.

#### 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.Inductive com : Type :=

| CSkip : com

| CAsgn : 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) ident(c) :=

first;

[ Case_aux c "SKIP" | Case_aux c "::=" | Case_aux c ";"

| Case_aux c "IFB" | Case_aux c "WHILE"

| Case_aux c "CRepeat" ].

Notation "'SKIP'" :=

CSkip.

Notation "c1 ;; c2" :=

(CSeq c1 c2) (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' 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 : ∀st,

ceval st SKIP st

| E_Ass : ∀st a1 n X,

aeval st a1 = n →

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

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

ceval st c1 st' →

ceval st' c2 st'' →

ceval st (c1 ;; c2) st''

| E_IfTrue : ∀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 : ∀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 : ∀b1 st c1,

beval st b1 = false →

ceval st (WHILE b1 DO c1 END) st

| E_WhileLoop : ∀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) ident(c) :=

first;

[ Case_aux c "E_Skip" | Case_aux c "E_Ass"

| Case_aux c "E_Seq"

| Case_aux c "E_IfTrue" | Case_aux c "E_IfFalse"

| Case_aux c "E_WhileEnd" | Case_aux 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 :=

∀st st', (c / st ⇓ st') → P st → Q st'.

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

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

To make sure you've got the evaluation rules for REPEAT right,
prove that ex1_repeat evaluates correctly.

Definition ex1_repeat :=

REPEAT

X ::= ANum 1;;

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

UNTIL (BEq (AId X) (ANum 1)) END.

Theorem ex1_repeat_works :

ex1_repeat / empty_state ⇓

update (update empty_state X 1) Y 1.

Proof.

(* FILL IN HERE *) Admitted.

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.

(* FILL IN HERE *)

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

REPEAT

Y ::= X;;

X ::= X - 1

UNTIL X = 0 END

{{ X = 0 ∧ Y > 0 }}

End RepeatExercise.

☐

## Exercise: HAVOC

#### Exercise: 3 stars (himp_hoare)

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.

Tactic Notation "com_cases" tactic(first) ident(c) :=

first;

[ Case_aux c "SKIP" | Case_aux c "::=" | Case_aux c ";"

| Case_aux c "IFB" | Case_aux c "WHILE" | Case_aux c "HAVOC" ].

Notation "'SKIP'" :=

CSkip.

Notation "X '::=' a" :=

(CAsgn X a) (at level 60).

Notation "c1 ;; c2" :=

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

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 "'HAVOC' X" := (CHavoc X) (at level 60).

Reserved Notation "c1 '/' 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) (a1 : aexp) (n : nat) (X : id),

aeval st a1 = n → (X ::= a1) / st ⇓ update st X n

| E_Seq : ∀(c1 c2 : com) (st st' st'' : state),

c1 / st ⇓ st' → c2 / st' ⇓ st'' → (c1 ;; c2) / st ⇓ st''

| E_IfTrue : ∀(st st' : state) (b1 : bexp) (c1 c2 : com),

beval st b1 = true →

c1 / st ⇓ st' → (IFB b1 THEN c1 ELSE c2 FI) / st ⇓ st'

| E_IfFalse : ∀(st st' : state) (b1 : bexp) (c1 c2 : com),

beval st b1 = false →

c2 / st ⇓ st' → (IFB b1 THEN c1 ELSE c2 FI) / st ⇓ st'

| E_WhileEnd : ∀(b1 : bexp) (st : state) (c1 : com),

beval st b1 = false → (WHILE b1 DO c1 END) / st ⇓ st

| E_WhileLoop : ∀(st st' st'' : state) (b1 : bexp) (c1 : com),

beval st b1 = true →

c1 / st ⇓ st' →

(WHILE b1 DO c1 END) / st' ⇓ st'' →

(WHILE b1 DO c1 END) / st ⇓ st''

| E_Havoc : ∀(st : state) (X : id) (n : nat),

(HAVOC X) / st ⇓ update st X n

where "c1 '/' st '⇓' st'" := (ceval c1 st st').

Tactic Notation "ceval_cases" tactic(first) ident(c) :=

first;

[ Case_aux c "E_Skip" | Case_aux c "E_Ass" | Case_aux c "E_Seq"

| Case_aux c "E_IfTrue" | Case_aux c "E_IfFalse"

| Case_aux c "E_WhileEnd" | Case_aux c "E_WhileLoop"

| Case_aux c "E_Havoc" ].

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.

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

∀st st', c / st ⇓ st' → P st → Q st'.

Notation "{{ P }} c {{ Q }}" := (hoare_triple P c Q)

(at level 90, c at next level)

: hoare_spec_scope.

Complete the Hoare rule for HAVOC commands below by defining
havoc_pre and prove that the resulting rule is correct.

Definition havoc_pre (X : id) (Q : Assertion) : Assertion :=

(* FILL IN HERE *) admit.

Theorem hoare_havoc : ∀(Q : Assertion) (X : id),

{{ havoc_pre X Q }} HAVOC X {{ Q }}.

Proof.

(* FILL IN HERE *) Admitted.

End Himp.

☐

## Complete List of Hoare Logic Rules

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

(* $Date: 2014-12-01 15:16:30 -0500 (Mon, 01 Dec 2014) $ *)