HoareHoare Logic, Part I
Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
From PLF Require Import Maps.
From Coq Require Import Bool.Bool.
From Coq Require Import Arith.Arith.
From Coq Require Import Arith.EqNat.
From Coq Require Import Arith.PeanoNat. Import Nat.
From Coq Require Import Lia.
From PLF Require Export Imp.
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.
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 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.
- 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
Assertions
For example,
- fun st ⇒ st X = 3 holds if the value of X according to st is 3,
- fun st ⇒ True always holds, and
- fun st ⇒ False never holds.
Exercise: 1 star, standard, optional (assertions)
Paraphrase the following assertions in English (or your favorite natural language).Module ExAssertions.
Definition assn1 : Assertion := fun st ⇒ st X ≤ st Y.
Definition assn2 : Assertion :=
fun st ⇒ st X = 3 ∨ st X ≤ st Y.
Definition assn3 : Assertion :=
fun st ⇒ st Z × st Z ≤ st X ∧
¬ (((S (st Z)) × (S (st Z))) ≤ st X).
Definition assn4 : Assertion :=
fun st ⇒ st Z = max (st X) (st Y).
(* FILL IN HERE *)
End ExAssertions.
☐
fun st ⇒ st X = m
X = m
Definition assert_implies (P Q : Assertion) : Prop :=
∀ st, P st → Q st.
Declare Scope hoare_spec_scope.
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:
Notations for Assertions
Definition Aexp : Type := state → nat.
Definition assert_of_Prop (P : Prop) : Assertion := fun _ ⇒ P.
Definition Aexp_of_nat (n : nat) : Aexp := fun _ ⇒ n.
Definition Aexp_of_aexp (a : aexp) : Aexp := fun st ⇒ aeval st a.
Coercion assert_of_Prop : Sortclass >-> Assertion.
Coercion Aexp_of_nat : nat >-> Aexp.
Coercion Aexp_of_aexp : aexp >-> Aexp.
Arguments assert_of_Prop /.
Arguments Aexp_of_nat /.
Arguments Aexp_of_aexp /.
Declare Scope assertion_scope.
Bind Scope assertion_scope with Assertion.
Bind Scope assertion_scope with Aexp.
Delimit Scope assertion_scope with assertion.
Notation assert P := (P%assertion : Assertion).
Notation mkAexp a := (a%assertion : Aexp).
Notation "~ P" := (fun st ⇒ ¬ assert P st) : assertion_scope.
Notation "P /\ Q" := (fun st ⇒ assert P st ∧ assert Q st) : assertion_scope.
Notation "P \/ Q" := (fun st ⇒ assert P st ∨ assert Q st) : assertion_scope.
Notation "P -> Q" := (fun st ⇒ assert P st → assert Q st) : assertion_scope.
Notation "P <-> Q" := (fun st ⇒ assert P st ↔ assert Q st) : assertion_scope.
Notation "a = b" := (fun st ⇒ mkAexp a st = mkAexp b st) : assertion_scope.
Notation "a <> b" := (fun st ⇒ mkAexp a st ≠ mkAexp b st) : assertion_scope.
Notation "a <= b" := (fun st ⇒ mkAexp a st ≤ mkAexp b st) : assertion_scope.
Notation "a < b" := (fun st ⇒ mkAexp a st < mkAexp b st) : assertion_scope.
Notation "a >= b" := (fun st ⇒ mkAexp a st ≥ mkAexp b st) : assertion_scope.
Notation "a > b" := (fun st ⇒ mkAexp a st > mkAexp b st) : assertion_scope.
Notation "a + b" := (fun st ⇒ mkAexp a st + mkAexp b st) : assertion_scope.
Notation "a - b" := (fun st ⇒ mkAexp a st - mkAexp b st) : assertion_scope.
Notation "a * b" := (fun st ⇒ mkAexp a st × mkAexp b st) : assertion_scope.
One small limitation of this approach is that we don't have
an automatic way to coerce function applications that appear
within an assertion to make appropriate use of the state.
Instead, we use an explicit ap operator to lift the function.
Definition ap {X} (f : nat → X) (x : Aexp) :=
fun st ⇒ f (x st).
Definition ap2 {X} (f : nat → nat → X) (x : Aexp) (y : Aexp) (st : state) :=
f (x st) (y st).
Module ExPrettyAssertions.
Definition ex1 : Assertion := X = 3.
Definition ex2 : Assertion := True.
Definition ex3 : Assertion := False.
Definition assn1 : Assertion := X ≤ Y.
Definition assn2 : Assertion := X = 3 ∨ X ≤ Y.
Definition assn3 : Assertion :=
Z × Z ≤ X ∧ ¬ (((ap S Z) × (ap S Z)) ≤ X).
Definition assn4 : Assertion :=
Z = ap2 max X Y.
End ExPrettyAssertions.
Hoare Triples, Informally
{P} c {Q}
- If command c begins execution in a state satisfying assertion P,
- and if c eventually terminates in some final state,
- then that final state will satisfy the assertion Q.
{{P}} c {{Q}}
- {{X = 0}} X := X + 1 {{X = 1}} is a valid Hoare triple,
stating that command X := X + 1 would transform a state in
which X = 0 to a state in which X = 1.
- ∀ m, {{X = m}} X := X + 1 {{X = m + 1}}, is a proposition stating that the Hoare triple {{X = m}} X := X + m {{X = m × 2}}) is valid for any choice of m. Note that m in the two assertions and the command in the middle is a reference to the Coq variable m, which is bound outside the Hoare triple, not to an Imp variable.
Exercise: 1 star, standard, optional (triples)
Paraphrase the following in English.1) {{True}} c {{X = 5}}
2) ∀ m, {{X = m}} c {{X = m + 5)}}
3) {{X ≤ Y}} c {{Y ≤ X}}
4) {{True}} c {{False}}
5) ∀ m,
{{X = m}}
c
{{Y = real_fact m}}
6) ∀ m,
{{X = m}}
c
{{(Z × Z) ≤ m ∧ ¬(((S Z) × (S Z)) ≤ m)}}
(* FILL IN HERE *)
☐
☐
Exercise: 1 star, standard, 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}}
(* FILL IN HERE *)
☐
☐
Definition hoare_triple
(P : Assertion) (c : com) (Q : Assertion) : Prop :=
∀ st st',
st =[ c ]=> st' →
P st →
Q st'.
Notation "{{ P }} c {{ Q }}" :=
(hoare_triple P c Q) (at level 90, c custom com at level 99)
: hoare_spec_scope.
Check ({{True}} X := 0 {{True}}).
Exercise: 1 star, standard (hoare_post_true)
Theorem hoare_post_true : ∀ (P Q : Assertion) c,
(∀ st, Q st) →
{{P}} c {{Q}}.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 1 star, standard (hoare_pre_false)
Theorem hoare_pre_false : ∀ (P Q : Assertion) c,
(∀ st, ¬ (P st)) →
{{P}} c {{Q}}.
Proof.
(* FILL IN HERE *) Admitted.
☐
Proof Rules
Assignment
{{ ??? }} X := Y {{ X = 1 }}
{{ Y = 1 }} X := Y {{ X = 1 }}
{{ ??? }} X := X + Y {{ X = 1 }}
{{ X + Y = 1 }} X := X + Y {{ X = 1 }}
{{ ??? }} X := a {{ Q }}
{{ Q [X ⊢> a] }} X := a {{ Q }}
{{ (X ≤ 5) [X ⊢> X + 1] }} (that is, X + 1 ≤ 5)
X := X + 1
{{ X ≤ 5 }}
{{ (X = 3) [X ⊢> 3] }} (that is, 3 = 3)
X := 3
{{ X = 3 }}
{{ (0 ≤ X ∧ X ≤ 5) [X ⊢> 3] (that is, 0 ≤ 3 ∧ 3 ≤ 5)
X := 3
{{ 0 ≤ X ∧ X ≤ 5 }}
Definition assn_sub X a (P:Assertion) : Assertion :=
fun (st : state) ⇒
P (X !-> aeval st a ; st).
Notation "P [ X ⊢> a ]" := (assn_sub X a P)
(at level 10, X at next level, a custom com).
That is, P [X ⊢> a] stands for an assertion -- let's call it P' --
that is just like P except that, wherever P looks up the
variable X in the current state, P' instead uses the value
of the expression a.
To see how this works, let's calculate what happens with a couple
of examples. First, suppose P' is (X ≤ 5) [X ⊢> 3] -- that
is, more formally, P' is the Coq expression
fun st ⇒
(fun st' ⇒ st' X ≤ 5)
(X !-> aeval st 3 ; st),
which simplifies to
fun st ⇒
(fun st' ⇒ st' X ≤ 5)
(X !-> 3 ; st)
and further simplifies to
fun st ⇒
((X !-> 3 ; st) X) ≤ 5
and finally to
fun st ⇒
3 ≤ 5.
That is, P' is the assertion that 3 is less than or equal to
5 (as expected).
For a more interesting example, suppose P' is (X ≤ 5) [X ⊢>
X + 1]. Formally, P' is the Coq expression
fun st ⇒
(fun st' ⇒ st' X ≤ 5)
(X !-> aeval st (X + 1) ; st),
which simplifies to
fun st ⇒
(X !-> aeval st (X + 1) ; st) X ≤ 5
and further simplifies to
fun st ⇒
(aeval st (X + 1)) ≤ 5.
That is, P' is the assertion that X + 1 is at most 5.
Now, using the concept of substitution, we can give the precise
proof rule for assignment:
We can prove formally that this rule is indeed valid.
fun st ⇒
(fun st' ⇒ st' X ≤ 5)
(X !-> aeval st 3 ; st),
fun st ⇒
(fun st' ⇒ st' X ≤ 5)
(X !-> 3 ; st)
fun st ⇒
((X !-> 3 ; st) X) ≤ 5
fun st ⇒
3 ≤ 5.
fun st ⇒
(fun st' ⇒ st' X ≤ 5)
(X !-> aeval st (X + 1) ; st),
fun st ⇒
(X !-> aeval st (X + 1) ; st) X ≤ 5
fun st ⇒
(aeval st (X + 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 :
{{(X < 5) [X ⊢> X + 1]}}
X := X + 1
{{X < 5}}.
Proof.
(* WORKED IN CLASS *)
apply hoare_asgn. Qed.
(Of course, what we'd probably prefer is to prove this
simpler triple:
{{X < 4}} X := X + 1 {{X < 5}}
We will see how to do so in the next section.
1) {{ ??? }}
X ::= 2 × X
{{ X ≤ 10 }}
2) {{ ??? }}
X := 3
{{ 0 ≤ X ∧ X ≤ 5 }}
...using the names assn_sub_ex1 and assn_sub_ex2, and prove
both with just apply hoare_asgn. If you find that tactic doesn't
suffice, double check that you have completed the triple properly.
{{X < 4}} X := X + 1 {{X < 5}}
Exercise: 2 stars, standard, optional (hoare_asgn_examples)
Complete these Hoare triples...1) {{ ??? }}
X ::= 2 × X
{{ X ≤ 10 }}
2) {{ ??? }}
X := 3
{{ 0 ≤ X ∧ X ≤ 5 }}
(* FILL IN HERE *)
(* Do not modify the following line: *)
Definition manual_grade_for_hoare_asgn_examples : option (nat×string) := None.
☐
Exercise: 2 stars, standard, especially useful (hoare_asgn_wrong)
The assignment rule looks backward to almost everyone the first time they see it. If it still seems puzzling 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 *)
(* Do not modify the following line: *)
Definition manual_grade_for_hoare_asgn_wrong : option (nat×string) := None.
☐
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' = (X !-> m ; st)) |
Theorem hoare_asgn_fwd :
∀ m a P,
{{fun st ⇒ P st ∧ st X = m}}
X := a
{{fun st ⇒ P (X !-> m ; st)
∧ st X = aeval (X !-> m ; st) a }}.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, advanced, optional (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. Prove that it is correct.(hoare_asgn_fwd_exists) | |
{{fun st => P st}} | |
X := a | |
{{fun st => exists m, P (X !-> m ; st) /\ | |
st X = aeval (X !-> m ; st) a }} |
Theorem hoare_asgn_fwd_exists :
∀ a P,
{{fun st ⇒ P st}}
X := a
{{fun st ⇒ ∃ m, P (X !-> m ; st) ∧
st X = aeval (X !-> m ; st) a }}.
Proof.
(* FILL IN HERE *) Admitted.
☐
Consequence
{{(X = 3) [X ⊢> 3]}} X := 3 {{X = 3}},
{{True}} X := 3 {{X = 3}}
{{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}}.
Proof.
unfold hoare_triple, "->>".
intros P P' Q c Hhoare Himp st st' Heval Hpre.
apply Hhoare with (st := st).
- assumption.
- apply Himp. assumption.
Qed.
unfold hoare_triple, "->>".
intros P P' Q c Hhoare Himp st st' Heval Hpre.
apply Hhoare with (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.
unfold hoare_triple, "->>".
intros P Q Q' c Hhoare Himp st st' Heval Hpre.
apply Himp.
apply Hhoare with (st := st).
- assumption.
- assumption.
Qed.
unfold hoare_triple, "->>".
intros P Q Q' c Hhoare Himp st st' Heval Hpre.
apply Himp.
apply Hhoare with (st := st).
- assumption.
- assumption.
Qed.
For example, we can use the first consequence rule like this:
{{ True }} ->>
{{ (X = 1) [X ⊢> 1] }}
X := 1
{{ X = 1 }}
Or, formally...
{{ True }} ->>
{{ (X = 1) [X ⊢> 1] }}
X := 1
{{ X = 1 }}
Example hoare_asgn_example1 :
{{True}} X := 1 {{X = 1}}.
Proof.
(* WORKED IN CLASS *)
apply hoare_consequence_pre with (P' := (X = 1) [X ⊢> 1]).
- apply hoare_asgn.
- unfold "->>", assn_sub, t_update.
intros st _. simpl. reflexivity.
Qed.
We can also use it to prove the example mentioned earlier.
{{ X < 4 }} ->>
{{ (X < 5)[X ⊢> X + 1] }}
X := X + 1
{{ X < 5 }}
Or, formally ...
{{ X < 4 }} ->>
{{ (X < 5)[X ⊢> X + 1] }}
X := X + 1
{{ X < 5 }}
Example assn_sub_example2 :
{{X < 4}}
X := X + 1
{{X < 5}}.
Proof.
(* WORKED IN CLASS *)
apply hoare_consequence_pre with (P' := (X < 5) [X ⊢> X + 1]).
- apply hoare_asgn.
- unfold "->>", assn_sub, t_update.
intros st H. simpl in ×. lia.
Qed.
Finally, here is 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}}
{{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 Htriple Hpre Hpost.
apply hoare_consequence_pre with (P' := P').
- apply hoare_consequence_post with (Q' := Q').
+ assumption.
+ assumption.
- assumption.
Qed.
intros P P' Q Q' c Htriple Hpre Hpost.
apply hoare_consequence_pre with (P' := P').
- apply hoare_consequence_post with (Q' := Q').
+ assumption.
+ assumption.
- assumption.
Qed.
Automation
Hint Unfold assert_implies hoare_triple assn_sub t_update : core.
Hint Unfold assert_of_Prop Aexp_of_nat Aexp_of_aexp : core.
Also recall that auto will search for a proof involving intros
and apply. By default, the theorems that it will apply include
any of the local hypotheses, as well as theorems in a core
database.
The proof of hoare_consequence_pre, repeated below, looks
like an opportune place for such automation, because all it does
is unfold, intros, and apply. It uses assumption, too,
but that's just application of a hypothesis.
Theorem hoare_consequence_pre' : ∀ (P P' Q : Assertion) c,
{{P'}} c {{Q}} →
P ->> P' →
{{P}} c {{Q}}.
Proof.
unfold hoare_triple, "->>".
intros P P' Q c Hhoare Himp st st' Heval Hpre.
apply Hhoare with (st := st).
- assumption.
- apply Himp. assumption.
Qed.
Merely using auto, though, doesn't complete the proof.
Theorem hoare_consequence_pre'' : ∀ (P P' Q : Assertion) c,
{{P'}} c {{Q}} →
P ->> P' →
{{P}} c {{Q}}.
Proof.
auto. (* no progress *)
Abort.
The problem is the apply Hhoare with... part of the proof. Coq
isn't able to figure out how to instantiate st without some help
from us. Recall, though, that there are versions of many tactics
that will use existential variables to make progress even when
the regular versions of those tactics would get stuck.
Here, the eapply tactic will introduce an existential variable
?st as a placeholder for st, and eassumption will
instantiate ?st with st when it discovers st in assumption
Heval. By using eapply we are essentially telling Coq, "Be
patient: The missing part is going to be filled in later in the
proof."
Theorem hoare_consequence_pre''' : ∀ (P P' Q : Assertion) c,
{{P'}} c {{Q}} →
P ->> P' →
{{P}} c {{Q}}.
Proof.
unfold hoare_triple, "->>".
intros P P' Q c Hhoare Himp st st' Heval Hpre.
eapply Hhoare.
- eassumption.
- apply Himp. assumption.
Qed.
Tactic eauto will use eapply as part of its proof search.
So, the entire proof can be done in just one line.
Theorem hoare_consequence_pre'''' : ∀ (P P' Q : Assertion) c,
{{P'}} c {{Q}} →
P ->> P' →
{{P}} c {{Q}}.
Proof.
eauto.
Qed.
Of course, it's hard to predict that eauto suffices here
without having gone through the original proof of
hoare_consequence_pre to see the tactics it used. But now that
we know eauto works, it's a good bet that it will also work for
hoare_consequence_post.
Theorem hoare_consequence_post' : ∀ (P Q Q' : Assertion) c,
{{P}} c {{Q'}} →
Q' ->> Q →
{{P}} c {{Q}}.
Proof.
eauto.
Qed.
We can also use eapply to streamline a proof,
hoare_asgn_example1, that we did earlier as an example of using
the consequence rule:
Example hoare_asgn_example1' :
{{True}} X := 1 {{X = 1}}.
Proof.
eapply hoare_consequence_pre. (* no need to state an assertion *)
- apply hoare_asgn.
- unfold "->>", assn_sub, t_update.
intros st _. simpl. reflexivity.
Qed.
The final bullet of that proof also looks like a candidate for
automation.
Example hoare_asgn_example1'' :
{{True}} X := 1 {{X = 1}}.
Proof.
eapply hoare_consequence_pre.
- apply hoare_asgn.
- auto.
Qed.
Now we have quite a nice proof script: it simply identifies the
Hoare rules that need to be used and leaves the remaining
low-level details up to Coq to figure out.
By now it might be apparent that the entire proof could be
automated if we added hoare_consequence_pre and hoare_asgn to
the hint database. We won't do that in this chapter, so that we
can get a better understanding of when and how the Hoare rules are
used. In the next chapter, Hoare2, we'll dive deeper into
automating entire proofs of Hoare triples.
The other example of using consequence that we did earlier,
hoare_asgn_example2, requires a little more work to automate.
We can streamline the first line with eapply, but we can't just use
auto for the final bullet, since it needs omega.
Example assn_sub_example2' :
{{X < 4}}
X := X + 1
{{X < 5}}.
Proof.
eapply hoare_consequence_pre.
- apply hoare_asgn.
- auto. (* no progress *)
unfold "->>", assn_sub, t_update.
intros st H. simpl in ×. lia.
Qed.
Let's introduce our own tactic to handle both that bullet and the
bullet from example 1:
Ltac assn_auto :=
try auto; (* as in example 1, above *)
try (unfold "->>", assn_sub, t_update;
intros; simpl in *; lia). (* as in example 2 *)
Example assn_sub_example2'' :
{{X < 4}}
X := X + 1
{{X < 5}}.
Proof.
eapply hoare_consequence_pre.
- apply hoare_asgn.
- assn_auto.
Qed.
Example hoare_asgn_example1''':
{{True}} X := 1 {{X = 1}}.
Proof.
eapply hoare_consequence_pre.
- apply hoare_asgn.
- assn_auto.
Qed.
Again, we have quite a nice proof script. All the low-level
details of proof about assertions have been taken care of
automatically. Of course, assn_auto isn't able to prove
everything we could possibly want to know about assertions --
there's no magic here! But it's good enough so far.
Exercise: 2 stars, standard (hoare_asgn_examples_2)
Prove these triples. Try to make your proof scripts as nicely automated as those above.Example assn_sub_ex1' :
{{ X ≤ 5 }}
X := 2 × X
{{ X ≤ 10 }}.
Proof.
(* FILL IN HERE *) Admitted.
Example assn_sub_ex2' :
{{ 0 ≤ 3 ∧ 3 ≤ 5 }}
X := 3
{{ 0 ≤ X ∧ X ≤ 5 }}.
Proof.
(* FILL IN HERE *) Admitted.
☐
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.
unfold hoare_triple.
intros P Q R c1 c2 H1 H2 st st' H12 Pre.
inversion H12; subst.
eauto.
Qed.
unfold hoare_triple.
intros P Q R c1 c2 H1 H2 st st' H12 Pre.
inversion H12; subst.
eauto.
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, 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.
Here's an example of a program involving sequencing. Note the use
of hoare_seq in conjunction with hoare_consequence_pre and the
eapply tactic.
Example hoare_asgn_example3 : ∀ (a:aexp) (n:nat),
{{a = n}}
X := a;
skip
{{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.
+ assn_auto.
Qed.
Informally, a nice way of displaying a proof using the sequencing
rule is as a "decorated program" where the intermediate assertion
Q is written between c1 and c2:
{{ a = n }}
X := a;
{{ X = n }} <--- decoration for Q
skip
{{ X = n }}
{{ 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.
We've started you off by providing a use of hoare_seq that
explicitly identifies X = 1 as the intermediate assertion.
{{ a = n }}
X := a;
{{ X = n }} <--- decoration for Q
skip
{{ X = n }}
Exercise: 2 stars, standard, especially useful (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 }}
Example hoare_asgn_example4 :
{{ True }}
X := 1;
Y := 2
{{ X = 1 ∧ Y = 2 }}.
Proof.
apply hoare_seq with (Q := (X = 1)%assertion).
(* The annotation %assertion is needed here to help Coq parse correctly. *)
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, standard (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}}
Definition swap_program : com
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Theorem swap_exercise :
{{X ≤ Y}}
swap_program
{{Y ≤ X}}.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 4 stars, standard (invalid_triple)
Show that{{ a = n }}
X := 3;; Y := a
{{ Y = n }}
specialize H with (a := your_a) (n := your_n)
Theorem invalid_triple : ¬ ∀ (a : aexp) (n : nat),
{{ a = n }}
X := 3; Y := a
{{ Y = n }}.
Proof.
unfold hoare_triple.
intros H.
(* FILL IN HERE *) Admitted.
☐
Conditionals
{{P}} c1 {{Q}} | |
{{P}} c2 {{Q}} | |
{{P}} if b then c1 else c2 {{Q}} |
{{ True }}
if X = 0
then Y := 2
else Y := X + 1
end
{{ X ≤ Y }}
{{P /\ b}} c1 {{Q}} | |
{{P /\ ~ b}} c2 {{Q}} | (hoare_if) |
{{P}} if b then c1 else c2 end {{Q}} |
Definition bassn b : Assertion :=
fun st ⇒ (beval st b = true).
Coercion bassn : bexp >-> Assertion.
Arguments bassn /.
A useful fact about bassn:
Lemma bexp_eval_false : ∀ b st,
beval st b = false → ¬ ((bassn b) st).
Proof. congruence. Qed.
Hint Resolve bexp_eval_false : core.
We mentioned the congruence tactic in passing in Auto when
building the find_rwd tactic. Like find_rwd, congruence is able to
automatically find that both beval st b = false and beval st b = true
are being assumed, notice the contradiction, and discriminate to complete
the proof.
Now we can formalize the Hoare proof rule for conditionals
and prove it correct.
Theorem hoare_if : ∀ P Q (b:bexp) c1 c2,
{{ P ∧ b }} c1 {{Q}} →
{{ P ∧ ¬ b}} c2 {{Q}} →
{{P}} if b then c1 else c2 end {{Q}}.
That is (unwrapping the notations):
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}} if b then c1 else c2 end {{Q}}.
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}} if b then c1 else c2 end {{Q}}.
Proof.
intros P Q b c1 c2 HTrue HFalse st st' HE HP.
inversion HE; subst; eauto.
Qed.
intros P Q b c1 c2 HTrue HFalse st st' HE HP.
inversion HE; subst; eauto.
Qed.
Example
Example if_example :
{{True}}
if (X = 0)
then Y := 2
else Y := X + 1
end
{{X ≤ Y}}.
Proof.
apply hoare_if.
- (* Then *)
eapply hoare_consequence_pre.
+ apply hoare_asgn.
+ assn_auto. (* no progress *)
unfold "->>", assn_sub, t_update, bassn.
simpl. intros st [_ H].
apply eqb_eq in H.
rewrite H. lia.
- (* Else *)
eapply hoare_consequence_pre.
+ apply hoare_asgn.
+ assn_auto.
Qed.
apply hoare_if.
- (* Then *)
eapply hoare_consequence_pre.
+ apply hoare_asgn.
+ assn_auto. (* no progress *)
unfold "->>", assn_sub, t_update, bassn.
simpl. intros st [_ H].
apply eqb_eq in H.
rewrite H. lia.
- (* Else *)
eapply hoare_consequence_pre.
+ apply hoare_asgn.
+ assn_auto.
Qed.
As we did earlier, it would be nice to eliminate all the low-level
proof script that isn't about the Hoare rules. Unfortunately, the
assn_auto tactic we wrote wasn't quite up to the job. Looking
at the proof of if_example, we can see why. We had to unfold a
definition (bassn) and use a theorem (eqb_eq) that we didn't
need in earlier proofs. So, let's add those into our tactic,
and clean it up a little in the process.
Ltac assn_auto' :=
unfold "->>", assn_sub, t_update, bassn;
intros; simpl in *;
try rewrite → eqb_eq in *; (* for equalities *)
auto; try lia.
Now the proof is quite streamlined.
Example if_example'' :
{{True}}
if X = 0
then Y := 2
else Y := X + 1
end
{{X ≤ Y}}.
Proof.
apply hoare_if.
- eapply hoare_consequence_pre.
+ apply hoare_asgn.
+ assn_auto'.
- eapply hoare_consequence_pre.
+ apply hoare_asgn.
+ assn_auto'.
Qed.
We can even shorten it a little bit more.
Example if_example''' :
{{True}}
if X = 0
then Y := 2
else Y := X + 1
end
{{X ≤ Y}}.
Proof.
apply hoare_if; eapply hoare_consequence_pre;
try apply hoare_asgn; try assn_auto'.
Qed.
For later proofs, it will help to extend assn_auto' to handle
inequalities, too.
Ltac assn_auto'' :=
unfold "->>", assn_sub, t_update, bassn;
intros; simpl in *;
try rewrite → eqb_eq in *;
try rewrite → leb_le in *; (* for inequalities *)
auto; try lia.
Exercise: 2 stars, standard (if_minus_plus)
Prove the theorem below using hoare_if. Do not use unfold hoare_triple.Theorem if_minus_plus :
{{True}}
if (X ≤ Y)
then Z := Y - X
else Y := X + Z
end
{{Y = X + Z}}.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: One-sided conditionals
Module If1.
Inductive com : Type :=
| CSkip : com
| CAss : string → aexp → com
| CSeq : com → com → com
| CIf : bexp → com → com → com
| CWhile : bexp → com → com
| CIf1 : bexp → com → com.
Notation "'if1' x 'then' y 'end'" :=
(CIf1 x y)
(in custom com at level 0, x custom com at level 99).
Notation "'skip'" :=
CSkip (in custom com at level 0).
Notation "x := y" :=
(CAss x y)
(in custom com at level 0, x constr at level 0,
y at level 85, no associativity).
Notation "x ; y" :=
(CSeq x y)
(in custom com at level 90, right associativity).
Notation "'if' x 'then' y 'else' z 'end'" :=
(CIf x y z)
(in custom com at level 89, x at level 99,
y at level 99, z at level 99).
Notation "'while' x 'do' y 'end'" :=
(CWhile x y)
(in custom com at level 89, x at level 99, y at level 99).
Exercise: 2 stars, standard (if1_ceval)
Reserved Notation "st '=[' c ']=>'' st'"
(at level 40, c custom com at level 99,
st constr, st' constr at next level).
Inductive ceval : com → state → state → Prop :=
| E_Skip : ∀ st,
st =[ skip ]=> st
| E_Ass : ∀ st a1 n x,
aeval st a1 = n →
st =[ x := a1 ]=> (x !-> n ; st)
| E_Seq : ∀ c1 c2 st st' st'',
st =[ c1 ]=> st' →
st' =[ c2 ]=> st'' →
st =[ c1 ; c2 ]=> st''
| E_IfTrue : ∀ st st' b c1 c2,
beval st b = true →
st =[ c1 ]=> st' →
st =[ if b then c1 else c2 end ]=> st'
| E_IfFalse : ∀ st st' b c1 c2,
beval st b = false →
st =[ c2 ]=> st' →
st =[ if b then c1 else c2 end ]=> st'
| E_WhileFalse : ∀ b st c,
beval st b = false →
st =[ while b do c end ]=> st
| E_WhileTrue : ∀ st st' st'' b c,
beval st b = true →
st =[ c ]=> st' →
st' =[ while b do c end ]=> st'' →
st =[ while b do c end ]=> st''
(* FILL IN HERE *)
where "st '=[' c ']=>' st'" := (ceval c st st').
Hint Constructors ceval : core.
The following unit tests should be provable simply by eauto if
you have defined the rules for if1 correctly.
Example if1true_test :
empty_st =[ if1 X = 0 then X := 1 end ]=> (X !-> 1).
Proof. (* FILL IN HERE *) Admitted.
Example if1false_test :
(X !-> 2) =[ if1 X = 0 then X := 1 end ]=> (X !-> 2).
Proof. (* FILL IN HERE *) Admitted.
☐
Definition hoare_triple
(P : Assertion) (c : com) (Q : Assertion) : Prop :=
∀ st st',
st =[ c ]=> st' →
P st →
Q st'.
Hint Unfold hoare_triple : core.
Notation "{{ P }} c {{ Q }}" := (hoare_triple P c Q)
(at level 90, c custom com at level 99)
: hoare_spec_scope.
Exercise: 2 stars, standard (hoare_if1)
(* FILL IN HERE *)
For full credit, prove formally hoare_if1_good that your rule is
precise enough to show the following valid Hoare triple:
{{ X + Y = Z }}
if1 ~(Y = 0) then
X := X + Y
end
{{ X = Z }}
{{ X + Y = Z }}
if1 ~(Y = 0) then
X := X + Y
end
{{ X = Z }}
(* Do not modify the following line: *)
Definition manual_grade_for_hoare_if1 : option (nat×string) := None.
☐
Definition manual_grade_for_hoare_if1 : option (nat×string) := None.
☐
Theorem hoare_consequence_pre : ∀ (P P' Q : Assertion) c,
{{P'}} c {{Q}} →
P ->> P' →
{{P}} c {{Q}}.
Proof.
eauto.
Qed.
Theorem hoare_asgn : ∀ Q X a,
{{Q [X ⊢> a]}} (X := a) {{Q}}.
Proof.
intros Q X a st st' Heval HQ.
inversion Heval; subst.
auto.
Qed.
Exercise: 2 stars, standard (hoare_if1_good)
Lemma hoare_if1_good :
{{ X + Y = Z }}
if1 ¬(Y = 0) then
X := X + Y
end
{{ X = Z }}.
Proof. (* FILL IN HERE *) Admitted.
☐
While Loops
{{P}} c {{P}}
{{P}} c {{P}}
---------------------------
{{P} while b do c end {{P}}
{{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}}
- If the loop body executes zero times, the rule is like skip in
that the precondition survives to become (part of) the
postcondition.
- Like a conditional, we can assume guard b holds on entry to the subcommand.
Theorem hoare_while : ∀ P (b:bexp) c,
{{P ∧ b}} c {{P}} →
{{P}} while b do c end {{P ∧ ¬ b}}.
Proof.
intros P b c Hhoare st st' Heval HP.
(* We proceed by induction on Heval, because, in the "keep looping" case,
its hypotheses talk about the whole loop instead of just c. The
remember is used to keep the original command in the hypotheses;
otherwise, it would be lost in the induction. By using inversion
we clear away all the cases except those involving while. *)
remember <{while b do c end}> as original_command eqn:Horig.
induction Heval;
try (inversion Horig; subst; clear Horig);
eauto.
Qed.
intros P b c Hhoare st st' Heval HP.
(* We proceed by induction on Heval, because, in the "keep looping" case,
its hypotheses talk about the whole loop instead of just c. The
remember is used to keep the original command in the hypotheses;
otherwise, it would be lost in the induction. By using inversion
we clear away all the cases except those involving while. *)
remember <{while b do c end}> as original_command eqn:Horig.
induction Heval;
try (inversion Horig; subst; clear Horig);
eauto.
Qed.
We say that P is a loop invariant of while b do c end if P
suffices to prove hoare_while for that loop. Being a loop
invariant is different from being an invariant of the body,
because it means being able to prove correctness of the loop. For
example, X = 0 is a loop invariant of
while X = 2 do X := 1 end
even though X = 0 is not an invariant of X := 1.
This is a slightly (but crucially) 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.
while X = 2 do X := 1 end
while X = 2 do X := 1 end
Example while_example :
{{X ≤ 3}}
while (X ≤ 2) do
X := X + 1
end
{{X = 3}}.
Proof.
eapply hoare_consequence_post.
- apply hoare_while.
eapply hoare_consequence_pre.
+ apply hoare_asgn.
+ assn_auto''.
- assn_auto''.
Qed.
eapply hoare_consequence_post.
- apply hoare_while.
eapply hoare_consequence_pre.
+ apply hoare_asgn.
+ assn_auto''.
- assn_auto''.
Qed.
If the loop never terminates, any postcondition will work.
Theorem always_loop_hoare : ∀ Q,
{{True}} while true do skip end {{Q}}.
Proof.
intros Q.
eapply hoare_consequence_post.
- apply hoare_while. apply hoare_post_true. auto.
- simpl. intros st [Hinv Hguard]. congruence.
Qed.
intros Q.
eapply hoare_consequence_post.
- apply hoare_while. apply hoare_post_true. auto.
- simpl. intros st [Hinv Hguard]. congruence.
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 specify what happens if commands terminate,
without proving that they do, are said to describe a logic of
partial correctness. It is also possible to give Hoare rules
for total correctness, which additionally specifies that
commands must terminate. Total correctness is out of the scope of
this textbook.
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 b 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
| CAss : string → 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 "'repeat' e1 'until' b2 'end'" :=
(CRepeat e1 b2)
(in custom com at level 0,
e1 custom com at level 99, b2 custom com at level 99).
Notation "'skip'" :=
CSkip (in custom com at level 0).
Notation "x := y" :=
(CAss x y)
(in custom com at level 0, x constr at level 0,
y at level 85, no associativity).
Notation "x ; y" :=
(CSeq x y)
(in custom com at level 90, right associativity).
Notation "'if' x 'then' y 'else' z 'end'" :=
(CIf x y z)
(in custom com at level 89, x at level 99,
y at level 99, z at level 99).
Notation "'while' x 'do' y 'end'" :=
(CWhile x y)
(in custom com at level 89, x at level 99, y at level 99).
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,
st =[ skip ]=> st
| E_Ass : ∀ st a1 n x,
aeval st a1 = n →
st =[ x := a1 ]=> (x !-> n ; st)
| E_Seq : ∀ c1 c2 st st' st'',
st =[ c1 ]=> st' →
st' =[ c2 ]=> st'' →
st =[ c1 ; c2 ]=> st''
| E_IfTrue : ∀ st st' b c1 c2,
beval st b = true →
st =[ c1 ]=> st' →
st =[ if b then c1 else c2 end ]=> st'
| E_IfFalse : ∀ st st' b c1 c2,
beval st b = false →
st =[ c2 ]=> st' →
st =[ if b then c1 else c2 end ]=> st'
| E_WhileFalse : ∀ b st c,
beval st b = false →
st =[ while b do c end ]=> st
| E_WhileTrue : ∀ st st' st'' b c,
beval st b = true →
st =[ c ]=> st' →
st' =[ while b do c end ]=> st'' →
st =[ while b do c end ]=> st''
(* FILL IN HERE *)
where "st '=[' c ']=>' st'" := (ceval st c st').
A couple of definitions from above, copied here so they use the
new ceval.
Definition hoare_triple (P : Assertion) (c : com) (Q : Assertion)
: Prop :=
∀ st st', st =[ c ]=> st' → P st → Q st'.
Notation "{{ P }} c {{ Q }}" :=
(hoare_triple P c Q) (at level 90, c custom com at level 99).
To make sure you've got the evaluation rules for repeat right,
prove that ex1_repeat evaluates correctly.
Definition ex1_repeat :=
<{ repeat
X := 1;
Y := Y + 1
until (X = 1) end }>.
Theorem ex1_repeat_works :
empty_st =[ ex1_repeat ]=> (Y !-> 1 ; X !-> 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 }}
{{ X > 0 }}
repeat
Y := X;
X := X - 1
until X = 0 end
{{ X = 0 ∧ Y > 0 }}
End RepeatExercise.
(* Do not modify the following line: *)
Definition manual_grade_for_hoare_repeat : option (nat×string) := None.
☐
Summary
(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}} if b then c1 else c2 end {{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
Havoc
Module Himp.
Inductive com : Type :=
| CSkip : com
| CAss : string → aexp → com
| CSeq : com → com → com
| CIf : bexp → com → com → com
| CWhile : bexp → com → com
| CHavoc : string → com.
Notation "'havoc' l" := (CHavoc l)
(in custom com at level 60, l constr at level 0).
Notation "'skip'" :=
CSkip (in custom com at level 0).
Notation "x := y" :=
(CAss x y)
(in custom com at level 0, x constr at level 0,
y at level 85, no associativity).
Notation "x ; y" :=
(CSeq x y)
(in custom com at level 90, right associativity).
Notation "'if' x 'then' y 'else' z 'end'" :=
(CIf x y z)
(in custom com at level 89, x at level 99,
y at level 99, z at level 99).
Notation "'while' x 'do' y 'end'" :=
(CWhile x y)
(in custom com at level 89, x at level 99, y at level 99).
Inductive ceval : com → state → state → Prop :=
| E_Skip : ∀ st,
st =[ skip ]=> st
| E_Ass : ∀ st a1 n x,
aeval st a1 = n →
st =[ x := a1 ]=> (x !-> n ; st)
| E_Seq : ∀ c1 c2 st st' st'',
st =[ c1 ]=> st' →
st' =[ c2 ]=> st'' →
st =[ c1 ; c2 ]=> st''
| E_IfTrue : ∀ st st' b c1 c2,
beval st b = true →
st =[ c1 ]=> st' →
st =[ if b then c1 else c2 end ]=> st'
| E_IfFalse : ∀ st st' b c1 c2,
beval st b = false →
st =[ c2 ]=> st' →
st =[ if b then c1 else c2 end ]=> st'
| E_WhileFalse : ∀ b st c,
beval st b = false →
st =[ while b do c end ]=> st
| E_WhileTrue : ∀ st st' st'' b c,
beval st b = true →
st =[ c ]=> st' →
st' =[ while b do c end ]=> st'' →
st =[ while b do c end ]=> st''
| E_Havoc : ∀ st X n,
st =[ havoc X ]=> (X !-> n ; st)
where "st '=[' c ']=>' st'" := (ceval c st st').
Hint Constructors ceval : core.
The definition of Hoare triples is exactly as before.
Definition hoare_triple (P:Assertion) (c:com) (Q:Assertion) : Prop :=
∀ st st', st =[ c ]=> st' → P st → Q st'.
Hint Unfold hoare_triple : core.
Notation "{{ P }} c {{ Q }}" := (hoare_triple P c Q)
(at level 90, c custom com at level 99)
: hoare_spec_scope.
And the precondition consequence rule is exactly as before.
Theorem hoare_consequence_pre : ∀ (P P' Q : Assertion) c,
{{P'}} c {{Q}} →
P ->> P' →
{{P}} c {{Q}}.
Proof. eauto. Qed.
Exercise: 3 stars, standard (hoare_havoc)
Definition havoc_pre (X : string) (Q : Assertion) (st : total_map nat) : Prop
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Theorem hoare_havoc : ∀ (Q : Assertion) (X : string),
{{ havoc_pre X Q }} havoc X {{ Q }}.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, standard (havoc_post)
Theorem havoc_post : ∀ (P : Assertion) (X : string),
{{ P }} havoc X {{ fun st ⇒ ∃ (n:nat), P [X ⊢> n] st }}.
Proof.
intros P X. eapply hoare_consequence_pre.
- apply hoare_havoc.
- (* FILL IN HERE *) Admitted.
☐
In this exercise, we will extend IMP with two commands,
assert and ASSUME. Both commands are ways
to indicate that a certain statement should hold any time this part
of the program is reached. However they differ as follows:
The new set of commands is:
- If an assert statement fails, it causes the program to go into
an error state and exit.
- If an ASSUME statement fails, the program fails to evaluate at all. In other words, the program gets stuck and has no final state.
Inductive com : Type :=
| CSkip : com
| CAss : string → aexp → com
| CSeq : com → com → com
| CIf : bexp → com → com → com
| CWhile : bexp → com → com
| CAssert : bexp → com
| CAssume : bexp → com.
Notation "'assert' l" := (CAssert l)
(in custom com at level 8, l custom com at level 0).
Notation "'assume' l" := (CAssume l)
(in custom com at level 8, l custom com at level 0).
Notation "'skip'" :=
CSkip (in custom com at level 0).
Notation "x := y" :=
(CAss x y)
(in custom com at level 0, x constr at level 0,
y at level 85, no associativity).
Notation "x ; y" :=
(CSeq x y)
(in custom com at level 90, right associativity).
Notation "'if' x 'then' y 'else' z 'end'" :=
(CIf x y z)
(in custom com at level 89, x at level 99,
y at level 99, z at level 99).
Notation "'while' x 'do' y 'end'" :=
(CWhile x y)
(in custom com at level 89, x at level 99, y at level 99).
To define the behavior of assert and ASSUME, we need to add
notation for an error, which indicates that an assertion has
failed. We modify the ceval relation, therefore, so that
it relates a start state to either an end state or to error.
The result type indicates the end value of a program,
either a state or an error:
Now we are ready to give you the ceval relation for the new language.
Inductive ceval : com → state → result → Prop :=
(* Old rules, several modified *)
| E_Skip : ∀ st,
st =[ skip ]=> RNormal st
| E_Ass : ∀ st a1 n x,
aeval st a1 = n →
st =[ x := a1 ]=> RNormal (x !-> n ; st)
| E_SeqNormal : ∀ c1 c2 st st' r,
st =[ c1 ]=> RNormal st' →
st' =[ c2 ]=> r →
st =[ c1 ; c2 ]=> r
| E_SeqError : ∀ c1 c2 st,
st =[ c1 ]=> RError →
st =[ c1 ; c2 ]=> RError
| E_IfTrue : ∀ st r b c1 c2,
beval st b = true →
st =[ c1 ]=> r →
st =[ if b then c1 else c2 end ]=> r
| E_IfFalse : ∀ st r b c1 c2,
beval st b = false →
st =[ c2 ]=> r →
st =[ if b then c1 else c2 end ]=> r
| E_WhileFalse : ∀ b st c,
beval st b = false →
st =[ while b do c end ]=> RNormal st
| E_WhileTrueNormal : ∀ st st' r b c,
beval st b = true →
st =[ c ]=> RNormal st' →
st' =[ while b do c end ]=> r →
st =[ while b do c end ]=> r
| E_WhileTrueError : ∀ st b c,
beval st b = true →
st =[ c ]=> RError →
st =[ while b do c end ]=> RError
(* Rules for Assert and Assume *)
| E_AssertTrue : ∀ st b,
beval st b = true →
st =[ assert b ]=> RNormal st
| E_AssertFalse : ∀ st b,
beval st b = false →
st =[ assert b ]=> RError
| E_Assume : ∀ st b,
beval st b = true →
st =[ assume b ]=> RNormal st
where "st '=[' c ']=>' r" := (ceval c st r).
We redefine hoare triples: Now, {{P}} c {{Q}} means that,
whenever c is started in a state satisfying P, and terminates
with result r, then r is not an error and the state of r
satisfies Q.
Definition hoare_triple
(P : Assertion) (c : com) (Q : Assertion) : Prop :=
∀ st r,
st =[ c ]=> r → P st →
(∃ st', r = RNormal st' ∧ Q st').
Notation "{{ P }} c {{ Q }}" :=
(hoare_triple P c Q) (at level 90, c custom com at level 99)
: hoare_spec_scope.
To test your understanding of this modification, give an example
precondition and postcondition that are satisfied by the ASSUME
statement but not by the assert statement. Then prove that any
triple for assert also works for ASSUME.
Theorem assert_assume_differ : ∃ (P:Assertion) b (Q:Assertion),
({{P}} assume b {{Q}})
∧ ¬ ({{P}} assert b {{Q}}).
(* FILL IN HERE *) Admitted.
Theorem assert_implies_assume : ∀ P b Q,
({{P}} assert b {{Q}})
→ ({{P}} assume b {{Q}}).
Proof.
(* FILL IN HERE *) Admitted.
Your task is now to state Hoare rules for assert and assume,
and use them to prove a simple program correct. Name your hoare
rule theorems hoare_assert and hoare_assume.
For your benefit, we provide proofs for the old hoare rules
adapted to the new semantics.
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.
∃ (X !-> aeval st a ; st). split; try reflexivity.
assumption. Qed.
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 r Hc HP.
unfold hoare_triple in Hhoare.
assert (∃ st', r = RNormal st' ∧ Q' st').
{ apply (Hhoare st); assumption. }
destruct H as [st' [Hr HQ'] ].
∃ st'. split; try assumption.
apply Himp. assumption.
Qed.
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 r H12 Pre.
inversion H12; subst.
- eapply H1.
+ apply H6.
+ apply H2 in H3. apply H3 in Pre.
destruct Pre as [st'0 [Heq HQ] ].
inversion Heq; subst. assumption.
- (* Find contradictory assumption *)
apply H2 in H5. apply H5 in Pre.
destruct Pre as [st' [C _] ].
inversion C.
Qed.
State and prove your hoare rules, hoare_assert and
hoare_assume, below.
(* FILL IN HERE *)
Here are the other proof rules (sanity check)
(* NOTATION : IY -- Do we want <{ }> to be printing in here? *)
Theorem hoare_skip : ∀ P,
{{P}} skip {{P}}.
Proof.
intros P st st' H HP. inversion H. subst.
eexists. split. reflexivity. assumption.
Qed.
Theorem hoare_if : ∀ P Q (b:bexp) c1 c2,
{{ P ∧ b}} c1 {{Q}} →
{{ P ∧ ¬ b}} c2 {{Q}} →
{{P}} if b then c1 else c2 end {{Q}}.
Proof.
intros P Q b c1 c2 HTrue HFalse st st' HE HP.
inversion HE; subst.
- (* b is true *)
apply (HTrue st st').
assumption.
split. assumption. assumption.
- (* b is false *)
apply (HFalse st st').
assumption.
split. assumption.
apply bexp_eval_false. assumption. Qed.
Theorem hoare_while : ∀ P (b:bexp) c,
{{P ∧ b}} c {{P}} →
{{P}} while b do c end {{ P ∧ ¬b}}.
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.
- (* E_WhileFalse *)
eexists. split. reflexivity. split.
assumption. apply bexp_eval_false. assumption.
- (* E_WhileTrueNormal *)
clear IHHe1.
apply IHHe2. reflexivity.
clear IHHe2 He2 r.
unfold hoare_triple in Hhoare.
apply Hhoare in He1.
+ destruct He1 as [st1 [Heq Hst1] ].
inversion Heq; subst.
assumption.
+ split; assumption.
- (* E_WhileTrueError *)
exfalso. clear IHHe.
unfold hoare_triple in Hhoare.
apply Hhoare in He.
+ destruct He as [st' [C _] ]. inversion C.
+ split; assumption.
Qed.
Example assert_assume_example:
{{True}}
assume (X = 1);
X := X + 1;
assert (X = 2)
{{True}}.
Proof.
(* FILL IN HERE *) Admitted.
End HoareAssertAssume.
☐
Theorem hoare_skip : ∀ P,
{{P}} skip {{P}}.
Proof.
intros P st st' H HP. inversion H. subst.
eexists. split. reflexivity. assumption.
Qed.
Theorem hoare_if : ∀ P Q (b:bexp) c1 c2,
{{ P ∧ b}} c1 {{Q}} →
{{ P ∧ ¬ b}} c2 {{Q}} →
{{P}} if b then c1 else c2 end {{Q}}.
Proof.
intros P Q b c1 c2 HTrue HFalse st st' HE HP.
inversion HE; subst.
- (* b is true *)
apply (HTrue st st').
assumption.
split. assumption. assumption.
- (* b is false *)
apply (HFalse st st').
assumption.
split. assumption.
apply bexp_eval_false. assumption. Qed.
Theorem hoare_while : ∀ P (b:bexp) c,
{{P ∧ b}} c {{P}} →
{{P}} while b do c end {{ P ∧ ¬b}}.
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.
- (* E_WhileFalse *)
eexists. split. reflexivity. split.
assumption. apply bexp_eval_false. assumption.
- (* E_WhileTrueNormal *)
clear IHHe1.
apply IHHe2. reflexivity.
clear IHHe2 He2 r.
unfold hoare_triple in Hhoare.
apply Hhoare in He1.
+ destruct He1 as [st1 [Heq Hst1] ].
inversion Heq; subst.
assumption.
+ split; assumption.
- (* E_WhileTrueError *)
exfalso. clear IHHe.
unfold hoare_triple in Hhoare.
apply Hhoare in He.
+ destruct He as [st' [C _] ]. inversion C.
+ split; assumption.
Qed.
Example assert_assume_example:
{{True}}
assume (X = 1);
X := X + 1;
assert (X = 2)
{{True}}.
Proof.
(* FILL IN HERE *) Admitted.
End HoareAssertAssume.
☐
(* 2021-03-18 17:24 *)