# HoareAsLogicHoare Logic as a Logic

Definition valid (P : Assertion) (c : com) (Q : Assertion) : Prop :=

∀ st st',

st =[ c ]=> st' →

P st →

Q st'.

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
Proof rules constitute a logic in their own right:

---------------- (hoare_skip)

{{P}} SKIP {{P}}

----------------------------- (hoare_asgn)

{{Q [X ⊢> a]}} X ::= a {{Q}}

{{P}} c

{{Q}} c

------------------ (hoare_seq)

{{P}} c

{{P ∧ b}} c

{{P ∧ ¬b}} c

------------------------------------ (hoare_if)

{{P}} TEST b THEN c

{{P ∧ b}} c {{P}}

----------------------------- (hoare_while)

{{P} WHILE b DO c {{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}}

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
Our goal for the rest of this chapter is to formalize Hoare logic using
proof theory, and 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.

*model theory*.# Hoare Logic and Proof Theory

---------------- (hoare_skip)

{{P}} SKIP {{P}}

----------------------------- (hoare_asgn)

{{Q [X ⊢> a]}} X ::= a {{Q}}

{{P}} c

_{1}{{Q}}{{Q}} c

_{2}{{R}}------------------ (hoare_seq)

{{P}} c

_{1};; c_{2}{{R}}{{P ∧ b}} c

_{1}{{Q}}{{P ∧ ¬b}} c

_{2}{{Q}}------------------------------------ (hoare_if)

{{P}} TEST b THEN c

_{1}ELSE c_{2}FI {{Q}}{{P ∧ b}} c {{P}}

----------------------------- (hoare_while)

{{P} WHILE b DO c {{P ∧ ¬b}}

{{P'}} c {{Q'}}

P ->> P'

Q' ->> Q

----------------------------- (hoare_consequence)

{{P}} c {{Q}}

### Those rules can be used to show that a triple is

*derivable*by constructing a proof tree:--------------------------- (hoare_asgn)

X=0 ->> X+1=1 {{X+1=1}} X ::= X+1 {{X=1}}

---------------------------------------------------------- (hoare_consequence)

{{X=0}} X ::= X+1 {{X=1}}

*proof theory*.# Derivability

Inductive derivable : Assertion → com → Assertion → Type :=

| H_Skip : ∀ P,

derivable P (SKIP) P

| H_Asgn : ∀ Q X a,

derivable (Q [X ⊢> a]) (X ::= 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 : bexp) c

_{1}c

_{2},

derivable (P ∧ b) c

_{1}Q →

derivable (P ∧ ¬b) c

_{2}Q →

derivable P (TEST b THEN c

_{1}ELSE c

_{2}FI) Q

| H_While : ∀ P (b : bexp) c,

derivable (P ∧ b) c P →

derivable P (WHILE b DO c END) (P ∧ ¬b)

| H_Consequence : ∀ P Q P' Q' c,

derivable P' c Q' →

P ->> P' →

Q' ->> Q →

derivable P c Q.

{{(X=3) [X ⊢> X + 2] [X ⊢> X + 1]}}

X ::= X + 1;;

X ::= X + 2

{{X=3}}

Example example_proof :

derivable

((X = 3) [X ⊢> X + 2] [X ⊢> X + 1])

(X ::= X + 1;; X ::= X + 2)

(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.
We now have two approaches to formulating Hoare logic:
Do these two approaches agree? That is, are the valid Hoare triples exactly
the derivable ones? This is a standard question investigated in
mathematical logic. There are two pieces to answering it:
We can prove that Hoare logic is sound and complete.
We might hope that Hoare logic would be
Consider the triple {{True}} c {{False}}. This triple is valid if and
only if c is non-terminating. So any algorithm that could
determine validity of arbitrary triples could solve the Halting
Problem.
Similarly, the triple {{True}} SKIP {{P}} is valid if and only if
∀ s, P s is valid, where P is an arbitrary assertion of Coq's
logic. But it is known that there can be no decision procedure for
this logic.

# 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.

# Postscript: Decidability

*decidable*; that is, that there is an (terminating) algorithm (a*decision procedure*) that can determine whether or not a given Hoare triple is valid or derivable. But such a decision procedure cannot exist.