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.
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 in this chapter 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 structured proof
technique for proving that programs are correct with respect to
such specifications -- where by "structured" 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 for states st in which value of X
is 3,
- fun st ⇒ True hold for all states, and
- fun st ⇒ False holds for no states.
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.
☐
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 we'll write just
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.
∀ 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.
Add Printing Coercion Aexp_of_nat Aexp_of_aexp assert_of_Prop.
Arguments assert_of_Prop /.
Arguments Aexp_of_nat /.
Arguments Aexp_of_aexp /.
Add Printing Coercion Aexp_of_nat Aexp_of_aexp assert_of_Prop.
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.
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.
Add Printing Coercion Aexp_of_nat Aexp_of_aexp assert_of_Prop.
Arguments assert_of_Prop /.
Arguments Aexp_of_nat /.
Arguments Aexp_of_aexp /.
Add Printing Coercion Aexp_of_nat Aexp_of_aexp assert_of_Prop.
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 ExamplePrettyAssertions.
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 = ap2 max X Y.
Definition assn4 : Assertion := Z × Z ≤ X
∧ ¬ (((ap S Z) × (ap S Z)) ≤ X).
End ExamplePrettyAssertions.
fun st ⇒ f (x st).
Definition ap2 {X} (f : nat → nat → X) (x : Aexp) (y : Aexp) (st : state) :=
f (x st) (y st).
Module ExamplePrettyAssertions.
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 = ap2 max X Y.
Definition assn4 : Assertion := Z × Z ≤ X
∧ ¬ (((ap S Z) × (ap S Z)) ≤ X).
End ExamplePrettyAssertions.
Hoare Triples, Informally
{P} c {Q} meaning:
- 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}} For example,
- {{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 + 1}} 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.
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}}).
(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.
☐
(∀ 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.
☐
(∀ st, ¬ (P st)) →
{{P}} c {{Q}}.
Proof.
(* FILL IN HERE *) Admitted.
☐
Proof Rules
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 }} 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}}.
{{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.
Assignment
{{ ??? }} X := Y {{ X = 1 }}
{{ Y = 1 }} X := Y {{ X = 1 }} It may seem as though coming up with that precondition must have taken some clever thought. But there is a mechanical way we could have done it: if we take the postcondition X = 1 and in it replace X with Y---that is, replace the left-hand side of the assignment statement with the right-hand side---we get the precondition, Y = 1.
{{ ??? }} X := X + Y {{ X = 1 }} If we replace the X in X = 1 with X + Y, we get X + Y = 1. That again leads to a valid Hoare triple:
{{ X + Y = 1 }} X := X + Y {{ X = 1 }} Why does this technique work? The postcondition identifies some property P that we want to hold of the variable X being assigned. In this case, P is "equals 1". To complete the triple and make it valid, we need to identify a precondition that guarantees that property will hold of X. Such a precondition must ensure that the same property holds of whatever is being assigned to X. So, in the example, we need "equals 1" to hold of X + Y. That's exactly what the technique guarantees.
{{ ??? }} X := a {{ Q }} The precondition would then be Q, but with any occurrences of X in it replaced by a. Let's introduce a notation for this idea of replacing occurrences: Define Q [X ⊢> a] to mean "Q where a is substituted in place of X".
{{ Q [X ⊢> a] }} X := a {{ Q }} One way of reading this rule is: If you want statement X := a to terminate in a state that satisfies assertion Q, then it suffices to start in a state that also satisfies Q, except where a is substituted for every occurrence of X.
{{ (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).
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 substitution operation we've just defined, 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), 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).
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.
(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 :
{{(X < 5) [X ⊢> X + 1]}}
X := X + 1
{{X < 5}}.
Proof.
apply hoare_asgn. Qed.
{{(X < 5) [X ⊢> X + 1]}}
X := X + 1
{{X < 5}}.
Proof.
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.
Complete these Hoare triples by providing an appropriate
precondition using ∃, then prove then with 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}} We will see how to do so in the next section.
Exercise: 2 stars, standard, optional (hoare_asgn_examples1)
Example hoare_asgn_examples1 :
∃ P,
{{ P }}
X := 2 × X
{{ X ≤ 10 }}.
Proof.
(* FILL IN HERE *) Admitted.
☐
∃ P,
{{ P }}
X := 2 × X
{{ X ≤ 10 }}.
Proof.
(* FILL IN HERE *) Admitted.
☐
Example hoare_asgn_examples2 :
∃ P,
{{ P }}
X := 3
{{ 0 ≤ X ∧ X ≤ 5 }}.
Proof. (* FILL IN HERE *) Admitted.
☐
∃ P,
{{ P }}
X := 3
{{ 0 ≤ X ∧ X ≤ 5 }}.
Proof. (* FILL IN HERE *) Admitted.
☐
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.
☐
(* 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 (X !-> m ; st) /\ st X = aeval (X !-> m ; st) a }} |
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.
☐
∀ 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.
☐
∀ 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}}, follows directly from the assignment rule, but
{{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.
{{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.
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 }} Or, formally...
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.
{{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 }} Or, formally ...
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.
{{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}} |
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 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.
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.
{{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.
{{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.
{{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.
The eauto tactic will use eapply as part of its proof search.
So, the entire proof can actually 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.
{{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 worked there, 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.
{{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.
{{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.
{{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 lia.
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.
{{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.
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 proofs 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.
☐
{{ 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.
☐
Sequencing + Assignment
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.
{{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 }} We'll come back to the idea of decorated programs in much more detail in the next chapter.
{{ 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 }} We'll come back to the idea of decorated programs in much more detail in the next chapter.
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 }} Note the use of "->>" decorations, each marking a use of hoare_consequence_pre.
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.
☐
{{ 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}} Your proof should not need to use unfold hoare_triple. (Hint: Remember that the assignment rule works best when it's applied "back to front," from the postcondition to the precondition. So your proof will want to start at the end and work back to the beginning of your program.)
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.
☐
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Theorem swap_exercise :
{{X ≤ Y}}
swap_program
{{Y ≤ X}}.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 4 stars, advanced (invalid_triple)
Show that{{ a = n }} X := 3; Y := a {{ Y = n }} is not a valid Hoare triple for some choices of a and n.
specialize H with (a := your_a) (n := your_n) the hypothesis will be instantiated on your_a and your_n.
- Use the (assumed) validity of the given hoare triple to derive a state st' in which Y has some value y1
- Use the evaluation rules (E_Seq and E_Asgn) to show that Y has a different value y2 in the same final state st'
- since y1 and y2 are both equal to st' Y, they are equal to each other; but we chose them to be different, so this is a contradiction, which finishes the proof.
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.
☐
{{ 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 }} since the rule tells us nothing about the state in which the assignments take place in the "then" and "else" branches.
{{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 /.
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).
Hint Resolve bexp_eval_false : core.
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}}.
{{ 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.
{{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.
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.
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.
{{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.
{{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.
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.
☐
{{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
| CAsgn : 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" :=
(CAsgn 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 com : Type :=
| CSkip : com
| CAsgn : 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" :=
(CAsgn 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, especially useful (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_Asgn : ∀ 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.
(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_Asgn : ∀ 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.
☐
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.
(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.
{{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.
☐
{{ X + Y = Z }}
if1 Y ≠ 0 then
X := X + Y
end
{{ X = Z }}.
Proof. (* FILL IN HERE *) Admitted.
☐
While Loops
{{P}} c {{P}} holds. Note that in the middle of executing c, the invariant might temporarily become false, but by the end of c, it must be restored.
{{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}}.
{{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 call P a loop invariant of while b do c end if
{{P ∧ b}} c {{P}} is a valid Hoare triple. This means that P will be true at the end of the loop body whenever the loop body executes. If P contradicts b, this holds trivially since the precondition is false. For instance, X = 0 is a loop invariant of
while X = 2 do X := 1 end since we will never enter the loop.
The program
while Y > 10 do Y := Y - 1; Z := Z + 1 end admits an interesting loop invariant:
X = Y + Z Note that this doesn't contradict the loop guard but neither is it an invariant of
Y := Y - 1; Z := Z + 1 since, if X = 5, Y = 0 and Z = 5, running the command will set Y + Z to 6. The loop guard Y > 10 guarantees that this will not be the case. We will see many such loop invariants in the following chapter.
{{P ∧ b}} c {{P}} is a valid Hoare triple. This means that P will be true at the end of the loop body whenever the loop body executes. If P contradicts b, this holds trivially since the precondition is false. For instance, X = 0 is a loop invariant of
while X = 2 do X := 1 end since we will never enter the loop.
while Y > 10 do Y := Y - 1; Z := Z + 1 end admits an interesting loop invariant:
X = Y + Z Note that this doesn't contradict the loop guard but neither is it an invariant of
Y := Y - 1; Z := Z + 1 since, if X = 5, Y = 0 and Z = 5, running the command will set Y + Z to 6. The loop guard Y > 10 guarantees that this will not be the case. We will see many such loop invariants in the following chapter.
Example while_example :
{{X ≤ 3}}
while (X ≤ 2) do
X := X + 1
end
{{X = 3}}.
{{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}}.
{{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, optional (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
| CAsgn : string → 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 : 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" :=
(CAsgn 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).
(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" :=
(CAsgn 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_Asgn : ∀ 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').
| E_Skip : ∀ st,
st =[ skip ]=> st
| E_Asgn : ∀ 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).
: 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.
<{ 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.
☐
(* 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
| CAsgn : 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" :=
(CAsgn 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_Asgn : ∀ 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.
Inductive com : Type :=
| CSkip : com
| CAsgn : 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" :=
(CAsgn 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_Asgn : ∀ 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.
∀ 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.
{{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.
☐
(* 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.
☐
{{ 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.
☐
Assert and Assume
Exercise: 4 stars, standard (assert_vs_assume)
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:- 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.
Module HoareAssertAssume.
Inductive com : Type :=
| CSkip : com
| CAsgn : 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" :=
(CAsgn 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 com : Type :=
| CSkip : com
| CAsgn : 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" :=
(CAsgn 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_Asgn : ∀ 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).
(* Old rules, several modified *)
| E_Skip : ∀ st,
st =[ skip ]=> RNormal st
| E_Asgn : ∀ 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.
(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.
Theorem assert_assume_differ : ∃ (P:Assertion) b (Q:Assertion),
({{P}} assume b {{Q}})
∧ ¬ ({{P}} assert b {{Q}}).
(* FILL IN HERE *) Admitted.
({{P}} assume b {{Q}})
∧ ¬ ({{P}} assert b {{Q}}).
(* FILL IN HERE *) Admitted.
Then prove that any triple for an assert also works when
assert is replaced by assume.
Theorem assert_implies_assume : ∀ P b Q,
({{P}} assert b {{Q}})
→ ({{P}} assume b {{Q}}).
Proof.
(* FILL IN HERE *) Admitted.
({{P}} assert b {{Q}})
→ ({{P}} assume b {{Q}}).
Proof.
(* FILL IN HERE *) Admitted.
Next, here are proofs for the old hoare rules adapted to the new
semantics. You don't need to do anything with these.
Theorem hoare_asgn : ∀ Q X a,
{{Q [X ⊢> a]}} X := a {{Q}}.
Theorem hoare_consequence_pre : ∀ (P P' Q : Assertion) c,
Theorem hoare_consequence_post : ∀ (P Q Q' : Assertion) c,
{{P}} c {{Q'}} →
Q' ->> Q →
{{P}} c {{Q}}.
Theorem hoare_seq : ∀ P Q R c1 c2,
{{Q}} c2 {{R}} →
{{P}} c1 {{Q}} →
{{P}} c1;c2 {{R}}.
{{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.
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.
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.
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.
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.
Here are the other proof rules (sanity check)
Theorem hoare_skip : ∀ P,
{{P}} skip {{P}}.
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}}.
Theorem hoare_while : ∀ P (b:bexp) c,
{{P ∧ b}} c {{P}} →
{{P}} while b do c end {{ P ∧ ¬b}}.
{{P}} skip {{P}}.
Proof.
intros P st st' H HP. inversion H. subst.
eexists. split. reflexivity. assumption.
Qed.
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.
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.
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.
Finally, state Hoare rules for assert and assume and use them
to prove a simple program correct. Name your rules hoare_assert
and hoare_assume.
(* FILL IN HERE *)
Use your rules to prove the following triple.
Example assert_assume_example:
{{True}}
assume (X = 1);
X := X + 1;
assert (X = 2)
{{True}}.
Proof.
(* FILL IN HERE *) Admitted.
End HoareAssertAssume.
☐
{{True}}
assume (X = 1);
X := X + 1;
assert (X = 2)
{{True}}.
Proof.
(* FILL IN HERE *) Admitted.
End HoareAssertAssume.
☐
(* 2022-09-20 16:43 *)