In this section we turn to the task of giving a formal system for the verification of partial correctness
assertions for while programs. Hoare’s proof system manipulates certain formulas, called Hoare formulas.
The proof system is built up according to the traditions of logical calculi: it consists of a set of axioms
together with a set of rules to derive conclusions from hypothesis. The axioms are themselves axiom
schemata: the substitution of concrete elements in place of metavariables of the axioms render the
concrete forms of the axioms. For example, if stands for the skip
axiom, then is an instance of it. We
defined an extended notion arithmetical expressions and logical formulas in the course of Section
1.3. Let and *Form*, respectively, stand for the sets of arithmetical
expressions and first order formulas defined there. We define the set of Hoare formulae as
follows.

Definition 35.LetP, . LetCbe a program, then is a Hoare correctness formula. The set of Hoare correctness formulae are denoted byH, while gives the formulas of Hoare logic.

Now we present the axioms and rules of the Hoare calculus. The names next to the rules or axioms are the rule- or axiom names.

In the consequence rule we denoted by the relation , where in the standard interpretation . In the next example we show in detail how to apply the Hoare rules as formal tools in proving a partial correctness assertion. We present the formal proof in a linear style rather than in a tree like form, we indicate by indices the order of deduction in the argument.

Definition 38.Let be a set of Hoare formulas, that is . We define inductively when a Hoare correctness formula is provable in the Hoare logic from . In notation .

If we fix an interpretation, we can talk about the meaning of Hoare formulas. As before, assume that
the base set of the interpretation is the set of natural numbers, function symbols like , ,
, etc., are interpreted as the usual functions on natural numbers, similar suppositions are
made concerning the predicate symbols like , , , etc. For the
sake of completeness, we give here the interpretation of terms and formulas. As before, let
be an interpretation, where is the base set- in our case
the set of natural numbers-, and is an interpretation of the constants, the and
function- and predicate symbols. Let be a state, we denote by
the state, which is the same as *s* except for the value at *X*, for
which holds. Then the interpretation of terms is as
follows:

For a fixed interpretation , we denote by the function
given by the expression . Now we can define the
interpretation of formulas. Let *A*, *B* be subsets of some set *S*. Then should denote
the set .

We may also apply the notation instead of . is called the meaning of the predicate

Punder the interpretation . If is fixed, we simply write . As an abuse of notation we identify sets of states and their characteristic functions. Thus, may also stand for , where iff for a fixed interpretation . We say thatPis true for the fixed interpretation , if for every . We may apply the notation , and , if , and are true, respectively.

The interpretation of a Hoare correctness formula is defined as follows.

Definition 41.Let be a Hoare correctness formula. Then the meaning of the formula is

which is , by Definition 22. We may write for , as well. We omit the superscripts , if the interpretation is fixed.

It is a natural question to ask whether our deductive system is sound and complete. The soundness of Hoare logic is an easy consequence of Theorem 28, we state it without repeating the proof. The only change is the presence of the assumption that the formulas in should hold in the interpretation .

The case of the completeness assertion is somewhat more elaborate. First of all, observe that in rule
the consequence depends on hypothesis two of which must be provable arithmetical
formulas. But, by Gödel’s results, we know that there exist true formulas in usual first order arithmetic
(Peano arithmetic) which are not provable. This already gives a boundary of provability in Hoare logic
also. Besides this, there emerge other problems, too. Assume by some oracle we know about the truth
values of the arithmetical formulas we use in our proofs. In the course of the proof of Theorem
30, for example, we encountered the necessity of finding an assertion *i* for which
and hold,
given that is true. This could be done by defining *i* as
.
In the case of Hoare logic, for pre- and postconditions of programs only assertions defined by
first order Hoare formulas are allowed. Is it the case for every
and program *C* that we can find a formula *A* such that is true iff
implies . In
general, the answer is no. But in the case of Peano arithmetic, we can find an affirmative answer, which
the next section is about.