HoareAsLogicHoare Logic as a Logic
Set Warnings "-deprecated-hint-without-locality,-deprecated-hint-without-locality".
From PLF Require Import Maps.
From PLF Require Import Imp.
Hint Constructors ceval : core.
From PLF Require Import Hoare.
Hoare Logic and Model Theory
Pre: X = 0
Com: X ::= X + 1
Post: X = 1
Pre: X = 0
Com: skip
Post: X = 1
Definition valid (P : Assertion) (c : com) (Q : Assertion) : Prop :=
∀ st st',
st =[ c ]=> st' →
P st →
Q st'.
This notion of validity is based on the underlying model of how
Imp programs execute. That model itself is based on states. So,
Pre: X = 0
Com: X ::= X + 1
Post: X = 1
is valid, because starting from any state in which X is 0,
and executing X ::= X + 1, we are guaranteed to reach a state in
which X is 1. But,
Pre: X = 0
Com: skip
Post: X = 1
is invalid, because starting from any state in which X is 0,
we are guaranteed not to change the state, so X cannot be 1.
So far, we have punned between the syntax of a Hoare triple,
written {{P}} c {{Q}}, and its validity, as expressed by
valid. In essence, we have said that the semantic meaning of
that syntax is the proposition returned by valid. This way of
giving semantic meaning to something syntactic is part of the
branch of mathematical logic known as model theory.
Our approach to Hoare logic through model theory led us to
state proof rules in terms of that same state-based model, and to
prove program correctness in it, too. But there is another
approach, which is arguably more common in Hoare logic. We turn to
it, next.
Instead of using states and evaluation as the basis for reasoning,
let's take the proof rules from Hoare as the basis. Those
proof rules give us a set of axioms and inference rules that
constitute a logic in their own right. We repeat them here:
---------------- (hoare_skip)
{{P}} skip {{P}}
----------------------------- (hoare_asgn)
{{Q [X ⊢> a]}} X ::= a {{Q}}
{{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}}
Read the Hoare triples in those rules as devoid of any
meaning other than what the rules give them. Forget about states
and evaluations. They are just syntax that the rules tell us how
to manipulate in legal ways.
Through this new lens, triple {{X = 0}} X ::= X + 1 {{X = 1}}
is derivable, because we can derive a proof tree using the rules:
--------------------------- (hoare_asgn)
X=0 ->> X+1=1 {{X+1=1}} X ::= X+1 {{X=1}}
---------------------------------------------------------- (hoare_consequence)
{{X=0}} X ::= X+1 {{X=1}}
At each step we have either used one of the rules, or we
have appealed to reasoning about assertions, which do not involve
Hoare triples. (Note that we have left off the trivial part of
hoare_consequence above, namely X=1 ->> X=1, only because of
horizontal space contraints: it's hard to fit that many characters
on a line and have the page still be readable. If you prefer,
think of it as using hoare_consequence_pre instead.)
On the other hand, {{X = 0}} skip {{X = 1}} is not derivable,
because there is no way to apply the rules to construct a proof
tree with this triple at its root.
This approach gives meaning to triples not in terms of a model,
but in terms of how they can be used to construct proof trees.
It's a different way of giving semantic meaning to something
syntactic, and it's part of the branch of mathematical logic known
as proof theory.
Our goal for the rest of this chapter is to formalize Hoare logic
using proof theory, and then to prove that the model-theoretic and
proof-theoretic formalizations are consistent with one another.
To formalize derivability of Hoare triples, we introduce inductive type
derivable, which describes legal proof trees using the Hoare rules.
Pre: X = 0
Com: X ::= X + 1
Post: X = 1
Pre: X = 0
Com: skip
Post: X = 1
Hoare Logic and Proof Theory
---------------- (hoare_skip)
{{P}} skip {{P}}
----------------------------- (hoare_asgn)
{{Q [X ⊢> a]}} X ::= a {{Q}}
{{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}}
--------------------------- (hoare_asgn)
X=0 ->> X+1=1 {{X+1=1}} X ::= X+1 {{X=1}}
---------------------------------------------------------- (hoare_consequence)
{{X=0}} X ::= X+1 {{X=1}}
Derivability
Inductive derivable : Assertion → com → Assertion → Type :=
| H_Skip : ∀ P,
derivable P <{skip}> P
| H_Asgn : ∀ Q V a,
derivable (Q [V ⊢> a]) <{V := a}> Q
| H_Seq : ∀ P c Q d R,
derivable P c Q → derivable Q d R → derivable P <{c;d}> R
| H_If : ∀ P Q b c1 c2,
derivable (fun st ⇒ P st ∧ bassn b st) c1 Q →
derivable (fun st ⇒ P st ∧ ~(bassn b st)) c2 Q →
derivable P <{if b then c1 else c2 end}> Q
| H_While : ∀ P b c,
derivable (fun st ⇒ P st ∧ bassn b st) c P →
derivable P <{while b do c end}> (fun st ⇒ P st ∧ ¬ (bassn b st))
| H_Consequence : ∀ (P Q P' Q' : Assertion) c,
derivable P' c Q' →
(∀ st, P st → P' st) →
(∀ st, Q' st → Q st) →
derivable P c Q.
We don't need to include axioms corresponding to
hoare_consequence_pre or hoare_consequence_post, because these
can be proven easily from H_Consequence.
Lemma H_Consequence_pre : ∀ (P Q P': Assertion) c,
derivable P' c Q →
(∀ st, P st → P' st) →
derivable P c Q.
Lemma H_Consequence_post : ∀ (P Q Q' : Assertion) c,
derivable P c Q' →
(∀ st, Q' st → Q st) →
derivable P c Q.
As an example, let's construct a proof tree for
{{(X=3) [X ⊢> X + 2] [X ⊢> X + 1]}}
X ::= X + 1;;
X ::= X + 2
{{X=3}}
{{(X=3) [X ⊢> X + 2] [X ⊢> X + 1]}}
X ::= X + 1;;
X ::= X + 2
{{X=3}}
Example sample_proof :
derivable
((fun st:state ⇒ st X = 3) [X ⊢> X + 2] [X ⊢> X + 1])
<{ X := X + 1; X := X + 2}>
(fun st:state ⇒ st X = 3).
Proof.
eapply H_Seq.
- apply H_Asgn.
- apply H_Asgn.
Qed.
You can see how the structure of the proof script mirrors the structure
of the proof tree: at the root there is a use of the sequence rule; and
at the leaves, the assignment rule.
Show that any Hoare triple whose postcondition is True is derivable. Proceed
by induction on c.
Exercise: 3 stars, standard (provable_true_post)
Exercise: 3 stars, standard (provable_false_pre)
Soundness and Completeness
- The model-theoretic approach uses valid to characterize when a Hoare
triple holds in a model, which is based on states.
- The proof-theoretic approach uses derivable to characterize when a Hoare triple is derivable as the end of a proof tree.
- A logic is sound if everything that is derivable is valid.
- A logic is complete if everything that is valid is derivable.
Exercise: 3 stars, standard (hoare_sound)
Definition wp (c:com) (Q:Assertion) : Assertion :=
fun s ⇒ ∀ s', s =[ c ]=> s' → Q s'.
Hint Unfold wp : core.
The following two theorems show that the two ways of thinking
about wp are the same.
Theorem wp_is_precondition : ∀ c Q,
{{wp c Q}} c {{Q}}.
Proof. auto. Qed.
Theorem wp_is_weakest : ∀ c Q P',
{{P'}} c {{Q}} →
P' ->> (wp c Q).
Proof. eauto. Qed.
Weakest preconditions are useful because they enable us to
identify assertions that otherwise would require clever thinking.
The next two lemmas show that in action.
What if we have a sequence c1;; c2, but not an intermediate assertion for
what should hold in between c1 and c2? No problem. Prove that wp c2 Q
suffices as such an assertion.
Exercise: 1 star, standard (wp_seq)
Lemma wp_seq : ∀ P Q c1 c2,
derivable P c1 (wp c2 Q) → derivable (wp c2 Q) c2 Q → derivable P <{c1; c2}> Q.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard (wp_invariant)
Lemma wp_invariant : ∀ b c Q,
valid (wp <{while b do c end}> Q ∧ b) c (wp <{while b do c end}> Q).
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 4 stars, standard (hoare_complete)
Theorem hoare_complete: ∀ P c Q,
valid P c Q → derivable P c Q.
Proof.
unfold valid. intros P c. generalize dependent P.
induction c; intros P Q HT.
(* FILL IN HERE *) Admitted.
☐
Postscript: Decidability
(* 2021-03-18 17:24 *)