(** * Hoare: Hoare Logic, Part I *)
Set Warnings "-notation-overridden,-parsing".
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 omega.Omega.
From PLF Require Import Imp.
(** What we've done so far:
- Formalized Imp
- identifiers and states
- abstract syntax trees
- evaluation functions (for [aexp]s and [bexp]s)
- evaluation relation (for commands)
- Proved some _metatheoretic_ properties
- 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
- meaning-preservation of some program transformations
- behavioral equivalence of programs ([Equiv]) *)
(** We've dealt with a few sorts of properties of Imp programs:
- Termination
- Nontermination
- Equivalence
Overview of this chapter...
Topic:
- A systematic method for reasoning about the _functional
correctness_ of programs in Imp
Goals:
- a natural notation for _program specifications_ and
- a _compositional_ proof technique for program correctness
Plan:
- specifications (assertions / Hoare triples)
- proof rules
- loop invariants
- decorated programs
- examples *)
(* ################################################################# *)
(** * Assertions *)
Definition Assertion := state -> Prop.
(* QUIZ
Paraphrase the following assertions in English
(1) [fun st => st X = 3]
(2) [fun st => st X <= st Y]
(3) [fun st => st X = 3 \/ st X <= st Y]
(4) [fun st => st Z * st Z <= st X /\
~ (((S (st Z)) * (S (st Z))) <= st X)]
(5) [fun st => True]
(6) [fun st => False]
*)
(* /QUIZ *)
(** Informally, instead of writing
fun st => (st Z) * (st Z) <= m /\
~ ((S (st Z)) * (S (st Z)) <= m)
we'll write just
Z * Z <= m /\ ~((S Z) * (S Z) <= m).
*)
(** Given two assertions [P] and [Q], we say that [P] _implies_ [Q],
written [P ->> Q], if, whenever [P] holds in some state [st], [Q]
also holds. *)
Definition assert_implies (P Q : Assertion) : Prop :=
forall 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.
(* ################################################################# *)
(** * Hoare Triples *)
(** In general, the behavior of a command is to transform one state to
another, so it is natural to express claims about commands in
terms of assertions that are true before and after the command
executes:
- "If command [c] is started in a state satisfying assertion
[P], and if [c] eventually terminates in some final state,
then this final state will satisfy the assertion [Q]."
Such a claim is called a _Hoare Triple_. The assertion [P] is
called the _precondition_ of [c], while [Q] is the
_postcondition_. *)
(** Formally: *)
Definition hoare_triple
(P : Assertion) (c : com) (Q : Assertion) : Prop :=
forall st st',
st =[ c ]=> st' ->
P st ->
Q st'.
(** Since we'll be working a lot with Hoare triples, it's useful to
have a compact notation:
{{P}} c {{Q}}.
*)
Notation "{{ P }} c {{ Q }}" :=
(hoare_triple P c Q) (at level 90, c at next level)
: hoare_spec_scope.
(* QUIZ
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)}}
*)
(* /QUIZ *)
(* QUIZ
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
*)
(* /QUIZ *)
(* QUIZ
What about this one?
{{X = 2}} X ::= X + 1 {{X = 3}}
(1) Yes
(2) No
*)
(* /QUIZ *)
(* QUIZ
What about this one?
{{True}} X ::= 5;; Y ::= 0 {{X = 5}}
(1) Yes
(2) No
*)
(* /QUIZ *)
(* QUIZ
What about this one?
{{X = 2 /\ X = 3}} X ::= 5 {{X = 0}}
(1) Yes
(2) No
*)
(* /QUIZ *)
(* QUIZ
What about this one?
{{True}} SKIP {{False}}
(1) Yes
(2) No
*)
(* /QUIZ *)
(* QUIZ
What about this one?
{{False}} SKIP {{True}}
(1) Yes
(2) No
*)
(* /QUIZ *)
(* QUIZ
What about this one?
{{True}} WHILE true DO SKIP END {{False}}
(1) Yes
(2) No
*)
(* /QUIZ *)
(* QUIZ
This one?
{{X = 0}}
WHILE X = 0 DO X ::= X + 1 END
{{X = 1}}
(1) Yes
(2) No
*)
(* /QUIZ *)
(* QUIZ
This one?
{{X = 1}}
WHILE ~(X = 0) DO X ::= X + 1 END
{{X = 100}}
(1) Yes
(2) No
*)
(* /QUIZ *)
(** To get us warmed up for what's coming, here are two simple facts
about Hoare triples. (Make sure you understand what they mean.) *)
Theorem hoare_post_true : forall (P Q : Assertion) c,
(forall st, Q st) ->
{{P}} c {{Q}}.
Proof.
intros P Q c H. unfold hoare_triple.
intros st st' Heval HP.
apply H. Qed.
Theorem hoare_pre_false : forall (P Q : Assertion) c,
(forall st, ~ (P st)) ->
{{P}} c {{Q}}.
Proof.
intros P Q c H. unfold hoare_triple.
intros st st' Heval HP.
unfold not in H. apply H in HP.
inversion HP. Qed.
(* ################################################################# *)
(** * Proof Rules *)
(** Plan:
- 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 *)
(** The rule for assignment is the most fundamental of the Hoare logic
proof rules. Here's how it works.
Consider this valid Hoare triple:
{{ Y = 1 }} X ::= Y {{ X = 1 }}
That is, the property of being equal to [1] gets transferred
from [Y] to [X]. *)
(** Similarly, in
{{ Y + Z = 1 }} X ::= Y + Z {{ X = 1 }}
the same property (being equal to one) gets transferred to
[X] from the expression [Y + Z] on the right-hand side of
the assignment. *)
(** More generally, if [a] is _any_ arithmetic expression, then
{{ a = 1 }} X ::= a {{ X = 1 }}
is a valid Hoare triple. *)
(** Even more generally, to conclude that an arbitrary assertion [Q]
holds after [X ::= a], we need to assume that [Q] holds before [X
::= a], but _with all occurrences of_ [X] replaced by [a] in
[Q]. This leads to the Hoare rule for assignment
{{ Q [X |-> a] }} X ::= a {{ Q }}
where "[Q [X |-> a]]" is pronounced "[Q] where [a] is substituted
for [X]". *)
(** For example, these are valid applications of the assignment
rule:
{{ (X <= 5) [X |-> X + 1]
i.e., X + 1 <= 5 }}
X ::= X + 1
{{ X <= 5 }}
{{ (X = 3) [X |-> 3]
i.e., 3 = 3 }}
X ::= 3
{{ X = 3 }}
{{ (0 <= X /\ X <= 5) [X |-> 3]
i.e., (0 <= 3 /\ 3 <= 5) }}
X ::= 3
{{ 0 <= X /\ X <= 5 }}
*)
(** To formalize the rule, we must first formalize the idea of
"substituting an expression for an Imp variable in an assertion",
which we refer to as assertion substitution, or [assn_sub]. That
is, given a proposition [P], a variable [X], and an arithmetic
expression [a], we want to derive another proposition [P'] that is
just the same as [P] except that [P'] should mention [a] wherever
[P] mentions [X]. *)
(** 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 :=
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:
------------------------------ (hoare_asgn)
{{Q [X |-> a]}} X ::= a {{Q}}
*)
(** We can prove formally that this rule is indeed valid. *)
Theorem hoare_asgn : forall 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.
(** Here's a first formal proof using this rule. *)
Example assn_sub_example :
{{(fun st => st X < 5) [X |-> X + 1]}}
X ::= X + 1
{{fun st => st 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}}
We will see how to do so in the next section. *)
(* QUIZ
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
*)
(* /QUIZ *)
(* QUIZ
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
*)
(* /QUIZ *)
(* QUIZ
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
*)
(* /QUIZ *)
(* QUIZ
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
*)
(* /QUIZ *)
(* QUIZ
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
*)
(* /QUIZ *)
(* QUIZ
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
*)
(* /QUIZ *)
(* ================================================================= *)
(** ** Consequence *)
(** Sometimes the preconditions and postconditions we get from the
Hoare rules won't quite be the ones we want in the particular
situation at hand -- they may be logically equivalent but have a
different syntactic form that fails to unify with the goal we are
trying to prove, or they actually may be logically weaker (for
preconditions) or stronger (for postconditions) than what we need.
For instance, while
{{(X = 3) [X |-> 3]}} X ::= 3 {{X = 3}},
follows directly from the assignment rule,
{{True}} X ::= 3 {{X = 3}}
does not. This triple is valid, but it is not an instance of
[hoare_asgn] because [True] and [(X = 3) [X |-> 3]] are not
syntactically equal assertions. However, they are logically
_equivalent_, so if one triple is valid, then the other must
certainly be as well. We can capture this observation with the
following rule:
{{P'}} c {{Q}}
P <<->> P'
----------------------------- (hoare_consequence_pre_equiv)
{{P}} c {{Q}}
*)
(** Taking this line of thought a bit further, we can see that
strengthening the precondition or weakening the postcondition of a
valid triple always produces another valid triple. This
observation is captured by two _Rules of Consequence_.
{{P'}} c {{Q}}
P ->> P'
----------------------------- (hoare_consequence_pre)
{{P}} c {{Q}}
{{P}} c {{Q'}}
Q' ->> Q
----------------------------- (hoare_consequence_post)
{{P}} c {{Q}}
*)
(** Here are the formal versions: *)
Theorem hoare_consequence_pre : forall (P P' Q : Assertion) c,
{{P'}} c {{Q}} ->
P ->> P' ->
{{P}} c {{Q}}.
Proof.
intros P P' Q c Hhoare Himp.
intros st st' Hc HP. apply (Hhoare st st').
assumption. apply Himp. assumption. Qed.
Theorem hoare_consequence_post : forall (P Q Q' : Assertion) c,
{{P}} c {{Q'}} ->
Q' ->> Q ->
{{P}} c {{Q}}.
Proof.
intros P Q Q' c Hhoare Himp.
intros st st' Hc HP.
apply Himp.
apply (Hhoare st st').
assumption. assumption. Qed.
(** For example, we can use the first consequence rule like this:
{{ True }} ->>
{{ (X = 1) [X |-> 1] }}
X ::= 1
{{ X = 1 }}
Or, formally... *)
Example hoare_asgn_example1 :
{{fun st => True}} X ::= 1 {{fun st => st 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 }}
Or, formally ... *)
Example assn_sub_example2 :
{{(fun st => st X < 4)}}
X ::= X + 1
{{fun st => st X < 5}}.
Proof.
(* WORK IN CLASS *) Admitted.
(** Finally, for convenience in proofs, here is a combined rule of
consequence that allows us to vary both the precondition and the
postcondition in one go.
{{P'}} c {{Q'}}
P ->> P'
Q' ->> Q
----------------------------- (hoare_consequence)
{{P}} c {{Q}}
*)
Theorem hoare_consequence : forall (P P' Q Q' : Assertion) c,
{{P'}} c {{Q'}} ->
P ->> P' ->
Q' ->> Q ->
{{P}} c {{Q}}.
Proof.
intros P P' Q Q' c Hht HPP' HQ'Q.
apply hoare_consequence_pre with (P' := P').
apply hoare_consequence_post with (Q' := Q').
assumption. assumption. assumption. Qed.
(* ================================================================= *)
(** ** Skip *)
(** Since [SKIP] doesn't change the state, it preserves any
assertion [P]:
-------------------- (hoare_skip)
{{ P }} SKIP {{ P }}
*)
Theorem hoare_skip : forall P,
{{P}} SKIP {{P}}.
Proof.
intros P st st' H HP. inversion H. subst.
assumption. Qed.
(* ================================================================= *)
(** ** Sequencing *)
(** More interestingly, if the command [c1] takes any state where
[P] holds to a state where [Q] holds, and if [c2] takes any
state where [Q] holds to one where [R] holds, then doing [c1]
followed by [c2] will take any state where [P] holds to one
where [R] holds:
{{ P }} c1 {{ Q }}
{{ Q }} c2 {{ R }}
---------------------- (hoare_seq)
{{ P }} c1;;c2 {{ R }}
*)
Theorem hoare_seq : forall P Q R c1 c2,
{{Q}} c2 {{R}} ->
{{P}} c1 {{Q}} ->
{{P}} c1;;c2 {{R}}.
Proof.
intros P Q R c1 c2 H1 H2 st st' H12 Pre.
inversion H12; subst.
apply (H1 st'0 st'); try assumption.
apply (H2 st st'0); assumption. Qed.
(** 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 }}
*)
(** Here's an example of a program involving both assignment and
sequencing. *)
Example hoare_asgn_example3 : forall a n,
{{fun st => aeval st a = n}}
X ::= a;; SKIP
{{fun st => st X = n}}.
Proof.
intros a n. eapply hoare_seq.
- (* right part of seq *)
apply hoare_skip.
- (* left part of seq *)
eapply hoare_consequence_pre. apply hoare_asgn.
intros st H. subst. reflexivity.
Qed.
(* ================================================================= *)
(** ** Conditionals *)
(** What sort of rule do we want for reasoning about conditional
commands?
Certainly, if the same assertion [Q] holds after executing
either of the branches, then it holds after the whole conditional.
So we might be tempted to write:
{{P}} c1 {{Q}}
{{P}} c2 {{Q}}
---------------------------------
{{P}} TEST b THEN c1 ELSE c2 {{Q}}
*)
(** However, this is rather weak. For example, using this rule,
we cannot show
{{ True }}
TEST X = 0
THEN Y ::= 2
ELSE Y ::= X + 1
FI
{{ X <= Y }}
since the rule tells us nothing about the state in which the
assignments take place in the "then" and "else" branches. *)
(** Better:
{{P /\ b}} c1 {{Q}}
{{P /\ ~ b}} c2 {{Q}}
------------------------------------ (hoare_if)
{{P}} TEST b THEN c1 ELSE c2 FI {{Q}}
*)
(** To make this formal, we need a way of formally "lifting"
any bexp [b] to an assertion.
We'll write [bassn b] for the assertion "the boolean expression
[b] evaluates to [true]." *)
Definition bassn b : Assertion :=
fun st => (beval st b = true).
(** A couple of useful facts about [bassn]: *)
Lemma bexp_eval_true : forall b st,
beval st b = true -> (bassn b) st.
Proof.
intros b st Hbe.
unfold bassn. assumption. Qed.
Lemma bexp_eval_false : forall b st,
beval st b = false -> ~ ((bassn b) st).
Proof.
intros b st Hbe contra.
unfold bassn in contra.
rewrite -> contra in Hbe. inversion Hbe. Qed.
(** Now we can formalize the Hoare proof rule for conditionals
and prove it correct. *)
Theorem hoare_if : forall P Q b c1 c2,
{{fun st => P st /\ bassn b st}} c1 {{Q}} ->
{{fun st => P st /\ ~ (bassn b st)}} c2 {{Q}} ->
{{P}} TEST b THEN c1 ELSE c2 FI {{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.
apply bexp_eval_true. assumption.
- (* b is false *)
apply (HFalse st st').
assumption.
split. assumption.
apply bexp_eval_false. assumption. Qed.
(* ----------------------------------------------------------------- *)
(** *** Example *)
Example if_example :
{{fun st => True}}
TEST X = 0
THEN Y ::= 2
ELSE Y ::= X + 1
FI
{{fun st => st X <= st Y}}.
Proof.
(* WORK IN CLASS *) Admitted.
(** [] *)
(* ================================================================= *)
(** ** Recap *)
(** Idea: create a _domain specific logic_ for reasoning about
properties of Imp programs.
- This hides the low-level details of the semantics of the program
- Leads to a compositional reasoning process
The basic structure is given by _Hoare triples_ of the form:
{{P}} c {{Q}}
- [P] and [Q] are assertions about the state of the Imp program.
- "If command [c] is started in a state satisfying assertion [P],
and if [c] eventually terminates in some final state, then this
final state will satisfy the assertion [Q]." *)
(** The rules of Hoare Logic (so far):
----------------------------- (hoare_asgn)
{{Q [X |-> a]}} X ::= a {{Q}}
---------------- (hoare_skip)
{{P}} SKIP {{P}}
{{P}} c1 {{Q}}
{{Q}} c2 {{R}}
------------------ (hoare_seq)
{{P}} c1;;c2 {{R}}
{{P /\ b}} c1 {{Q}}
{{P /\ ~ b}} c2 {{Q}}
------------------------------------ (hoare_if)
{{P}} TEST b THEN c1 ELSE c2 FI {{Q}}
{{P'}} c {{Q'}}
P ->> P'
Q' ->> Q
----------------------------- (hoare_consequence)
{{P}} c {{Q}}
*)
(* ================================================================= *)
(** ** Loops *)
(** Suppose we have a loop
WHILE b DO c END
and we want to find a precondition [P] and a postcondition
[Q] such that
{{P}} WHILE b DO c END {{Q}}
is a valid triple. *)
(** If [b] is false, then the loop is like [SKIP]:
{{P}} WHILE b DO c END {{P}}.
*)
(** But, as we remarked above for the conditional, we know a
little more at the end -- not just [P], but also the fact
that [b] is false in the current state. So we can enrich the
postcondition a little:
But, as with [if], we also know [~ b] in the postcondition:
{{P}} WHILE b DO c END {{P /\ ~ b}}
*)
(** What about when [b] is true?
First attempt:
{{P}} c {{P}}
-----------------------------------
{{P}} WHILE b DO c END {{P /\ ~ b}}
This is almost the rule we want, but again it can be improved a
little: at the beginning of the loop body, we know not only that
[P] holds, but also that the guard [b] is true in the current
state. *)
(** We know that [b] is true in the precondition of [c].
And this leads us to the final version of the rule:
{{P /\ b}} c {{P}}
---------------------------------- (hoare_while)
{{P}} WHILE b DO c END {{P /\ ~ b}}
The proposition [P] is called an _invariant_ of the loop.
*)
Theorem hoare_while : forall P b c,
{{fun st => P st /\ bassn b st}} c {{P}} ->
{{P}} WHILE b DO c END {{fun st => P st /\ ~ (bassn b st)}}.
Proof.
intros P b c Hhoare st st' He HP.
(* Like we've seen before, we need to reason by induction
on [He], because, in the "keep looping" case, its hypotheses
talk about the whole loop instead of just [c]. *)
remember (WHILE b DO c END)%imp as wcom eqn:Heqwcom.
induction He;
try (inversion Heqwcom); subst; clear Heqwcom.
- (* E_WhileFalse *)
split. assumption. apply bexp_eval_false. assumption.
- (* E_WhileTrue *)
apply IHHe2. reflexivity.
apply (Hhoare st st'). assumption.
split. assumption. apply bexp_eval_true. assumption.
Qed.
(* QUIZ
Is the assertion
Y = 0
an invariant of the following loop?
WHILE X .< 100 DO X ::= X + 1 END
(1) Yes
(2) No
*)
(* /QUIZ *)
(* QUIZ
Is the assertion
X = 0
an invariant of the following loop?
WHILE X .< 100 DO X ::= X + 1 END
(1) Yes
(2) No
*)
(* /QUIZ *)
(* QUIZ
Is the assertion
X < Y
an invariant of the following loop?
WHILE true DO X ::= X + 1;; Y ::= Y + 1 END
(1) Yes
(2) No
*)
(* /QUIZ *)
(* QUIZ
Is the assertion
X = Y + Z
an invariant of the following loop?
WHILE Y .> 10 DO Y := Y - 1;; Z ::= Z + 1 END
(1) Yes
(2) No
*)
(* /QUIZ
One subtlety in the terminology is that calling some assertion [P]
a "loop invariant" doesn't just mean that it is preserved by the
body of the loop in question (i.e., [{{P}} c {{P}}], where [c] is
the loop body), but rather that [P] _together with the fact that
the loop's guard is true_ is a sufficient precondition for [c] to
ensure [P] as a postcondition.
This is a slightly (but importantly) weaker requirement. For
example, if [P] is the assertion [X = 0], then [P] _is_ an
invariant of the loop
WHILE X = 2 DO X := 1 END
although it is clearly _not_ preserved by the body of the
loop. *)
(* QUIZ
Is the assertion
X > 0
an invariant of the following loop?
WHILE X = 0 DO X ::= X - 1 END
(1) Yes
(2) No
*)
(* /QUIZ *)
(* QUIZ
Is the assertion
X < 100
an invariant of the following loop?
WHILE X .< 100 DO X ::= X + 1 END
(1) Yes
(2) No
*)
(* /QUIZ *)
(* QUIZ
Is the assertion
X > 10
an invariant of the following loop?
WHILE X .> 10 DO X ::= X + 1 END
(1) Yes
(2) No
*)
(* /QUIZ
We can use the WHILE rule to prove the following Hoare triple... *)
Theorem always_loop_hoare : forall P Q,
{{P}} WHILE true DO SKIP END {{Q}}.
Proof.
(* WORK IN CLASS *) Admitted.