HoareHoare Logic, Part I
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.
Assertions
Definition Assertion := state → Prop.
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.
Paraphrase the following assertions in English
(1) fun st ⇒ st X ≤ st Y
(2) fun st ⇒ st X = 3 ∨ st X ≤ st Y
(3) fun st ⇒ st Z × st Z ≤ st X ∧
¬ (((S (st Z)) × (S (st Z))) ≤ st X)
Informally, instead of writing
fun st ⇒ st X = m
X = m
Definition assert_implies (P Q : Assertion) : Prop :=
∀ st, P st → Q st.
Notation "P ->> Q" := (assert_implies P Q)
(at level 80) : hoare_spec_scope.
Open Scope hoare_spec_scope.
We'll also want the "iff" variant of implication between
assertions:
Notation "P <<->> Q" :=
(P ->> Q ∧ Q ->> P) (at level 80) : hoare_spec_scope.
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 /.
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.
Lift functions to operate on assertion expressions.
Definition ap {X} (f : nat → X) (x : Aexp) :=
fun st ⇒ f (x st).
Definition ap_{2} {X} (f : nat → nat → X) (x : Aexp) (y : Aexp) (st : state) :=
f (x st) (y st).
Module ExPrettyAssertions.
Definition ex_{1} : Assertion := X = 3.
Definition ex_{2} : Assertion := True.
Definition ex_{3} : 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 = ap_{2} 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.
- {{X = m}} X ::= X + 1 {{X = m + 1}}, is also a valid Hoare triple. It's even more descriptive of the exact behavior of that command than the previous example.
Paraphrase the following Hoare triples in English.
1) {{True}} c {{X = 5}}
2) {{X = m}} c {{X = m + 5)}}
3) {{X ≤ Y}} c {{Y ≤ X}}
4) {{True}} c {{False}}
5) {{X = m}}
c
{{Y = real_fact m}}
6) {{X = m}}
c
{{(Z × Z) ≤ m ∧ ¬(((S Z) × (S Z)) ≤ m)}}
1) {{True}} c {{X = 5}}
2) {{X = m}} c {{X = m + 5)}}
3) {{X ≤ Y}} c {{Y ≤ X}}
4) {{True}} c {{False}}
5) {{X = m}}
c
{{Y = real_fact m}}
6) {{X = m}}
c
{{(Z × Z) ≤ m ∧ ¬(((S Z) × (S Z)) ≤ m)}}
Is the following Hoare triple valid -- i.e., is the
claimed relation between P, c, and Q true?
{{True}} X ::= 5 {{X = 5}}
(1) Yes
(2) No
{{True}} X ::= 5 {{X = 5}}
What about this one?
{{X = 2}} X ::= X + 1 {{X = 3}}
(1) Yes
(2) No
{{X = 2}} X ::= X + 1 {{X = 3}}
What about this one?
{{True}} X ::= 5;; Y ::= 0 {{X = 5}}
(1) Yes
(2) No
{{True}} X ::= 5;; Y ::= 0 {{X = 5}}
What about this one?
{{X = 2 ∧ X = 3}} X ::= 5 {{X = 0}}
(1) Yes
(2) No
{{X = 2 ∧ X = 3}} X ::= 5 {{X = 0}}
What about this one?
{{True}} SKIP {{False}}
(1) Yes
(2) No
{{True}} SKIP {{False}}
What about this one?
{{False}} SKIP {{True}}
(1) Yes
(2) No
{{False}} SKIP {{True}}
What about this one?
{{True}} WHILE true DO SKIP END {{False}}
(1) Yes
(2) No
{{True}} WHILE true DO SKIP END {{False}}
This one?
{{X = 0}}
WHILE X = 0 DO X ::= X + 1 END
{{X = 1}}
(1) Yes
(2) No
{{X = 0}}
WHILE X = 0 DO X ::= X + 1 END
{{X = 1}}
This one?
{{X = 1}}
WHILE ~(X = 0) DO X ::= X + 1 END
{{X = 100}}
(1) Yes
(2) No
{{X = 1}}
WHILE ~(X = 0) DO X ::= X + 1 END
{{X = 100}}
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 at next level)
: hoare_spec_scope.
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
- introduce one "proof rule" for each Imp syntactic form
- plus a couple of "structural rules" that help glue proofs together
- prove programs correct using these proof rules, without ever unfolding the definition of hoare_triple
Assignment
{{ ??? }} X ::= Y {{ X = 1 }}
{{ Y = 1 }} X ::= Y {{ X = 1 }}
Another example:
{{ ??? }} 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 }}
Since P is an arbitrary Coq assertion, we can't directly "edit" its text. However, we can achieve the same effect by evaluating P in an updated state:
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).
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.
Example assn_sub_example :
{{(X < 5) [X ⊢> X + 1]}}
X ::= X + 1
{{X < 5}}.
Proof.
(* WORK IN CLASS *) Admitted.
Of course, what would be even more helpful is to prove this simpler triple:
{{X < 4}} X ::= X + 1 {{X < 5}}
Here is the assignment rule again:
{{ Q [X ⊢> a] }} X ::= a {{ Q }}
Is the following triple a valid instance of this rule?
{{ X = 5 }} X ::= X + 1 {{ X = 6 }}
(1) Yes
(2) No
{{ Q [X ⊢> a] }} X ::= a {{ Q }}
{{ X = 5 }} X ::= X + 1 {{ X = 6 }}
Here is the assignment rule again:
{{ Q [X ⊢> a] }} X ::= a {{ Q }}
Is the following triple a valid instance of this rule?
{{ Y < Z }} X ::= Y {{ X < Z }}
(1) Yes
(2) No
{{ Q [X ⊢> a] }} X ::= a {{ Q }}
{{ Y < Z }} X ::= Y {{ X < Z }}
The assignment rule again:
{{ Q [X ⊢> a] }} X ::= a {{ Q }}
Is the following triple a valid instance of this rule?
{{ X+1 < Y }} X ::= X + 1 {{ X < Y }}
(1) Yes
(2) No
{{ Q [X ⊢> a] }} X ::= a {{ Q }}
{{ X+1 < Y }} X ::= X + 1 {{ X < Y }}
The assignment rule again:
{{ Q [X ⊢> a] }} X ::= a {{ Q }}
Is the following triple a valid instance of this rule?
{{ X < Y }} X ::= X + 1 {{ X+1 < Y }}
(1) Yes
(2) No
{{ Q [X ⊢> a] }} X ::= a {{ Q }}
{{ X < Y }} X ::= X + 1 {{ X+1 < Y }}
The assignment rule again:
{{ Q [X ⊢> a] }} X ::= a {{ Q }}
Is the following triple a valid instance of this rule?
{{ X < Y }} X ::= X + 1 {{ X < Y+1 }}
(1) Yes
(2) No
{{ Q [X ⊢> a] }} X ::= a {{ Q }}
{{ X < Y }} X ::= X + 1 {{ X < Y+1 }}
The assignment rule again:
{{ Q [X ⊢> a] }} X ::= a {{ Q }}
Is the following triple a valid instance of this rule?
{{ True }} X ::= 3 {{ X = 3 }}
(1) Yes
(2) No
{{ Q [X ⊢> a] }} X ::= a {{ Q }}
{{ True }} X ::= 3 {{ X = 3 }}
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.
{{ True }} ->>
{{ (X = 1) [X ⊢> 1] }}
X ::= 1
{{ X = 1 }}
Example hoare_asgn_example1 :
{{True}} X ::= 1 {{X = 1}}.
Proof.
(* WORK IN CLASS *) Admitted.
We can also use it to prove the example mentioned earlier.
{{ X < 4 }} ->>
{{ (X < 5)[X ⊢> X + 1] }}
X ::= X + 1
{{ X < 5 }}
Example assn_sub_example2 :
{{X < 4}}
X ::= X + 1
{{X < 5}}.
Proof.
(* WORK IN CLASS *) Admitted.
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}}.
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.
Hint Unfold assert_of_Prop Aexp_of_nat Aexp_of_aexp.
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.
A good candidate for automation:
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.
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.
As can the same proof for the postcondition consequence
rule.
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 identifies the Hoare
rules that need to be used, and leaves the remaining low-level
details up to Coq to figure out.
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 ×. omega.
Qed.
Let's introduce our own tactic to handle both that bullet, as well as
the bullet from example 1:
Ltac assn_auto :=
try auto; (* as in example 1, above *)
try (unfold "->>", assn_sub, t_update;
intros; simpl in *; omega). (* 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.
{{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 about assertions! But it's
good enough so far.
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 }} c_{1} {{ Q }} | |
{{ Q }} c_{2} {{ R }} | (hoare_seq) |
{{ P }} c_{1};;c_{2} {{ R }} |
Theorem hoare_seq : ∀ P Q R c_{1} c_{2},
{{Q}} c_{2} {{R}} →
{{P}} c_{1} {{Q}} →
{{P}} c_{1};;c_{2} {{R}}.
Proof.
unfold hoare_triple.
intros P Q R c_{1} c_{2} H_{1} H_{2} st st' H_{12} Pre.
inversion H_{12}; subst.
eauto.
Qed.
unfold hoare_triple.
intros P Q R c_{1} c_{2} H_{1} H_{2} st st' H_{12} Pre.
inversion H_{12}; subst.
eauto.
Qed.
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 c_{1} and c_{2}:
{{ a = n }}
X ::= a;;
{{ X = n }} <--- decoration for Q
SKIP
{{ X = n }}
{{ a = n }}
X ::= a;;
{{ X = n }} <--- decoration for Q
SKIP
{{ X = n }}
Conditionals
{{P}} c_{1} {{Q}} | |
{{P}} c_{2} {{Q}} | |
{{P}} TEST b THEN c_{1} ELSE c_{2} {{Q}} |
{{ True }}
TEST X = 0
THEN Y ::= 2
ELSE Y ::= X + 1
FI
{{ X ≤ Y }}
Better:
{{P /\ b}} c_{1} {{Q}} | |
{{P /\ ~ b}} c_{2} {{Q}} | (hoare_if) |
{{P}} TEST b THEN c_{1} ELSE c_{2} FI {{Q}} |
Definition bassn b : Assertion :=
fun st ⇒ (beval st b = true).
Theorem hoare_if : ∀ P Q (b:bexp) c_{1} c_{2},
{{ P ∧ b }} c_{1} {{Q}} →
{{ P ∧ ¬b}} c_{2} {{Q}} →
{{P}} TEST b THEN c_{1} ELSE c_{2} FI {{Q}}.
Proof.
intros P Q b c_{1} c_{2} HTrue HFalse st st' HE HP.
inversion HE; subst; eauto.
Qed.
intros P Q b c_{1} c_{2} HTrue HFalse st st' HE HP.
inversion HE; subst; eauto.
Qed.
Example if_example :
{{True}}
TEST X = 0
THEN Y ::= 2
ELSE Y ::= X + 1
FI
{{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. omega.
- (* Else *)
eapply hoare_consequence_pre.
+ apply hoare_asgn.
+ assn_auto.
Qed.
Ltac assn_auto' :=
unfold "->>", assn_sub, t_update, bassn;
intros; simpl in *;
try rewrite → eqb_eq in *; (* for equalities *)
auto; try omega.
Example if_example'' :
{{True}}
TEST X = 0
THEN Y ::= 2
ELSE Y ::= X + 1
FI
{{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}}
TEST X = 0
THEN Y ::= 2
ELSE Y ::= X + 1
FI
{{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 omega.
☐
While Loops
{{P}} c {{P}}
The Hoare while rule combines the idea of an invariant with information about when guard b does or does not hold.
{{P ∧ b}} c {{P}}
----------------------------- (hoare_while)
{{P} WHILE b DO c {{P ∧ ¬b}}
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 involing while. *)
remember (WHILE b DO c END)%imp 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 involing while. *)
remember (WHILE b DO c END)%imp as original_command eqn:Horig.
induction Heval;
try (inversion Horig; subst; clear Horig);
eauto.
Qed.
WHILE X = 2 DO X ::= 1 END
Is the assertion
Y = 0
a loop invariant of the following?
WHILE X < 100 DO X ::= X + 1 END
(1) Yes
(2) No
Y = 0
WHILE X < 100 DO X ::= X + 1 END
Is the assertion
X = 0
a loop invariant of the following?
WHILE X < 100 DO X ::= X + 1 END
(1) Yes
(2) No
X = 0
WHILE X < 100 DO X ::= X + 1 END
Is the assertion
X < Y
a loop invariant of the following?
WHILE true DO X ::= X + 1;; Y ::= Y + 1 END
(1) Yes
(2) No
X < Y
WHILE true DO X ::= X + 1;; Y ::= Y + 1 END
Is the assertion
X = Y + Z
a loop invariant of the following?
WHILE Y > 10 DO Y := Y - 1;; Z ::= Z + 1 END
(1) Yes
(2) No
X = Y + Z
WHILE Y > 10 DO Y := Y - 1;; Z ::= Z + 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.
Is the assertion
X > 0
a loop invariant of the following?
WHILE X = 0 DO X ::= X - 1 END
(1) Yes
(2) No
X > 0
WHILE X = 0 DO X ::= X - 1 END
Is the assertion
X < 100
a loop invariant of the following?
WHILE X < 100 DO X ::= X + 1 END
(1) Yes
(2) No
X < 100
WHILE X < 100 DO X ::= X + 1 END
Is the assertion
X > 10
a loop invariant of the following?
WHILE X > 10 DO X ::= X + 1 END
(1) Yes
(2) No
X > 10
WHILE X > 10 DO X ::= X + 1 END
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.