This chapter is optional. It explores how Hoare can be studied as a logic in its own right, from the perspective of mathematical logic.

Hoare Logic and Model Theory

A valid Hoare triple expresses a truth about how Imp program execute.

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.

Hoare Logic and Proof Theory

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}}
               {{Q}} c₂ {{R}}
              ------------------ (hoare_seq)
              {{P}} c₁;; c₂ {{R}}


              {{P ∧ b}} c₁ {{Q}}
              {{P ∧ ¬b}} c₂ {{Q}}
      ------------------------------------ (hoare_if)
      {{P}} TEST b THEN c₁ ELSE c₂ 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}}

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 prove that the model-theoretic and proof-theoretic formalizations are consistent with one another.

Derivability

To formalize derivability of Hoare triples, we introduce inductive type derivable, which describes legal proof trees using the Hoare rules.

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}}

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.

Soundness and Completeness

We now have two approaches to formulating Hoare logic:

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

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:

• A logic is sound if everything that is derivable is valid.
• A logic is complete if everything that is valid is derivable.

We can prove that Hoare logic is sound and complete.

Postscript: Decidability

We might hope that Hoare logic would be 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. 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.