**Table of Contents**

- The operational semantics of while programs
- Denotational semantics of while programs
- Partial correctness of while-programs
- The stepwise Floyd–Naur method
- Hoare logic from a semantical point of view
- Proof outlines
- Proof rules for the Hoare calculus
- The wlp-calculus
- Relative completeness of the Hoare partial correctness calculus
- The wp-calculus
- Total correctness
- Soundness of the Hoare total correctness calculus
- Relative completeness of the Hoare total correctness calculus

While programs constitute a set of deterministic programs. A while program is a string of symbols, they represent the core of ALGOL-like languages. An abstract syntax is given for the formulation of while programs:

where form the set of variables and

Bdenotes a Boolean andEstands for an arithmetical expression, respectively. We write for the set of while programs.

Unless otherwise stated by Boolean expressions we mean the set of formal arithmetic expressions built from natural numbers, variables and usual number theoretic functions and relations like summation, subtraction, multiplication, division, equality, less than or equals and so on.

For the sake of clarity, we give some elementary definitions of these notions. For the time being, we
restrict ourselves to basic arithmetic operations. We assume a fixed domain to be given, it is either
the set of natural numbers or the set of integers. Unless otherwise stated let denote the natural
numbers. Let capital letters *X*, *Y *, etc. denote variables, and let *n*,
stand for elements of . Then

are arithmetical expressions. The set of arithmetical expressions is denoted by . If represents the natural numbers, then subtraction is understood as follows:

Otherwise it is the usual subtraction of integers. In the sequel, by an abuse of notation, we use instead of . In the definition below let , be arithmetical expressions. Then

are Boolean expressions. The set of Boolean expressions is denoted by . In order to facilitate writing expressions we use usual conventions for the order of evaluation of operators: multiplication is evaluated before addition and subtraction etc. We also introduce convenient abbreviations, like

and

If possible, we omit parentheses in Boolean expressions, stipulating that conjunction and disjunction binds stronger than implication, which is stronger than equivalence. Negation is stronger than any of the two argument logical operations.

With this in hand we can turn to the informal explanations of the elements of a program. The meaning of is self explanatory: it always terminates and leaves everything as was before its execution. We can define the abbreviation then

The command , where *X* is a variable and *E* is an arithmetical expression, is called an
*assignment*. The meaning of the *conditional statement * is again self explanatory, whereas the *while
statement*, or *loop*, acts as follows. It evaluates the Boolean expression following the *while*, which is
the head of the loop, and, if it evaluates to true, the execution continues with the body of
the loop. After the body of the loop has terminated, the head of the loop is evaluated again.
The *while statement* terminates when the head of the loop evaluates to false. Of course, for
proving statements about programs this informal explanation is not enough. That’s why we
turn to a more rigorous description of the behaviour of programs. We need the notion of a
state:

Definition 3.Let be a function. Thensis called a state. The set of states is denoted by . If we are interested in the values assigned to the variables , bys, then we write , provided , .

In effect, the while program is a function manipulating states. We start from the initial state, and to every execution of a component of the program a state is attached. When the program terminates, we obtain the result of the execution by reading the values assigned to the variables of the program by the final state, which is the state attached to the program at the time of termination. We can make precise these notions as follows. We introduce a more general form of a transition system than needed for our present purposes, since we will be able to make use of this definition even in the subsequent parts of the course material.

Definition 4.A pair labelled transition system (LTS), if for every . If , then we callpthe source,qthe target, and we say thatqis a derivative ofpundera. In notation: . We use the notation , if . In case of , we let . We write .

We define the operational semantics of a program as a transition system. The definition is
compositional: knowing the transitions for the subprograms of the program we can determine the
behaviour of the program itself. Beforehand, we have to define the meaning of the arithmetical and
Boolean expressions, respectively. We assume an interpretation is given,
where is a mapping assigning concrete values to constants and functions and predicate symbols
appearing in arithmetical expressions. Then the truth values of Boolean expressions are obtained in the
usual way. As an abuse of notation, we denote the values assigned by to the constant *c*,
function symbol *f * by and instead of and
, respectively. If *B* is true in the model with respect to an interpretation *s*, we
write , or . If the states are not
interesting for our treatment, we may omit them. Moreover, for a Boolean expression *B*, let
. Thus identifies a
subset of .

In the definition below let be states, *B* be a Boolean expression and
be programs, respectively. The elements of the transition system belonging to
a program *C* are elements of , where are
the subprograms of *C*. We denote by . The transitions
are defined as follows:

Definition 6.A transition sequence

starting from

sis a computation if it is infinite or cannot be extended any further. A computation is terminating if its last configuration is an element of .Ccan diverge fromsif there is a diverging computation starting with .

Example 7.LetCbe the program of Example 2. Let , and otherwise. For the moment, let us denotesby a triple representing the values assigned toX,YandZ, respectively. Then

where is

Cwith the first assignment omitted, and is the body of the while loop inC.

Lemma 10.LetCbe a while program, assumesand are two states such that , ifXoccurs inC. Then terminates iff terminates, and, in this case, iff for every state .

Definition 11.The operational semantics or the meaning of the while program in the operational way is defined as follows. LetCbe a while program, then the meaning ofCin the operational way is the set of pairs

An alternative approach to the operational semantics is to construct a set of pairs as the operational semantics
of a program in a direct way (cf. [3]). As before, let .
Then , where is the set
of subsets of *A*, is defined as follows. In the definition below, let , where *s* is a state
and *E* is an arithmetical expression, denote the state which is identical to *s* except for the value at *X*, for
which .

As an example let us consider the following simple program.

Intuitively, the program terminates for every , and when it terminates the value
of *Y * equals the starting value of *X*. Let *C* denote the whole program, be the while loop and
let stand for the body of the loop. Then:

From the set of pairs we can extract a computation sequence for any given state *s*. For
example, let , assume all the other values of *s* are zero. In the example below we
denote *s* by its *X* and *Y * values. Then

is a
computation for *C* with .

Without proof we state the equivalence of the two approaches. In the theorem below, let denote the reflexive and transitive closure of .