HoareHoare Logic, Part I
Set Warnings "-notation-overridden,-parsing".
Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
Require Import Coq.omega.Omega.
From PLF Require Import Imp.
From PLF Require Import Maps.
Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
Require Import Coq.omega.Omega.
From PLF Require Import Imp.
From PLF Require Import Maps.
In the final chaper of Logical Foundations (Software
Foundations, volume 1), we began 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 this volume 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 Floyd-Hoare 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.
This chapter:
Goals:
Plan:
- 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 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
- A systematic method for reasoning about the correctness of particular programs in Imp
- a natural notation for program specifications and
- a compositional proof technique for program correctness
- assertions (Hoare Triples)
- proof rules
- decorated programs
- loop invariants
- examples
Assertions
Exercise: 1 star, optional (assertions)
Paraphrase the following assertions in English (or your favorite natural language).
Module ExAssertions.
Definition as_{1} : Assertion := fun st ⇒ st X = 3.
Definition as_{2} : Assertion := fun st ⇒ st X ≤ st Y.
Definition as_{3} : Assertion :=
fun st ⇒ st X = 3 ∨ st X ≤ st Y.
Definition as_{4} : Assertion :=
fun st ⇒ st Z * st Z ≤ st X ∧
¬ (((S (st Z)) * (S (st Z))) ≤ st X).
Definition as_{5} : Assertion := fun st ⇒ True.
Definition as_{6} : Assertion := fun st ⇒ False.
(* FILL IN HERE *)
End ExAssertions.
☐
Definition as_{1} : Assertion := fun st ⇒ st X = 3.
Definition as_{2} : Assertion := fun st ⇒ st X ≤ st Y.
Definition as_{3} : Assertion :=
fun st ⇒ st X = 3 ∨ st X ≤ st Y.
Definition as_{4} : Assertion :=
fun st ⇒ st Z * st Z ≤ st X ∧
¬ (((S (st Z)) * (S (st Z))) ≤ st X).
Definition as_{5} : Assertion := fun st ⇒ True.
Definition as_{6} : Assertion := fun st ⇒ False.
(* FILL IN HERE *)
End ExAssertions.
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).
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.
∀ st, P st → Q st.
Notation "P ->> Q" := (assert_implies P Q)
(at level 80) : hoare_spec_scope.
Open Scope 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.)
We'll also want the "iff" variant of implication between
assertions:
Notation "P <<->> Q" :=
(P ->> Q ∧ Q ->> P) (at level 80) : hoare_spec_scope.
(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."
Definition hoare_triple
(P:Assertion) (c:com) (Q:Assertion) : Prop :=
∀ st st',
c / st \\ st' →
P st →
Q st'.
(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.
(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)}}
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}}
Theorem hoare_post_true : ∀ (P Q : Assertion) c,
(∀ st, Q st) →
{{P}} c {{Q}}.
Theorem hoare_pre_false : ∀ (P Q : Assertion) c,
(∀ st, ~(P st)) →
{{P}} c {{Q}}.
(∀ st, Q st) →
{{P}} c {{Q}}.
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
Assignment
{{ Y = 1 }} X ::= Y {{ X = 1 }}
In English: if we start out in a state where the value of Y
is 1 and we assign Y to X, then we'll finish in a
state where X is 1.
That is, the property of being equal to 1 gets transferred
from Y to X.
{{ Y + Z = 1 }} X ::= Y + Z {{ X = 1 }}
the same property (being equal to one) gets transferred to
X from the expression Y + Z on the right-hand side of
the assignment.
{{ a = 1 }} X ::= a {{ X = 1 }}
is a valid Hoare triple.
{{ Q [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 (t_update st X (aeval st a)).
Notation "P [ X |-> a ]" := (assn_sub X a P) (at level 10).
fun (st : state) ⇒
P (t_update st X (aeval st a)).
Notation "P [ X |-> a ]" := (assn_sub X a P) (at level 10).
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
For a more interesting example, suppose P' is (X ≤ 5) [X |->
X+1]. Formally, P' is the Coq expression
Now, using the concept of substitution, 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)
(t_update st X (aeval st (ANum 3))),
which simplifies to
(fun st' ⇒ st' X ≤ 5)
(t_update st X (aeval st (ANum 3))),
fun st ⇒
(fun st' ⇒ st' X ≤ 5)
(t_update st X 3)
and further simplifies to
(fun st' ⇒ st' X ≤ 5)
(t_update st X 3)
fun st ⇒
((t_update st X 3) X) ≤ 5)
and finally to
((t_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)
(t_update st X (aeval st (APlus (AId X) (ANum 1)))),
which simplifies to
(fun st' ⇒ st' X ≤ 5)
(t_update st X (aeval st (APlus (AId X) (ANum 1)))),
fun st ⇒
(((t_update st X (aeval st (APlus (AId X) (ANum 1))))) X) ≤ 5
and further simplifies to
(((t_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}}.
{{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.
(* WORKED IN CLASS *)
apply hoare_asgn. Qed.
{{(fun st ⇒ st X = 3) [X |-> ANum 3]}}
(X ::= (ANum 3))
{{fun st ⇒ st X = 3}}.
Proof.
(* WORKED IN CLASS *)
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 (use the names assn_sub_ex_{1}
and assn_sub_ex_{2}) 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 *)
☐
Exercise: 2 stars, recommended (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 }} |
(* FILL IN HERE *)
☐
Exercise: 3 stars, advanced (hoare_asgn_fwd)
However, by using a parameter m (a Coq number) 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) |
Theorem hoare_asgn_fwd :
∀ m a P,
{{fun st ⇒ P st ∧ st X = m}}
X ::= a
{{fun st ⇒ P (t_update st X m)
∧ st X = aeval (t_update st X m) a }}.
Proof.
(* FILL IN HERE *) Admitted.
☐
∀ m a P,
{{fun st ⇒ P st ∧ st X = m}}
X ::= a
{{fun st ⇒ P (t_update st X m)
∧ st X = aeval (t_update st X m) a }}.
Proof.
(* 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 (t_update st X m) ∧ | |
st X = aeval (t_update st X m) a }} |
Theorem hoare_asgn_fwd_exists :
∀ a P,
{{fun st ⇒ P st}}
X ::= a
{{fun st ⇒ ∃ m, P (t_update st X m) ∧
st X = aeval (t_update st X m) a }}.
Proof.
intros a P.
(* FILL IN HERE *) Admitted.
☐
∀ a P,
{{fun st ⇒ P st}}
X ::= a
{{fun st ⇒ ∃ m, P (t_update st X m) ∧
st X = aeval (t_update st X m) a }}.
Proof.
intros 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 can capture this observation with the
following rule:
{{P'}} c {{Q}} | |
P <<->> P' | (hoare_consequence_pre_equiv) |
{{P}} c {{Q}} |
{{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}}.
Theorem hoare_consequence_post : ∀ (P Q Q' : Assertion) c,
{{P}} c {{Q'}} →
Q' ->> Q →
{{P}} c {{Q}}.
{{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 can 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.
(* WORKED IN CLASS *)
apply hoare_consequence_pre
with (P' := (fun st ⇒ st X = 1) [X |-> ANum 1]).
apply hoare_asgn.
intros st H. unfold assn_sub, t_update. simpl. reflexivity.
Qed.
{{fun st ⇒ True}} (X ::= (ANum 1)) {{fun st ⇒ st X = 1}}.
Proof.
(* WORKED IN CLASS *)
apply hoare_consequence_pre
with (P' := (fun st ⇒ st X = 1) [X |-> ANum 1]).
apply hoare_asgn.
intros st H. unfold assn_sub, t_update. simpl. reflexivity.
Qed.
Finally, for convenience in 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}} |
Theorem hoare_consequence : ∀ (P P' Q Q' : Assertion) c,
{{P'}} c {{Q'}} →
P ->> P' →
Q' ->> Q →
{{P}} c {{Q}}.
{{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.
{{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 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.
(∀ 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. ("All the remaining goals
are on the shelf," means that we've finished all our top-level
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'].
∀ (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.
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.
(∃ 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.
{{ 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}}.
{{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 }} 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}}.
{{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.
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 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 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}:
Here's an example of a program involving both assignment and
sequencing.
{{ 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.
- (* right part of seq *)
apply hoare_skip.
- (* left part of seq *)
eapply hoare_consequence_pre. apply hoare_asgn.
intros st H. subst. reflexivity.
Qed.
{{fun st ⇒ aeval st a = n}}
(X ::= a;; SKIP)
{{fun st ⇒ st 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.
We typically use hoare_seq in conjunction with
hoare_consequence_pre and the eapply tactic, as in this
example.
Exercise: 2 stars, recommended (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 }}
(Note the use of "->>" decorations, each marking a use of
hoare_consequence_pre.)
{{ 1 = 1 }}
X ::= 1;;
{{ X = 1 }} ->>
{{ X = 1 ∧ 2 = 2 }}
Y ::= 2
{{ X = 1 ∧ Y = 2 }}
Example hoare_asgn_example4 :
{{fun st ⇒ True}} (X ::= (ANum 1);; Y ::= (ANum 2))
{{fun st ⇒ st X = 1 ∧ st Y = 2}}.
Proof.
(* FILL IN HERE *) Admitted.
☐
{{fun st ⇒ True}} (X ::= (ANum 1);; Y ::= (ANum 2))
{{fun st ⇒ st X = 1 ∧ st Y = 2}}.
Proof.
(* FILL IN HERE *) Admitted.
Exercise: 3 stars (swap_exercise)
Write an Imp program c that swaps the values of X and Y and show that it satisfies the following specification:
{{X ≤ Y}} c {{Y ≤ X}}
Your proof should not need to use unfold hoare_triple.
Definition swap_program : com
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Theorem swap_exercise :
{{fun st ⇒ st X ≤ st Y}}
swap_program
{{fun st ⇒ st Y ≤ st X}}.
Proof.
(* FILL IN HERE *) Admitted.
☐
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
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}} c_{1} {{Q}} | |
{{P}} c_{2} {{Q}} | |
{{P}} IFB b THEN c_{1} ELSE c_{2} {{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}} c_{1} {{Q}} | |
{{P ∧ ~b}} c_{2} {{Q}} | (hoare_if) |
{{P}} IFB b THEN c_{1} ELSE c_{2} FI {{Q}} |
A couple of useful facts about bassn:
Lemma bexp_eval_true : ∀ b st,
beval st b = true → (bassn b) st.
Lemma bexp_eval_false : ∀ b st,
beval st b = false → ¬ ((bassn b) st).
beval st b = true → (bassn b) st.
Lemma bexp_eval_false : ∀ b st,
beval st b = false → ¬ ((bassn b) st).
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}}.
{{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.
- (* 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.
intros P Q b c_{1} c_{2} 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 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}}.
{{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.
- (* Then *)
eapply hoare_consequence_pre. apply hoare_asgn.
unfold bassn, assn_sub, t_update, assert_implies.
simpl. intros st [_ H].
apply beq_nat_true in H.
rewrite H. omega.
- (* Else *)
eapply hoare_consequence_pre. apply hoare_asgn.
unfold assn_sub, t_update, assert_implies.
simpl; intros st _. omega.
Qed.
(* WORKED IN CLASS *)
apply hoare_if.
- (* Then *)
eapply hoare_consequence_pre. apply hoare_asgn.
unfold bassn, assn_sub, t_update, assert_implies.
simpl. intros st [_ H].
apply beq_nat_true in H.
rewrite H. omega.
- (* Else *)
eapply hoare_consequence_pre. apply hoare_asgn.
unfold assn_sub, t_update, assert_implies.
simpl; intros st _. omega.
Qed.
Exercise: 2 stars (if_minus_plus)
Prove the following hoare triple using hoare_if. Do not use unfold hoare_triple.
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.
☐
{{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)
In this exercise we consider extending Imp with "one-sided 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.
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).
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 one-sided conditionals?
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_WhileFalse : ∀ (b_{1} : bexp) (st : state) (c_{1} : com),
beval st b_{1} = false → (WHILE b_{1} DO c_{1} END) / st \\ st
| E_WhileTrue : ∀ (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''
(* FILL IN HERE *)
where "c_{1} '/' st '\\' st'" := (ceval c_{1} st st').
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_WhileFalse : ∀ (b_{1} : bexp) (st : state) (c_{1} : com),
beval st b_{1} = false → (WHILE b_{1} DO c_{1} END) / st \\ st
| E_WhileTrue : ∀ (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''
(* FILL IN HERE *)
where "c_{1} '/' st '\\' st'" := (ceval c_{1} st st').
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.
∀ 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_if_{1}, 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 hoare_if1_good 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 }}
IF_{1} Y ≠ 0 THEN
X ::= X + Y
FI
{{ X = Z }}
IF_{1} Y ≠ 0 THEN
X ::= X + Y
FI
{{ X = Z }}
Lemma hoare_if1_good :
{{ fun st ⇒ st X + st Y = st Z }}
IF_{1} 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 If_{1}.
☐
{{ fun st ⇒ st X + st Y = st Z }}
IF_{1} 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 If_{1}.
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}}
{{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}} |
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)}}.
{{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.
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.
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.
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.
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.
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}}.
{{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, t_update. simpl.
intros st [H_{1} H_{2}]. apply leb_complete in H_{2}. omega.
unfold bassn, assert_implies. intros st [Hle Hb].
simpl in Hb. destruct (leb (st X) 2) eqn : Heqle.
exfalso. apply Hb; reflexivity.
apply leb_iff_conv in Heqle. omega.
Qed.
eapply hoare_consequence_post.
apply hoare_while.
eapply hoare_consequence_pre.
apply hoare_asgn.
unfold bassn, assn_sub, assert_implies, t_update. simpl.
intros st [H_{1} H_{2}]. apply leb_complete in H_{2}. omega.
unfold bassn, assert_implies. intros st [Hle Hb].
simpl in Hb. destruct (leb (st X) 2) eqn : Heqle.
exfalso. apply Hb; reflexivity.
apply leb_iff_conv in Heqle. omega.
Qed.
We can use the WHILE rule to prove the following Hoare triple...
Theorem always_loop_hoare : ∀ P Q,
{{P}} WHILE BTrue DO SKIP END {{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.
- (* Loop body preserves invariant *)
apply hoare_post_true. intros st. apply I.
- (* Loop invariant and negated guard imply postcondition *)
simpl. intros st [Hinv Hguard].
exfalso. apply Hguard. reflexivity.
- (* 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.
- (* Loop body preserves invariant *)
apply hoare_post_true. intros st. apply I.
- (* Loop invariant and negated guard imply postcondition *)
simpl. intros st [Hinv Hguard].
exfalso. apply Hguard. reflexivity.
- (* 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 only when the command terminates. If the command
doesn't terminate, we can prove anything we like about the
post-condition.
Hoare rules that only talk about what happens when commands
terminate (without proving that they do) 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. (You may recall that the evaluation rule is given in an example in the Auto chapter. Try to figure it out yourself here rather than peeking.)
Module RepeatExercise.
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.
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.
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).
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.
Inductive ceval : state → com → state → Prop :=
| E_Skip : ∀ st,
ceval st SKIP st
| E_Ass : ∀ st a_{1} n X,
aeval st a_{1} = n →
ceval st (X ::= a_{1}) (t_update st X n)
| E_Seq : ∀ c_{1} c_{2} st st' st'',
ceval st c_{1} st' →
ceval st' c_{2} st'' →
ceval st (c_{1} ;; c_{2}) st''
| E_IfTrue : ∀ st st' b_{1} c_{1} c_{2},
beval st b_{1} = true →
ceval st c_{1} st' →
ceval st (IFB b_{1} THEN c_{1} ELSE c_{2} FI) st'
| E_IfFalse : ∀ st st' b_{1} c_{1} c_{2},
beval st b_{1} = false →
ceval st c_{2} st' →
ceval st (IFB b_{1} THEN c_{1} ELSE c_{2} FI) st'
| E_WhileFalse : ∀ b_{1} st c_{1},
beval st b_{1} = false →
ceval st (WHILE b_{1} DO c_{1} END) st
| E_WhileTrue : ∀ st st' st'' b_{1} c_{1},
beval st b_{1} = true →
ceval st c_{1} st' →
ceval st' (WHILE b_{1} DO c_{1} END) st'' →
ceval st (WHILE b_{1} DO c_{1} END) st''
(* FILL IN HERE *)
.
| E_Skip : ∀ st,
ceval st SKIP st
| E_Ass : ∀ st a_{1} n X,
aeval st a_{1} = n →
ceval st (X ::= a_{1}) (t_update st X n)
| E_Seq : ∀ c_{1} c_{2} st st' st'',
ceval st c_{1} st' →
ceval st' c_{2} st'' →
ceval st (c_{1} ;; c_{2}) st''
| E_IfTrue : ∀ st st' b_{1} c_{1} c_{2},
beval st b_{1} = true →
ceval st c_{1} st' →
ceval st (IFB b_{1} THEN c_{1} ELSE c_{2} FI) st'
| E_IfFalse : ∀ st st' b_{1} c_{1} c_{2},
beval st b_{1} = false →
ceval st c_{2} st' →
ceval st (IFB b_{1} THEN c_{1} ELSE c_{2} FI) st'
| E_WhileFalse : ∀ b_{1} st c_{1},
beval st b_{1} = false →
ceval st (WHILE b_{1} DO c_{1} END) st
| E_WhileTrue : ∀ st st' st'' b_{1} c_{1},
beval st b_{1} = true →
ceval st c_{1} st' →
ceval st' (WHILE b_{1} DO c_{1} END) st'' →
ceval st (WHILE b_{1} DO c_{1} END) st''
(* FILL IN HERE *)
.
A couple of definitions from above, copied here so they use the
new ceval.
Notation "c_{1} '/' st '\\' st'" := (ceval st c_{1} 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).
(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 \\
t_update (t_update empty_state X 1) Y 1.
Proof.
(* FILL IN HERE *) Admitted.
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 \\
t_update (t_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 }}
Summary
(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}} |
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.
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_WhileFalse : ∀ (b_{1} : bexp) (st : state) (c_{1} : com),
beval st b_{1} = false → (WHILE b_{1} DO c_{1} END) / st \\ st
| E_WhileTrue : ∀ (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').
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_WhileFalse : ∀ (b_{1} : bexp) (st : state) (c_{1} : com),
beval st b_{1} = false → (WHILE b_{1} DO c_{1} END) / st \\ st
| E_WhileTrue : ∀ (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.
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.
∀ 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
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Theorem hoare_havoc : ∀ (Q : Assertion) (X : id),
{{ havoc_pre X Q }} HAVOC X {{ Q }}.
Proof.
(* FILL IN HERE *) Admitted.
End Himp.
☐
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Theorem hoare_havoc : ∀ (Q : Assertion) (X : id),
{{ havoc_pre X Q }} HAVOC X {{ Q }}.
Proof.
(* FILL IN HERE *) Admitted.
End Himp.