Hwy-w
‘o 4

Pglnnﬂt!

uni. m: Im-

ri'n-dr“

3\~‘y;«x
l'l

‘...x-,..ys.;

 

 

 

 

 

 

IIIIUIHIHIWI.[ﬂlﬂijllwlllﬂllzllﬂllﬂllllll

___

LIBRARY
Michigan state
University

 

 

 

 

This is to certify that the

dissertation entitled

On the Formal Specification of Recursive Functions

presented by

Maureen Green Galsterer

has been accepted towards fulﬁllment
of the requirements for

Ph.D. Computer Science

degree in

 

 

 

 

MS U is an Affirmative Action/Equal Opportunity Institution 0-12771

”Momnmyw record.

PLACE ill RETURN BOX to remove
To AVOID Fines return on or befor- dd. duo.

 

 

 

 

 

 

 

 

 

On the Formal Speciﬁcation of Recursive

Functions

By

Maureen Green Galsterer

A DISSERTATION

Submitted to
Michigan State University
in partial fulﬁllment of the requirements

for the degree of

DOCTOR OF PHILOSOPHY

Department of Computer Science

1995

ABSTRACT

On the Formal Speciﬁcation of Recursive

Functions
By

Maureen Green Galsterer

Current predicate transformer methods for proving program correctness deal with
bounded loop programs, but these compute only a small fraction of the functions we
deal with. We introduce a proof of correctness method that works for bounded, un-
bounded, and nonterminating loop programs. We develop a mathematical foundation
that allows us to view programs as computational sequences. Using this foundation,
we deﬁne iteration as a recurrence relation between predicate transformers, and we
present a predicate transformer that can be used in the recurrence relation. Given
this basis, we present an inductive method that can be used to prove the correctness
of programs computing primitive, total, and partial recursive functions. We demon-
strate the use of our method on example programs that compute functions from each

class.

Copyright © by

Maureen Green Galsterer

1995

ACKNOWLEDGMENTS

It is customary in these things to acknowledge and thank the individuals who, by
their commitment or love, have given more of themselves than was expected to help
in this accomplishment.

First and foremost, I give thanks and all the glory to my Savior Jesus Christ,
whom I serve every day as Lord.

Second, my family: To my husband John who, while he paid with money, paid
with something much more valuable as well...his time; To my sons John and Jeff who
supported me in a very crucial time in their lives by understanding my absences from
home, who have disciplined themselves to become men that this mother is very proud
of, and have kept me current with the styles so I wouldn’t look like a geek; To my
parents Robert and Irene Green...I’ve kept my family name all these years just to
honor you.

Third, to my advisor, Dr. John G. Geske. You are a gentleman and a scholar.
Your direction and guidance was crucial. But even more important (and something
only other women in academia will understand) you accepted me as a gentlewoman
and a scholar. I cannot pay you high enough tribute, so I’ll just say: Thank you,
and I hope we’ll be friends forever. I also want to thank my committee members, Dr.
Betty H.C. Cheng and Dr. Abdol H. Esfahanian, for their support.

Fourth to my pastors: Rev. Judith K. Shepherd, and Rev. Jud Silveus. Thank
you for the times you’ve prayed with me to see this through, and even more for all
the times you’ve sought God on my behalf that I don’t even know about. I promise
you I’ll use this degree to build the Kingdom.

Fifth to my sisters and brothers in Christ at MSU: Barb Birchler, Barb Czerny,
Dr. Jon Englesma, Sally Howden, Ron Sass, and Dr. Steve Walsh...You’ve all been
bright points of encouragement and comfort. To you who have graduated, God Speed!
To you who will follow me, Take Heart! If 'we can do all things through Christ, you
can certainly trust Him to complete your research.

Finally, to my very best friend in Computer Science, Dr. Steve Turner...I love
you, Steve...acklPhphhpffttt!

iv

TABLE OF CONTENTS

LIST OF FIGURES

vii
1 Introduction 1
1.1 Motivation for the Research ....................... 2
1.1.1 Statement of the Problem .................... 3
1.2 Overview of the Solution ......................... 4
1.3 Organization of the Thesis ........................ 8
2 Mathematical Preliminaries and Definitions
2.1 Relations ..................................
2.1.1 Deﬁnitions .............................
2.1.2 Operations ......... . .................... 10
2.2 PrOperties of Relations .......................... 11
2.2.1 Ordering Properties ........................ 11
2.2.2 Lattices .............................. 12
2.2.3 Measuring the Information Contained in a Relation ...... 12
2.3 Functions ................................. 13
2.4 Assertions as Approximations ...................... l4
3 Previous Work 15
4 Semantics of A Language 26
4.1 Syntax of the Language ......................... 27
4.2 Semantics of the Language ........................ 29
4.2.1 The Denotational Semantics of the Language .......... 29
4.2.2 The Operational Semantics of the Language .......... 35
4.2.3 Semantic Equivalence . . .. .................... 44
5 Mathematical Foundation for Reasoning About Nonterminating
Computations 48
5.1 The Semi-Lattice of Computations ................... 52

5.2 Fixed Points ................. . ...............
5.2.1 Interpretation of Fixed Points ..................
5.3 Theory of Fixed Points ..........................
5.3.1 Monotonic Functions .......................
5.3.2 Properties of Monotonic Functions ...............
5.3.3 Least Upper Bound ........................
5.3.4 “;” When Viewed As A Functional Is Continuous .......
5.3.5 Fixed Points of the Functional 1' .................
6 The wpw Predicate Transformer
6.1 Macros ...................................
6.1.1 Syntax of Macros .........................
6.1.2 Use of Macro Names .......................
6.2 The wpw Predicate Transformer .....................
6.2.1 Formal Deﬁnition of an Unbounded Loop ............
6.2.2 Incremental Progress .......................
6.2.3 Properties 9f the wpw Predicate Transformer ..........
6.2.4 Relationship Between I, R’, and R. ...............
7 Application of the wpw Predicate ’h'ansformer
7.1 Description of the Method ........................
7.2 Examples .................................
7.2.1 Proof of Correctness of a Total Recursive Function ......
7.2.2 Proof of Correctness of a Partial Recursive Function ......
7.2.3 Proof of Correctness of a Nonterminating Computation . . . .
7.3 Annotated Program Code for Examples .................
8 Conclusion
8.1 Future Work ...... ' ..........................
BIBLIOGRAPHY

55
56
61
61
62
64
66
72

74
75
77
78
79
81
82
84
87

89
89
91
91
98
102
108

113
114

117

4.1
4.2
4.3

7.1
7.2
7.3
7.4
7.5
7.6

LIST OF FIGURES

Syntax of the Language. ....................... 28
Example of the denotational deﬁnition of whiledo od ...... 35
Random Access Machine (RAM). ................. 37
Example 1, A Total Recursive Function. ............. 108
Major Macro for Example 1. .................. ‘ . . 109
Minor Macro for Example 1. .................... 110
Example 3, A Nonterminating Program. ............. 110
Example 3, The Macro divides. ................... 111
Example 3, The Macro Prime. ................... 112

CHAPTER 1

Introduction

This research deals with partial recursive functions. Specifically, we are interested in
reasoning about programs that use unbounded iteration or general recursion to com-
pute partial functions. A large body of research already exists on reasoning about
terminating programs that stems from Dijkstra’s weakest precondition (wp) predicate
transformer [1]. All of this work deals with primitive recursive functions since termi-
nation must be guaranteed with an a priori upper bound. This restriction was based
not only on Dijkstra’s firm belief that all meaningful programs terminate [2], but for
simplicity, because it allowed him to define iteration as a recurrence relation between
predicates [1].

We will show that a mathematical foundation for reasoning about unbounded and
nonterminating programs exists. Based on this foundation, we will define iteration as
a recurrence relation between predicate transformers. We will define a new predicate
transformer that can be used with our mathematical foundation to prove the correct-
ness of programs computing primitive recursive, total recursive, and partial recursive

functions.

1.1 Motivation for the Research

While many programs have a priori time bounds, there are important programs that
do not, such as those that manipulate sequential ﬁles. These programs are expected to
terminate, but they require unbounded loops. It is also common to use programs that
are not designed to terminate at all, such as operating system daemons and networking
processes. A priori time bounds are meaningless for programs using unbounded loops
to compute total functions, and for programs using nonterminating loops to compute
partial functions.

Program speciﬁcation techniques based on predicate logic use assertions to pre-
cisely deﬁne the condition of a program’s variables before and after a program state-
ment executes. These assertions are called preconditions and postconditions, respec-
tively. The weakest precondition (wp) calculus of Dijkstra is one of the most widely
known of these methods that use predicate transformers. Dijkstra’s predicate trans-
former maps a program statement and its postcondition to a predicate describing the
set of all initial states from which the statement can execute leaving its postcondition
true. Dijkstra envisioned his method as a top-down design tool. The wp calculus is
a total correctness method, i.e., it is only applied to statements that are guaranteed
to terminate. This guarantee ensures that the postcondition of any statement can be
reached and veriﬁed. This assurance of always being able to reach a postcondition
allowed Dijkstra to deﬁne the semantics of simple iteration as a recurrence relation
between predicates [l], keeping it in the realm of ﬁrst order logic, but it also restricts
the utility of the method: The only recursions that can be proven to terminate a pri-
ori are direct (tail) recursions. To encompass all the computable functions we need
general recursion.

In the classes characterized by general recursion it is not possible to predict when,

or if, a computation will terminate. Any method for reasoning about correctness in

these classes cannot make termination an issue in its proofs, therefore our solution
does not depend on termination. We can deal with termination if it does occur, but
we concentrate on correctness at each step of a computation not just at its end. So,
whether a computation step leads to a ﬁnal state or not we can verify its correctness.

Proof of correct design was Hoare’s intention when he proposed predicate logic
with equality as a means for reasoning about programs [3]. Hoare viewed a program
as a logical model and used predicate logic to show that as a sequence of statements
it was a tautology. Dijkstra’s main disagreement with Hoare was that programs are
not recipes for computing, but are agents that when run on a computer can effect a
computation, i.e., programs execute [2]. Dijkstra contended that proving a computing
method is correct is only half of a proof of correctness. In addition, he insisted that

showing termination with correct results was necessary.

1.1.1 Statement of the Problem

Proof of correctness methods that rely on the wp calculus are only suited to pro-
grams computing functions in the primitive recursive class because the top predicate
transformer is too severely structured to accomodate the more powerful classes of
functions. The wp predicate transformer takes a program statement and its postcon-
dition as its arguments. Termination must be guaranteed a priori to ensure that the
postcondition can be reached and veriﬁed, and the primitive recursive functions are
the only class of functions for which a priori time bounds exist. A priori time bounds
are meaningless in the classes characterized by general recursion, but limiting proof of
correctness methods to the small class where the wp calculus works limits our ability
to verify the correctness of programs that we use regularly, i.e., all programs that use
general recursion or unbounded looping to compute.

We will show that a mathematical foundation for reasoning about unbounded and

nonterminating programs exists. Based on this foundation, we will deﬁne iteration as

a recurrence relation between predicate transformers. We will deﬁne a new predicate
transformer that can be used with our mathematical foundation to prove the correct-
ness of programs computing primitive recursive, total recursive, and partial recursive

functions.

1.2 Overview of the Solution

Our research carries Dijkstra’s statement that “programs execute” to its logical con-
clusion. Dijkstra ignored actual execution in favor of its beginning and its end,
concentrating on the predicate logic assertions he could make about the initial and
ﬁnal states of a computation. We use the results of each stage of a program’s exe~
cution and verify correctness from program state to program state; we use the entire
sequence of a computation. We will show that there is a logical foundation for rea-
soning about unbounded and nonterminating computations. We will provide the
mathematical foundation for reasoning about such computations, and we will give a
concrete method that can be used in proofs of correctness for programs using loops
with and without a priori upper bounds. Our method is based on a deﬁnition of
iteration as a recurrence relation between predicate transformers, i.e., functions from
predicate transformers to predicate transformers. Using our predicate transformer,
we will show with examples that we can reason about nonterminating and terminating
programs.

Using computational sequences raises technical issues because a consistent founda-
tion must be carefully laid, and it raises theoretical issues because proofs of correctness
are based on second order logic. We quantify over predicates, so we deﬁne iteration
as a recurrence relation between predicate transformers. While this adds complexity
to our foundation because we must reason in second order logic, it extends our abil-

ity to prove correctness of total and partial recursive functions, as well as primitive

recursive functions.

Technically, when we deal with a computational sequence we must ﬁrst deﬁne the
environment that generates the sequence. Because the sequence represents a “run”
of the program we must have a machine to execute it and a language to express it.
The machine we deﬁne must be sufficiently general so as to represent the class of
machines available in the real world, so we use the Random Access Machine of Meyer
and Ritchie [4]. The language we need must be simple but must also form a complete
programming system with the machine. Our language is similar to Dijkstra’s except
that we replace his bounded D0 loop with an unbounded WH I LEDO.

The semantics of our language are critical because we must be able to express
the meaning of terminating and nonterminating computational sequences with de-
ﬁned results (sequences that represent the computations of total and deﬁned partial
functions, respectively). We must also be able to express the meaning of nonter-
minating computational sequences with undeﬁned results (sequences that represent
partial functions undeﬁned on their input). We provide a formal denotational seman-
tics for our language that admits an undeﬁned element to handle partial functions
in a fashion similar to de Bakker [5] and Nelson [6]. The operational semantics of
our language is the foundation for our computational sequences. The sequences must
be sufﬁciently abstract so as not to make the method dependent on any particular
implementation but they must make sense given the environment we have deﬁned.
We must also guarantee that the information represented by the variable valuations
in each element of the sequence logically succeeds that of the element before it, that
it represents a useful value (i.e., it was derived as a result of a valid computation step
and not as a side effect), and that it represents a true approximation to the limit of
the sequence itself.

To ensure all this we differentiate operationally between the function computed

by a program and the operational meaning of a program. The function computed

by a program is the value of the variables in a ﬁnal state or an undeﬁned value if
the program does not terminate. This parallels the usage of the valuation function
in the denotational semantics deﬁnition. The operational meaning of a program, or
what it means to compute on our machine, is the computational sequence returned
by our operational semantic function. Our function allows us to express formally the
notion that computers actually execute programs. Making this distinction allows us
to prove that the operational semantics and denotational semantics are equivalent,
and to show that a computation produces more information than can be expressed
by its initial state/ﬁnal state pair.

Deﬁning the meaning of a program to be a computational sequence gives us a series
of program states to examine. The equivalence of our denotational and operational
semantics ensures that our programs will not display side effects. This is not sufﬁcient
to guarantee that each state of a computation logically succeeds that of the element
before it or that each successive state is a better approximation to the limit of the
computation than its predecessor. For these last two requirements we must impose
a well-ordered structure on our sequences; we must guarantee that in all cases our
sequences are chains. We do this by organizing our state space as a complete lattice,
and then proving that our program statements are monotonic (this ensures that each
state is a valid extension of its predecessor so no unanticipated results will creep into
our sequences) and that both our program statements and the higher order function
used by our Operational semantics to build our sequences are both monotonic and
continuous (this ensures that each element of a chain is a true approximation to the
limit of the computation).

Kleene’s First Recursion Theorem holds that every computational chain has a
least upper bound [7]. We can use this fact to induct over the elements of our compu-
tational chains in our proofs of correctness. We can step from predicate transformer

to predicate transformer to verify that each element of the chain is an approximation

to the least upper bound. For terminating computations the least upper bound is the
ﬁnal state. It is deﬁned by a logical assertion that fulﬁlls the program’s speciﬁcation
when the computation is correct. For nonterminating computations we use the least
upper bound of each subsequence in the chain, and view the logical descriptions of
these elements as approximations to the predicate that deﬁnes the limit of the com-
putation itself. To do this we have recognized that for every looping construct there
exists a logical assertion that is an approximation to a deﬁned loop’s speciﬁcation.
If termination occurs the conjunction of the loop invariant, this approximation, and
termination implies the postcondition. If termination has not occurred, the truth of
the conjunction of the loop invariant and this approximation proves the correctness
of the current iteration of the loop.

The theoretical issue that arises from the use of computational chains to prove
correctness is that the predicate transformer we deﬁne provides a mapping between
the logical assertions that deﬁne each element of the chain, not just for the initial
and ﬁnal states as the wp predicate transformer does. For noniterative commands the
operator behaves like the wp predicate transformer we are accustomed to because such
commands are atomic (they have an initial state and a ﬁnal state only). For iterative
commands the operator deﬁnes a recurrence relation between predicate transformers
because it maps the predicate transformer of one state to the predicate transformer
of another. We will show in Chapter 6, Section 6.2.3 that the predicate transformer
we deﬁne has all of the properties that the wp predicate transformer has.

We show that, given the syntax of unbounded looping and semantics to express
the results of partial functions, a logical basis for reasoning about general recursive
computations exists, and can be extended into a method for proving that they are

correct.

1.3 Organization of the Thesis

In Chapter 2 we present mathematical deﬁnitions and preliminaries that we use. In
Chapter 3 we review the related work that led to the development of the top calculus.
In Chapter 4 we deﬁne our machine model and its language, give our denotational
and operational semantics, deﬁne formally the distinction we make between the oper-
ational value of a program and the operational meaning of a program, and prove that
our denotational and operational semantics are equivalent. In Chapter 5 we present
the complete lattice induced by our operational semantics and prove the properties of
monotonicity and continuity for our program statements and the higher order func-
tional we use to construct computational chains. In Chapter 6 we introduce our
predicate transformer with the Incremental Progress Theorem, and give its proper-
ties. We show how we can use this theorem in our inductive veriﬁcation method.
In Chapter 7 we provide examples of the method used on a total recursive function,
a partial recursive function we expect to terminate, and a partial recursive function
that is nonterminating by design. In Chapter 8 we discuss several areas of application

for this research as future work.

CHAPTER 2

Mathematical Preliminaries and

Deﬁnitions

2.1 Relations

2.1.1 Deﬁnitions

Like Dijkstra [1], Hehner [8], and Nelson [6] we view commands as binary relations
on the set of program states. This state space is composed of machine vectors of
length n, where n is the total number of variables used by a program. Thus a
program command maps one program state (valuation of the machine vector before
the command executes) to another state (valuation of the machine vector after the
command executes).

A command, C, on the set I‘ of program states is a subset of I‘ x I‘. When we
represent individual elements of I‘ we write 7 to mean 7(< 21,rg,. . .,:r,, >), the
valuation of the machine vector. Let (7,7’) 6 C; 7 is an argument in C and 7’ is
an image in C. The domain of relation C is the set of arguments of C; formally,
dom(C) = {7|37’ : (7,7’) 6 C}. The range of relation C is the set of images of C;
formally. m9(0) = {7137: (7.7’) 6 C}-

10

The identity relation idp = {(7,7’)I7 E I‘ and 7’ = 7], and the empty relation
0 = {} are constant relations.

A relational is a relation on the set of binary relations (i.e., commands) on I‘.

2.1.2 Operations

Since commands are binary relations, we can obtain other relations using union,
intersection, and difference on these binary relations. In addition to these operations,

we deﬁne the following operations on relations.

0 Inverse: The inverse of command C is the relation denoted by C"1 and equal

to {(7,7’)I(7’,7) 6 C}-

. Composition: Let C1 and 02 be two commands on I‘. The composition of C;

with C2 is the relation denoted by C1C2 and deﬁned by

0102 = {(7.7')|37” = (7.7”) 6 Cl A (7”.7’) 6 02}

o Iterated Composition: Let C be a command on I‘. The i“ iterated compo-
sition of C, for i Z 0, is the relation denoted by Ci and deﬁned by
Co = idp,
C’ = Cf‘lC, for i 2 1.
Note that for all i 2 1, dom(C’) Q dom(C).

o 'D‘ansitive closure: Let C be a relation on I‘. The transitive closure of C is

the relation denoted by 0"”, and deﬁned by

0* ={(7,7’)|3i21=(7,7’)€ C’}-

11

o Reﬂexive transitive closure: The reﬂexive transitive closure of command C

on I‘ is the relation denoted by C“ and is equal to idr U 0".

0 Image set: The image set of 7 E I‘ of command C is the set denoted by 7.0
and deﬁned by

7.0 = {7’l(7,7’) 6 C}.
A command’s speciﬁcation deﬁnes its image set.
To extend this notation, if I" Q I‘ then I" .C = U761» 7.C. We deﬁne 0.7 and

C.I" as 7.C'1 and I".C'l.

o Nucleus: The nucleus of command C is the relation
N (C ) = CC '1.

This relation contains the state pair (7,7’) if and only if 7 and 7' map to the

same state 7” under C.

The set of elements that make up the nucleus can be deﬁned by the weakest

precondition of a command and its speciﬁcation.

2.2 Properties of Relations

2.2.1 Ordering Properties

Let C be a relation on I‘. C is said to be reﬂexive if and only if idr Q C. C is said
to be transitive if and only if C2 Q C. C is said to be antisymmetric if and only if
C n G-1 g idp.

C is said to be a partial ordering if and only if it is reﬂexive, antisymmetric, and

transitive.

12

2.2.2 Lattices

Let C be a partial ordering relation on I", and let I" be a subset of I‘. An element 7
of I" is said to be C — maximal in I" if and only if there is no 7’ other than 7 in I"
such that (7,7’) 6 C.

Let C be a partial ordering relation on I‘, and let I" be a subset of I‘. An element
‘7 E I" is said to be C — minimal if and only if there is no 7’ other than 7 in I" such
that (7,7) 6 0.

Let 7 and 7’ be two elements of P and let C be a partial ordering on I‘. The set
of upper-bounds of 7 and 7’ is denoted by ub(7,7’) and deﬁned as

ubhm’) = (7-0) 0 (7'0)-

The set of lower-bounds of 7 and 7’ is denoted by lb(7,7’) and deﬁned as

lb(mv’) = (0-7) 0 (07’)-

Let 7 and 7’ be two elements of P, and let C be a partial ordering relation on I‘. A
C — least upper bound of 7 and 7’, if it exists, is a C-minimal element of ub(7,7’),
denoted lub(7, 7’). A C — greatest lower bound of 7 and 7’, if it exists, is a C-maximal
element of lb(7,7’), denoted glb(7, 7').

Let C be a partial ordering on I‘. We say that C is a lattice if and only if every

pair (7,7’) 6 I‘ has a greatest lower bound and a least upper bound.

2.2.3 Measuring the Information Contained in a Relation

Let C and C’ be two relations on I‘. We say that C is more-deﬁned than C' (or C’ is
less deﬁned than C) if and only if

1. dom(C’) Q dom(C),

13

2. V7 6 dom(C'), 7.0 Q 7.C’

Example 2.1 Suppose there are two observers watching a deterministic input/output
process. The process draws inputs from the set {a,b, c, d} and has outputs in the set
{0, 1,2, 3,4}. Suppose C and C’ are the reports of the two observers as they view the
process. Let

C = {(0.0),(5: 1),(C. 2M", 3)}

C" = {(0,0), (0, 1), (0,2), (5, 1), (b, 2), (b, 3), (c, 2), (c, 3), (c, 4)}
Report C is more-deﬁned than report C’ because the observer who gives it reports about
more inputs than the observer who gives report C'. This is what condition 1 means.
Report C is more-deﬁned than report C’ for the additional reason that the observer
who gives it is more precise in his assignment of the inputs both have recorded. This

is what condition 2 means.

2.3 Functions

Functions can be viewed as relations that map elements of the domain to unique
elements of the range. For a function f and domain element x, r. f is the singleton
set denoted f (at)

We use a function name f is three distinct ways. First, f denotes a set of pairs
such that for any value a: there is at most one pair (2:, y). Second, a: f y holds if (1:, y)
is in f. Third, f(a:) is the value associated with 3, that is, (:c, f(:r)) is a member of
the function (relation) f. Notice that the usage a: f y denotes a predicate.

We deﬁne functions as restricted forms of relations because then the theory and
terminology for relations carries over to functions. Thus we know what image set and
iterated composition of a function mean. Since a function is a relation we know what
the inverse f"1 of function f is. f'1 is a function when f is invertible, i.e., when f

is one-to—one and onto.

14

Nucleus. The nucleus of a function f is

N(f) = ff";

which can also be written

N(f) = {(3,1')|f(1=)= f($')}-

2.4 Assertions as Approximations

Each state in a computational chain represents an approximation to the limit of the
computation. These states can be described by logical assertions, and each logical
assertion is approximated by its predecessors. We represent predicates with capital
letters of the roman alphabet: A, B, . . . , P, Q, R, . . . , Z. When we represent the ap-
proximation to a particular predicate, we append a prime (I) to the letter we use for
that predicate. For example, R’ approximates R.
This convention is used when we specify a looping construct. For example:
{Precondition}
{Invariant}
while 9 do
5;
{R’ : Assertion about 5' } this assertion approximates R
od
{R : Assertion about whiledo . . .od}

CHAPTER 3

Previous Work

The application of mathematical techniques to prove the correctness of a program was
proposed in 1969 by C. A. R. Hoare [3]. Hoare’s intention was to provide a logical basis
for proofs of the properties of a program. His primary concern was to demonstrate
that a given program is able to carry out its intended function. Hoare considered
the semantics of computation without addressing the implementation issues. Since
Hoare was interested in the axiomatic semantics his interest was primarily model
theoretic. Hoare made a distinction between a program and the implementation of
the program, sidestepping the issue of termination of a computation. Hoare’s work
deﬁned the notion of partial correctness, that is, programs should guarantee that they
will not produce an incorrect answer. This gave the ﬁrst half of the requirements used
today to prove that programs are correct.

Hoare speciﬁed the intended function of a program by making general assertions
about the values which the relevant variables will take after execution. The assertions
are not speciﬁc about particular values each variable will have, but rather specify
certain general properties of the values and the relationships that hold between them.
Hoare’s notation is predicate logic.

Hoare recognized that the validity of the results of a program will often depend on

the values taken by the variables before the program is initiated. He used statements

15

16

in predicate logic to specify the “initial preconditions” of successful use and also
to describe the results obtained on termination. To state the required connection
between a precondition (P), a program (Q), and a description of the result of its

execution (R), Hoare introduced the notation

called a “Hoare triple.” The interpretation of this statement is: If the assertion P
is true before initiation of the program Q, then the assertion R will be true on its
completion.

Hoare deﬁnes one axiom schema to specify the assignment statement, and three
rules: one to specify the decision construct, one for composition of sequential state-
ments, and one to cover iteration.

Building on Hoare’s work in the mid 70’s, Dijkstra [2], [1] observed that computer
programs were not just static sequences of statements, but when programmed on a
computer became dynamic entities. Where Hoare looked at programs as sets of state-
ments to be veriﬁed with predicate logic, Dijkstra was concerned with the outcome
of statements after their execution. Dijkstra insisted that the only programs we are
interested in are the ones that terminate and accomplish what we want [2]. Dijkstra’s
work deﬁned the notion of total correctness: partial correctness (provided by Hoare)
and termination (insisted upon by Dijkstra).

Dijkstra’s weakest-precondition calculus is probably one of the most familiar of the
speciﬁcation methods that use predicate transformers to deal with program state-
ments and control structures. Whereas Hoare was interested in correctness of the
method, Dijkstra was interested in the correctness of the method and correctness
in the implementation of the method. Dijkstra recognized the utility of Hoare’s

work in specifying the preconditions and results of executing a statement (which he

17

called “postconditions”), so his method used predicate logic to specify the pre- and
post-conditions of the four basic programming constructs: assignment, sequencing,
decision, and repetition.

Unlike Hoare, Dijkstra was very interested in what actually happens during exe-
cution of one of these basic programming statements, so he introduced notation that
could capture the meaning of “implementing a statement.” Dijkstra deﬁnes the se-
mantics of a programming construct in terms of weakest preconditions (wp). In this
notation, {Q}S {R} means that execution of statement (program) 5 begun in any
state satisfying predicate Q will terminate in a state satisfying predicate R. The
different syntax used to present this assertion (or “Dijkstra triple”) is not accidental:
Dijkstra strengthened the meaning of the assertion from correctness (Hoare’s mean-
ing) to correctness and termination. In this context, Q is called the precondition and
R is called the postcondition of a statement 5'. The weakest precondition of S with
respect to R, wp(S, R), represents the set of all states such that execution begun
in any one of them will terminate with R true. The notation {Q}S {R} is another
notation for

Q => wp(5. R),

which is a statement in predicate calculus that is either true or false in any state.
The syntax of the four basic programming statements is as follows. An assignment

statement is denoted by “r := E” where a: is any variable and E is any expression of

the appropriate type. Sequencing is denoted by “.S' 1; 52,” ﬁrst execute S 1 and then

execute 52. The decision construct, IF is denoted by

IfB] ‘4 SL1” ... ”En —+ SLnﬁ

where the B,- are Boolean expressions called “guards,” and the SL; are statements

(or statement lists) called “alternatives.” To execute an IF statement, execute any

18

one of the alternatives whose guard is true.

The repetitive construct, D0, denoted

(1031 —t SL1” ... [18,; —t SLnOd

is executed as follows: repeatedly, as long as some guard B,- is true, execute any
one of the alternatives whose guard is true. The repetitive construct only terminates
in a state in which none of the guards is true. When the repetitive construct has
terminated properly, we know that all of its guards are false.

This deﬁnition seems appropriate for unbounded loops but it lacks the mechanism
for proving termination that Dijkstra required. Dijkstra supplied this mechanism by
building the requirement of termination into his semantic deﬁnition of the above
syntax. The semantic meaning of the construct is: For at most I: iterations, execute
any one of the guards that is true. Since the repetitive construct can only terminate
when none of the guards is true, the a priori upper bound k is used to design the
guards so that this condition is ensured.

Dijkstra used predicates to deﬁne sets of initial and ﬁnal states the way Hoare
did [3]. The main difference in their methods is that while Hoare introduced sufﬁcient
preconditions such that the mechanisms will not produce the wrong result (but may
fail to terminate), Dijkstra introduced necessary and sufﬁcient, i.e., “weakest” pre-
conditions, such that the mechanisms are guaranteed to produce the right result. The
semantic tool he used was predicate transformers, which specify, for a given statement
5 (which he called a “mechanism”) and postcondition R, the weakest precondition
guaranteeing that S' will establish R.

The weakest precondition (semantic) equations for the four basic programming

constructs are:

1. Assignment: wp(“x := e”,R) = R”.

e

19

Where Rf indicates that e is deﬁned on the domain of R and we replace every

occurrence ofa: in R with e.
2. Sequential composition: wp(“S 1;S'2”,R) = wp(“S 1”,wp(“S2”,R)).

3. IF: wp(IF, R) = (BB and (Vi : 1 S i S n: B.-=> wp(S'L;,R)).
Where BB is a Boolean expression that ensures there exists a true guard, and
the second term requires that each guarded list eligible for execution will lead

to an acceptable ﬁnal state.

4. D0: wp(DO, R) = (3k : lc 2 0 : Hk(R)).
Where Hk(R) is the weakest precondition guaranteeing proper termination after

at most I: selections of a guarded list, leaving the system in a ﬁnal state satisfying

R. Hk(R) is deﬁned by cases:

. [10(3): RA-a(3j:ISan:B,-)

O Hk(R) = wp(IF,Hk-1(R))VHo(R)

The semantics of Dijkstra’s looping construct are deﬁned using tail recursion, with
the predicates describing the state of the computation at each level of recursion.
Dijkstra had to show that his recursions formed a ﬁnite decreasing chain to ensure
termination of his looping constructs. This is the basis for the deﬁnition of compu-
tational progress which is measured as a decrease in an integer-valued function that
is bounded from below. Computational progress is perfectly suited for functions in
the primitive recursive class because the primitive recursive functions are deﬁned to
be those functions that are computable by bounded loop programs [9]. Dijkstra intro-
duced his ﬁnite integer bound function as a free variable that must be manipulated
in each proof of a repetitive construct.

Hehner [8] challenged the utility of the repetitive DO statement and offered the

notion of recursive reﬁnement for specifying looping statements. He argued that the

20

semantics of Dijkstra’s DO were the most complicated part of Dijkstra’s language,
because of the requirement of demonstrating a ﬁnite decreasing chain of predicates by
manipulating another variable in the semantic equations. Hehner reasoned that since
Dijkstra was deﬁning the semantics of the looping construct with recursion, it would
be easier to throw away the looping construct entirely and just use recursion. He
proposed replacing Dijkstra’s looping construct with recursive reﬁnement, a technique
that uses divide-and-conquer to repeatedly deﬁne a repetitive problem in ﬁner and
ﬁner detail until the base deﬁnition of the problem is reached. At this point, the
speciﬁcation is composed entirely of sequential steps which can each be speciﬁed
individually without regard to termination, since it is assumed that each sequential
action terminates. In this sense, reﬁnement eliminates loops.

In eliminating the looping construct, Hehner eliminated the need to carry along
and manipulate an explicit counter in his semantic equations. This removed the
added complexity of demonstrating that the recursive computation behaved as a. ﬁnite
decreasing chain. It is important to note that Hehner explicitly speciﬁed tail recursion,
which was appropriate because his motivation was to replace Dijkstra’s bounded
loops. Limiting the method to tail recursion had two consequences: ﬁrst, the method
could only be used to specify primitive recursive functions; second, the method had to
be designed to demonstrate termination. Hehner addressed the second consequence
with the same mechanism Dijkstra used: computational progress, incorporating the
requirement to show computational progress into the reﬁnement process.

The recursive reﬁnement technique involves the invention of a name for a portion
of a program, using the name in place of the program portion, and specifying the text
of the program portion elsewhere. Hehner referred to the use of a name in place of
some statements as a “call,” and refered to the speciﬁcation of the statements as a
“reﬁnement.” A call is a name enclosed in quotation marks; a reﬁnement consists of

the quoted name, followed by a colon, followed by a statement list (SL):

21

“name”:SL
Hehner’s “call” gives no semantic equation; a call is given meaning by the details of
its reﬁnement. A reﬁnement gives the equation: wp( “name”,R) = wp(S L, R).

Computational progress is the cornerstone of Dijkstra’s repetitive construct and
Hehner’s recursive reﬁnement because both methods rely on it in their proofs of
termination. In its most formal sense, computational progress refers to a theorem of
Dijkstra’s that shows how a loop invariant and a ﬁnite integer bound function can
be used to prove that a repetitive construct is totally correct, i.e., is partially correct
and terminates.

Informally, computational progress refers to the manipulation of a loop counter
to demonstrate that a repetitive construct will make progress towards termination.

In all of its manifestations, computational progress is an explicit reference to an
a priori upper bound on the number of iterations a loop must perform. Because of
this, every method that depends on computational progress is limited to programs
computing in the primitive recursive class of functions.

The primitive recursive class contains only a fraction of the functions we rely on
regularly. Consider this Pascal program segment

while not eof(dataﬁle) do

readln(dataﬁle, value);

This loop depends on the ﬁle variable reaching a particular condition independent of
a counter, and cannot be proven to meet its speciﬁcation using the wp calculus or
recursive reﬁnement. There are many such applications outside the primitive recursive
class: communicating processes, searching, Operating systems processes, networking
services, etc.

de Bakker addressed the problem of unbounded 100ps in 1980 [5]. He added an
unbounded looping construct to Dijkstra’s language and deﬁned a denotational se-

mantics to formally express the function computed by each statement. To accomodate

22

nonterminating loops he extended the state space of program variables to include an
undeﬁned element (J.), and called it “bottom” in keeping with Scott’s work on deno-
tational semantics [10]. Thus his program statements as functions could return either
a deﬁned value from the program’s state space of all variable valuations, or they could
return the value .L. de Bakker deﬁned an operational semantics that acted as a func-
tion, returning either a state whose variables had the valuation resulting from correct
execution of a statement, or in the case of a nonterminating statement, a state with
variables undeﬁned.

The availability of both an initial and a ﬁnal state for any execution of a statement
fulﬁlled the requirements of Di j kstra’s wp predicate transformer. However, de Bakker
did not redeﬁne the foundation of Dijkstra’s predicate transformer, so the predicate
logic meaning FALSE that deﬁned .1. violated one of the properties of Dijkstra’s
predicate transformers: wp(Statement, FALSE) = FALSE, i.e., statements can-
not lead to undeﬁned states.

Given the proper motivation this property of the wp predicate transformer can be
redeﬁned. In fact this was done subsequently by Nelson [6]. A more serious concern
that arose from de Bakker’s adherence to the initial state/ﬁnal state pair required
by the wp predicate transformer is that loops designed to be nonterminating, such
as operating system processes, require the postcondition FALSE by deﬁnition of his
denotational semantics, and his operational semantics was designed to return only
an undeﬁned state as well. The problem with this is that intuitively much more can
be said about nonterminating computations that are deﬁned on their input, but all
de Bakker could say, in the absence of intermediate states to analyze, was that the
loop did not terminate.

In 1984 Hehner worked brieﬂy at deﬁning program statements themselves as pred-

icates in an attempt to maintain the deﬁnition of iteration as a ﬁrst order recurrence

(a recurrence between predicates) [11]. Motivated by this, Nelson addressed the prob-

23

lem of recursively computed partial functions by generalizing the wp calculus [6]. In
Dijkstra’s world all loops terminate so they have descriptive predicate logic (i.e., not
FALSE) postconditions. This is the essence of his Law of the Excluded Miracle
(wp(Statement,FALSE) = FALSE). Nelson rejected this “law,” claiming that
since nonterminating recursions never reach a ﬁnal state they can be speciﬁed by the
predicate logic description FALSE, denoting the empty set. With the predicate logic
description FALSE for postcondition of a nonterminating computation Nelson had
both the set of initial states and the set of ﬁnal states (although it was empty) he
needed to satisfy the wp predicate transformer. However, the postcondition FALSE
is not helpful for verifying correctness, unless the computation is for a partial function
undeﬁned on its input, and since it is not even possible to identify these computations,
Nelson could certainly not predict them in advance.

Therefore, Nelson focused on the partial correctness conjunct of the wp predicate
transformer. This conjunct, the weakest liberal precondition (wlp) expresses that a
computation will not produce an incorrect answer, i.e., each stage is not wrong.
This is not equivalent to saying that each stage is “right,” because this stronger
statement requires termination of the whole in the wp model. Nelson deﬁned a
recursive computation as a sequence of approximations to the limit and used a pair
of predicates to specify each element of the sequence, making the mapping of the
predicate transformer a recursion between predicates. One predicate expressed what
the variables were not, and the other assured that the recursion would halt. He
showed that his work could be applied to direct recursion and implied that it could
be tailored to general recursion, although the assurance of halting only works if you
have a hand on the power switch in this case.

Nelson provided the mathematical foundation for extending the partial correct-

ness predicate transformer (wlp) into the classes represented by general recursion.

Nelson’s work relied on a limit theorem that required only monotonicity (not mono-

24

tonicity and continuity) because his computational model was based on recursion. A
general recursive computation can be modeled as a tree because the computation is
allowed to backtrack, or recover, from “dead ends.” Continuity limits the number of
dead ends that can be recovered from; it precludes unbounded nondeterminism. Nel-
son showed that as a computation progresses correctly monotonicity ensures that no
erroneous values are admitted into the set of states that represent the computation.
He showed that the wlp predicate transformer is an accurate map from the states in
the computation sequence to the initial states that allow them.

Because the wp predicate transformer only discusses initial and ﬁnal states Nel-
son’s generalization of it could not produce a method for verifying the sequence at
any intermediate stage. Additionally, his lack of continuity, coupled with the fact
that his predicates expressed the compliment of the actual computational sequence
precluded him from making assertions about individual states of the computation it-
self. The wlp predicate transformer only guarantees what a computation is not doing
(i.e., behaving incorrectly). We cannot use it of itself to say anything about what the
values in any stage actually are, because the wlp predicate transformer guarantees
correctness only upon termination.

Hesselink also worked with recursive computations [12]. He developed a language
that included procedure declarations that supported mutual recursion and gave its
semantics in terms of the wp calculus. He used the syntax of his procedure decla-
rations to reason in his semantic equations, but not in his program speciﬁcations as
we do. Reliance on the wp predicate transformer only allowed him to show partial
correctness in nonterminating computations. However, this is still more than Dijkstra
could do. Like Nelson, Hesselink showed that the wlp predicate transformer is valid
throughout a general recursive computation.

His result was stronger than Nelson’s because the version of the Knaster-Tarski

limit theorem he used allowed him to show that the Law of the Excluded Miracle

25

can be preserved while unlimited backtracking is supported. This work agreed with
Dijkstra and van Gasteren [13] that the restriction to continuity can be lifted in the
wp model. However, use of the wp model with its reliance on termination limited
Hesselink to the initial state/ ﬁnal state pair, so like Nelson, all he could say about a
nonterminating computation was that it would not be incorrect if it terminated.

We have highlighted the work that directly affected the mathematical foundation
of the current model of the wp calculus. Early pioneers in speciﬁcation and veriﬁcation
techniques were Floyd [14] who motivated Dijkstra with his work on ﬂow charts of
a program’s execution, Greif and Meyer [15], who gave a critique and tutorial on
Hoare’s work in 1981, Mills [16], who advocated the use of mathematical techniques to
describe programming objects and concepts as early as 1975, and van Emden [17] who
gave the semantics of predicate logic as a programming language in 1976. Cohen [18],
Dijkstra and Scholten [19], Conway and Cries [20], and Cries [21] have all worked
to develop the techniques of speciﬁcation and veriﬁcation using the wp calculus, and

have presented their work as text books.

CHAPTER 4

Semantics of A Language

One of the basic tenets of our research is that programs execute. Existing work is con-
cerned with the initial state/ ﬁnal state paradigm of the wp calculus, but we believe
that much more can be said about the execution of a program than an examination of
its initial state/ﬁnal state pair can show. This is particularly true of programs com-
puting partial functions because they may not terminate. We use the results of each
stage of a program’s execution and verify correctness from program state to program
state. We use the entire sequence of a computation, so whether a computation step
leads to a ﬁnal state or not we can verify that one execution of the statements that
comprise the step are correct.

In this chapter we deﬁne a necessary environment for our computational sequences.
First we give the syntax of a programming language so we will be able to record the
algorithms we use to compute partial functions. The semantics of our language are
critical because we must be able to express the meaning of terminating and nonter-
minating computational sequences with deﬁned results, and the meaning of nonter-
minating computational sequences with undeﬁned results. We provide a denotational
semantics that admits an undeﬁned element so we can express the value of a partial

function that is undeﬁned on its input. The operational semantics of our language

is the foundation for our computational sequences. To generate a computational se-

26

27

quence we need a machine. To accurately deﬁne the actions of the machine we provide
operational semantics. We deﬁne a machine because we expect our programs to exe—
cute, and we use our operational semantics to formalize the meaning of a program’s

execution.

4.1 Syntax of the Language

We compute with the natural numbers. Our programming language has an addi-
tion Operator, and a subtraction operator (monus), and uses a sequence of indexed
variables to store input, output, and intermediate values. We represent individual
variables in the sequence with identiﬁers. Our language permits Boolean expressions
as guards for loops and we allow unbounded looping. We also include two operators
that allow us to store a sequence of natural numbers in a variable and to retrieve the
leftmost value stored in such a sequence. The numbers in the sequence are separated
by a delimiter that has no value.‘ The programming language is similar to the lan-
guage used by Sommerhalder and van Westrhenen [22]. The syntax of this language
is given in Figure 4.1. Proof that this model forms a complete programming system,
sufﬁcient to express the set of all computable functions, is a standard exercise and is
omitted here. See Sommerhalder and van Westrhenen for details [22].

Let G be the grammar deﬁned by the productions in Figure 4.1, and let L(G)
be the set Of all valid sentences that can be constructed from G. We deﬁne a pro-
gram to be a quadruple Q = (p, k,n, P) consisting of three natural numbers and a
sequence of statements P E L(G). The identiﬁers that occur in the sequence P are
the program variables and ultimately will represent machine registers. The numbers

p, k specify that $1,152,. . .,:r,, and $1,132,. . . ,3], are the input and output variables

‘

‘These Operators are included only for expressibility and notational convenience. They add no
additional computational power to our language.

28

< identifier >::= {roumcmb}
< numeral >::=< pos >< numeral > I < digit >
< digit >::= 0I1I2| - - - [9
< pos >::=1I2I3I- - - I9
< expression >::=< expression > + < expression > I
< expression > 4 < expression > I(< expression >)I
< identifier > I < numeral >
<relop>::= <ISI=I7€IZI>
< Boolean constant >::= TRUEIFALSE
< guard >::=< Boolean expression >
< Boolean expression >::=< expression > or < expression > I
< expression > and < expression > Inot < expression > I
(< expression >)I < identifier >< relop >< identifier > I
< identifier >< relop >< numeral > I
< Boolean constant >
< assignment >::=< identifier >:=< expression > I
< identifier >:=< identifier >|I< identifier > I
< identifier >:=II’< identifier >
< statement >::=< assignment > Iwhile < guard > do < sequence > odI
if < guard > then < sequencel > else < sequence; > If
< sequence >::=< statement > I < sequence >; < statement >
< program >::= {(p,k,n, < sequence >);end.| p Z 0, k > 0 and p,lc S n}

Figure 4.1. Syntax of the Language.

and the number n speciﬁes that all these variables and all program variables belong
to the set {x1,xg,. . . ,xn}.

We require that p Z 0 to express that programs may or may not have input. We
require that k > 0 to express that programs have output. The value n expresses that
we require a ﬁxed number of variables for any program. In the syntax of this language,
we Often denote a sequence by S 1; S2; . . . ; Sn to imply the individual statements in
the sequence. We denote a guard by Q, and we Often use the letter e to denote

expressions.

29
4.2 Semantics of the Language

It is natural to take the meaning of a program to be the actions that a machine takes
upon it. The operational semantics of a program uses a machine to deﬁne a language.
The meaning Of a program in a language is the evaluation history or computational
sequence that the machine produces when it executes the program. The denotational
semantics method maps a program directly to its meaning, called its denotation.
The denotation is usually a mathematical value, such as a number or a function.
A machine is not a part of the denotational deﬁnition; a valuation function maps a

program directly to its meaning.

4.2.1 The Denotational Semantics of the Language

The Objects we have in mind when we compute a value are the natural numbers IN =
{0, 1,2, . . .}. We represent these objects as strings belonging to the set NAT, where
NAT = [x] < numeral >=+> x}. The valuation function for the set NAT maps it to
the set IN in the expected way. We also use sequences of natural numbers separated
by the delimiter II, where I has no value. We denote this set N = NAT(IINAT)'.
Note that NAT C N. Sequences containing delimiters are not used to compute values
so that for a string x, if x 6 N — NAT then the valuation function returns undeﬁned
if computation with x is attempted. Finally, we use the set 13 = {TRU E, F ALSE}
of Boolean values.

The Objects we compute with are constructed by a ﬁnite number Of applications
Of operators from a set Of operators we designate for this purpose. The operators are

applied to three distinct types Of elementary Objects.
1. Three types of objects:

0 NAT: {0,1,2,...,9,10,...}

30

. N = NAT(IINAT)‘

. ]B = {TRUE, FALSE}

2. Five operators:

0 0, a nullary Operator.
0 +, representing addition of the natural numbers.
a 4, (monus) representing subtraction of the natural numbers.

a II:N—>N deﬁned by
|| (4331)2 xiv-

II takes 23,3; 6 N and returns the sequence xIIy.

a II': N -+ NAT deﬁned by:

[I(x) 3- a, such that a E NAT for some ay = x 6 N

The sequence 3/ may be empty. [I’takes a sequence x E N and removes the

leftmost natural number a.

Denotational Semantics

Denotational semantics deﬁnes a mapping from syntactical entities to the values they
compute in such a way that the meaning or value of a construct is determined in
terms of the meanings of its constituent parts. This is the method of Scott and
Strachey [10]. In this view, a valuation function is deﬁned that maps statements to
their values. We use a variant of de Bakker’s notation [5] that includes the state and
the state function. A state is the condition, at any given moment, of a program’s
identiﬁers; it is an element of N”. The state function is denoted by 7, and allows us

to obtain the current value of any variables used in a statement. Recall, we represent

31

the elements of our program state space I‘ with 7. In a sense, 7 retrieves the result of
the valuation function applied to a statement in a particular state of the computation
so that we can inspect it. The set I‘ is the set Of all valuations of a given program’s
variables. Another representation for a given 7 6 I‘ is < x1, . . . ,xn >, the variable
vector used by our programs. We let M stand for the function that maps statements
to their meanings: M : S 6 L(G) x I‘ —> I‘. The valuation function or meaning
function M(S,7) = 7’, for S 6 L(G), reﬂects that the initial state 7 is transformed
by S into the ﬁnal state 7’, where 7 and 7’ determine the initial and ﬁnal values of the
variables before and after S executes. In the recursive class M is a partial function,
because nontermination is a possibility. It may be that for a given 7 and S there is
no 7’ such that M(S,7) = 7’.

To address the possiblity of nontermination in denotational semantics it is cus-

tomary to extend M to a total function by adding the undeﬁned state:

M:SxI‘U{.L}—»I‘U{J.},

where “.L” (“bottom”) is the undeﬁned state. Since .1. ¢ I‘ and 1" contains
all valuations of a program’s variables, .L is usually associated with the ev-

erywhere undeﬁned state [10], [5], [6]. For example, in denotational semantics

M (while TRUE do S od,7) = .L. The extended meaning function

M:SXI’U{i}—»FU{.L}

is strict (notation: M : S x F U {.L} —), I‘ U {.L}). A function is called strict if
f (.L) = i. That is, the value computed by a function undeﬁned on its arguments
is undeﬁned. The translation to strictness with respect to a denotational semantics

meaning function can be expressed by the acronym, Garbage In, Garbage Out, that

32

is, deﬁned outputs cannot be Obtained from undeﬁned inputs. Strictness applies to
functions for which meaningful valuation of a statement’s variables may not exist
because the statement represents a partial function undeﬁned on its argument. Our
extended meaning function is strict and we rely on strictness to guarantee that if a
meaningful valuation is impossible in a given state, then a valid deﬁnition cannot
magically be assigned by any statement. A formal discussion of strictness is given in
Section 4.2.3.

The only statement in our language for which termination is an issue is the while
do od statement. Letting d stand for the result of a typical element of the set Of
extended meaning functions M : S x I‘U {i} —» I‘U {.L}, we must determine a d such
that M(while 9 do S od,7) = 45. Intuitively by this statement we mean: repeat
execution of S zero or more times as long as Q = TRUE. This description can be
represented as the limit of a sequence of approximations ¢;,i = 0,1,2, . . ., (notation:
LL20 45;). The limit of a sequence Of approximations is the actual function value, if
it exists. For example, with f(x) = x!, f(4) = 24 is the limit and 1,2, 6, 24 is the
sequence of approximations to f (4) If a limit does not exist, e.g., f (x) = x +1, then
the limit is undeﬁned, but for each i = 0,1,2, . . ., U220 43; represents the limit of its
subsequences since for each i Z 0, d.- is the meaning that results from executing S
at most i - 1 times. The denotational semantics of a statement in our language is a

variant of de Bakker’s [5] that makes use of the state .1. and function 43 just deﬁned.
Deﬁnition 4.1 The denotational semantics of S E L(G) is given by the function
M:SxI’U{_L} —+,I‘U{_L}.

I. MCI}; := 131' + xk,7) =

A {< $17,. . .,$,‘7 = 27ft + $k7,$;+1‘7,. .. ,xn'v >} 17131317]; 6 NAT
‘7.

.L otherwise

x;-. E 7(x,-), the value of x,- in 7. Recall, 7 represents a state, and allows

33

us to obtain the value of variables in a state. M returns the least 7 such
that variable x.- obtains a new value because the arguments to addition represent
natural numbers. The state that results is J. if the arguments represent elements

of N - NAT because variables containing delimiters are not used to compute.

2. M(x; := xj;$ks7) =

{< x11,” .,x.-1 = qu — xm,x,-+11,. ..,x,,1 >} iij,xk E NAT and x51 2 xn
1‘87 {< x11,. . . ,x;-. = 0,x;+11,. . . ,xn-y >} ifx.,-,x;c e NAT and 2,": < 1:“

J. otherwise

 

If the arguments to monus represent natural numbers, then the value returned
is the result of subtraction on the natural numbers. Otherwise, one or both

arguments contain delimiters, so we return .L.
3. M(x; := xj,7) == A.7{< x11“ . . ,xn = xj1,x,'+1~:, . . .,x,,-: >} x,- 6 N

I. M(x; := c,7) = A.7{< x11,...,x;-. = c,x.-+p,...,x,n >}, c E NAT
If the right-hand side of the assignment statement is a natural number, then the
variable on the left-hand side of the assignment statement takes on the value of

that constant.

5. M(Sl;S2,7) = A7.M(S2,M(Sl,7))
The semicolon is used to combine adjacent, independent commands into a single
command [21]. We will formalize this notion in Deﬁnition 4.3 and discuss it
in depth in Chapter 4. To obtain the value of computing the whole statement

S 1; S2, we find the value of S 1 and then use this state when we operate to obtain
the value of S2.

6'. M(if g then 51 else S2 ﬁ,7) =

 

34

M(Sl,7) ifg is TRUE in 7
M(S2,7) ifg is FALSE in 7
The decision construct returns the value of executing 51 if the guard is TRUE,

i.e. if 7(9) = TRUE; it returns the value of executing S2 if the guard is
FALSE.

7. M(while 9 do S od,7) = U§O¢;(7), where

10.

do = A7.i

at,“ = A7.if 9 then ¢;(M(S,7)) else 7 ﬁ,i = 0,1,. . .
The loop has no meaning until it terminates. We obtain the value of each succes-
sive iteration by applying the loop ’3 statements to the most recent approximation
to the computation’s limit as long as conditions for termination are not met. See

Figure 4.2 for an example.

M(end-.7) = 7

The “end.” statement does not affect the value of variables in a state.

M(x; := x,- II xk,7) = A.7{< x11,. . . ,xn = $j7II$k7,$g+17,. . .,x,n >}
The concatenation operator appends the ﬁrst identiﬁer onto the left hand side
of the second operator and produces a state with the updated string as one of its

values.

M(x; :=II’x,-, < x17,...,x,~~ = 0'1II0'2II”'ﬁ01,$j+17,...,xn1 >) =

A {<317,...,$.’7=01,...,$J‘7=02II'°°II0(,$j+1'1,...,$n7 >} 1ft, EN
7.
_[_ otherwise

The deconcatenation operator moves the leftmost representation of a natural

number to the variable on the left hand side of the assignment operator, leav-

35

M(while x > 0 do x := x — 1 od,7(< 2 >)) = (Ln-:0 .-)7(< 2 >) = 7(< 0 >), since

40(7(< 2 >)) = J-
¢1(7(< 2 >)) = ¢o(7(< 1 >)) = J-
¢2(7(< 2 >)) = ¢1(‘7(< 1 >)) = ¢o(7(< 0 >)) = J-

¢3(3(< 2 >)) = ¢2(7(< 1 >)) = ¢1(7(< 0 >)) = 7(< 0 >)

¢a(‘7(< 2 >)) = 7(< 0 >),i > 3.

(U320 £)(7(< 2 >)) = 20¢.(7(< 2 >)) = Uf’iov(< 0 >) = (7(< 0 >))

Figure 4.2. Example of the denotational deﬁnition of whiledo od.

ing the remainder of the string in the variable on the right hand side of the
assignment operator. If x,- has not legally acquired a meaningful value through

execution of a previous statement, then .L is returned.

4.2.2 The Operational Semantics of the Language

The ﬁxed point argument that leads to our inductive proof method hinges on the
computational sequences built by our operational semantics. We contend that the
initial state/ﬁnal state model used by the wp calculus is insufﬁcient for partial func-
tions because the moment of termination for programs computing them cannot be
known or even guaranteed. Lacking the information “contained” in the ﬁnal state of
a computation leaves the wp method dependent on the partial assurance that the wlp
conjunct can give: The computation will not be incorrect if it terminates. Consider
an Operating system. In such a context this means that all we can do is start the
program running and wait. We may assume that “something is happening” because
we see disk lights ﬂashing and hear whirring sounds, but we cannot say anything
about what is happening for certain, because we must wait for termination since

the wp method depends on the postcondition. The wp method uses only the initial

36

state/ ﬁnal state predicate pair, so until we reach a ﬁnal state we cannot apply the wp
predicate transformer. Meanwhile, the operating system is managing the machine,
perhaps servicing requests from users, initiating remote printing jobs, or whatever.
With the ability to “examine” intermediate results of a computation via its evaluation
history, we can Observe all these activites, and check to see that they are executing
correctly.

The concept of evaluation history or computation sequence is tied to a machine.

The Machine

We specify computations with algorithms (ﬁnite descriptions of computations over a
certain data type for any given input), and represent algorithms as programs written
in the language we have described. Because we are interested in the correct behavior
of computations and not just in the correctness of the algorithms that specify them,
we need a computer to execute algorithms and produce an evaluation history of each
execution.

The machine model we use is the Random Access Machine (RAM) described by
Meyer and Ritchie [4]. The RAM consists of an instruction register of arbitrary
length that holds the program. The operational semantics of our language deﬁnes
the Operation Of the machine on this program. The RAM has a Boolean test register
for evaluating any guards the program uses, and a data memory that is unbounded
and composed of registers of arbitrary (but ﬁnite) length. See Figure 4.3. Prior
to execution of any program the variable vector of our machine is composed of n
undeﬁned variables. Once input is introduced, but before execution commences, the
variable vector of our machine is composed of p deﬁned input variables, with the

remaining n — p variables undeﬁned.

37

Data Memory

 

 

Instruction

.
Re . ‘———* x0

 

 

 

 

x1

 

x2

 

 

 

 

Boolean Test Register x3

 

 

Infinite bank of
registers of
arbitrary length

 

 

Figure 4.3. Random Access Machine (RAM).

The Operational Semantics

When we say that a program executes, we mean that our operational semantics
produces a unique computation sequence that contains an evaluation history for ex-
ecution of each statement, and the machine mirrors what the Operational semantic
function is doing. We formalize this notion of computation sequences and program
meaning with operational semantics for our language.

First we formalize the way our machine implements the natural numbers. The
machine consumes input and produces output. We require that all Objects used in
computing be ﬁnitely representable. The objects we use are the binary encodings of
the natural numbers. To specify these objects, we ﬁx a data type to formalize the
data elements and the Operators used by our machine.

The data type we use has three sorts. First is the set of binary strings represent-
ing the natural numbers BIN = {0,1,10,11,100,101,110,lll,...}. We normalize

these strings by deleting leading zeros. This is the sort that our machine computes

38

values with; it is the type of interest. Second is the set BIN = BIN (IBIN )‘, where
syntactically I is used as a delimiter and has no semantic value in a computation.
The semantic meaning of I is undeﬁned. When we say that a variable in our machine

vector is undeﬁned, we mean that the position of that variable within the vector is

set to I. Finally, we use the set 13 = {TRUE , FALSE} Of Boolean values.
1. Three sorts:

. BIN: {o,1,1o,11,100,101,110,111,...}
. BIN = BIN(IBIN)*

0 13 = {TRUE, FALSE}
2. Ten operators:

0 The functions 0 and 1, representing the elements 0 and 1 from the binary

numbers.
0 +, representing addition Of the binary numbers denoted by two strings.

o 3—, (monus) representing subtraction of the binary numbers denoted by

two strings.

. u: BIN —» BIN defined by
H (1‘, y) g $va-
. y; BIN —» BIN deﬁned by:
[I(x) é a, such that a e BIN for some ay = x e BIN

The string y may be empty.

0 idBIN : BIN -> BIN and idguf : BIN —> BIN, the identity functions.

39

o Predicate OBIN deﬁned by:
®a(x) s [i f x®a then TRUE else FALSE], a,x e BIN, G) e {<, s,=, 752, >}
Our data type is B:
3 = {BIN’BIN’IB’idBINtidBINs'I'a;’ ll, lI’,0,1,®BIN}

We express our input and output as natural numbers, IN = {0,1,2, . . ..} We do this
for readibility, because it is easier for people to think in the natural number domain
than in the binary number domain. Our machine is equipped with a coding function
e : IN -b BIN which maps zero onto 0 and any number greater than zero onto its
binary representation, with leading zeros removed. Our machine is also equipped
with a decoding function dc : BIN —+ IN. Since the function e is a bijection we deﬁne
the function dc in the logical way. NO decoding of elements using the I delimiter is

necessary.

Deﬁnition 4.2 A conﬁguration 6 of the machine is a pair 6 =< P,7 > where P E
L(G) is a sequence of command statements and 7 is a state in which the next command

S E P can execute.

Since our machine is digital, execution will move through discrete stages i, from
a conﬁguration, which are represented (if possible) by further conﬁgurations. These
conﬁgurations will either have the form < S;, 7.- > where 7; is the state at stage i and
S.- represents the remaining computation, or they will have the form < end.,7.- >
where i is the ﬁnal stage at termination and the resulting 7,- is the machine vector in

a terminal conﬁguration.

Deﬁnition 4.3 A functional 1' over L(G) maps the set ofstatements L(G) into itself.

That is, 1' takes any statement S E L(G) in a given state 7 as its argument and yields

40

a statement 7(5) 6 L(G) in a state 7’ as its value.

In our language, the functional we deﬁne is the symbol “;.” For readibility, we may

let 1' denote “;.”

Deﬁnition 4.4 A computational sequence, < 50,70 >l-< 51,71 >l- . . ., is a sequence
of configurations which is inﬁnite when no S,- 5 end. A computational sequence is
ﬁnite when an end. statement is encountered, i.e. < 50,7 >,...,< end.,7 > .
The symbols 6.- b 6.41 represent the transition from one conﬁguration to its successor
under our functional that maps program statement/program state pairs to program

statement/program state pairs.

Deﬁnition 4.5 The operational semantics of program statements is given by the
function 0 : L(G) x F —i L(G) x I‘. Let 0 denote a remaining sequence of pro-

gram instructions that may be empty.

1. 0(2); 2: 2:,- + xk;a,7) =

< 0,311,...,:r,-,: = x,» + $k1,$i+11,...,$n‘7 > iij,a:k e BIN

< a,ﬂ1,...,ﬂn > otherwise
an E 7(35). It represents the value of variable x,- in state 7. If the arguments to
addition represented binary encodings of natural numbers, then the remaining
program sequence and a new state with values reflecting the result of addition is

returned. Otherwise, the remaining program sequence and a state with undeﬁned

values denoted by the valueless delimiter ﬂ is returned.

2. 0(3; := xj;xk;a,7) =

7
< 0,117,...,a:,-.,r = I)». —$k1,l‘,‘+17,...,$n1 > if.1:,-,ac;g 6 BIN and 1:51 2 21.1

t < a,x11,...,:r,-,: = O,x,+1~,,...,:rm > if$j,$k E BIN and rep < 31:1

 

L < a,ﬂ1,...,ﬂn > otherwise

41

If the arguments to monus represented binary encodings of natural numbers,
then the remaining program sequence and a new state with values reflecting the
result of subtraction of binary encodings of natural numbers numbers is returned.
Otherwise, the remaining program sequence and a state with undeﬁned value,

denoted by the delimiter ﬂ, is returned.

. 0(x; := xj;a,7) = < a,xn,. . . ,x,-.,: = $j7,$.’+11,. . .,x,n >, x, E BIN
We obtain the remaining program sequence and a new state with the value of x.-
updated to the value of 3),, and x,- and all other variables remain as they were

before the operation.

. 0(x; := c;a,7) = < x17,...,x,-.,I = c,x.~+1~,...,xn1 >, c6 BIN
We obtain the remaining program sequence and a new state with the value ofx;
updated to the binary encoding of the natural number c represents, and all other

variables remain as they were before the operation.

- 0(51;52;a.7) = 0(52;0.H§(0(51.7)))
I]: is the function Ax1x2---xp[xk], projecting a p-dimensional vector onto its
1:“ component. We project into the computation sequence to obtain the state

resulting from execution of 5'1 and use this state in our computation of 52.

. 0(if Q then 51 else 52 fi; 0,7) =

0(Sl;a,7) ifg is TRUE in 7
0(52; 0,7) ifg is FALSE in 7

If the Boolean test register shows that the value of g is true when tested, then

we execute SI. We execute 52 ifg is false when tested.

42

7. 0(while g do 8 od;0,7) =

0(S;while g do 5' od; 0,7) ifg is TRUE in 7

< 0, 7 > otherwise

We extend our computation sequence one more step by unfolding the loop each
time the Boolean register shows that the guard tests true. When the guard tests
false, we obtain the program sequence that remains after the loop and the state

that resulted from the last execution of the loop.

8. 0(end.0,7) =< 0,7 >
When an end. statement is executed, the ﬁnal program state is returned and

the instruction register is cleared.

9. 0(x; := x,- ” xk;0,7) = < 0,2217,” . ,x,,: = xj-ylika,xg+p,. . .,x,.-: >
We obtain the remaining program sequence and a new state with variable x.-

containing the string xJ-ﬁxk.

10. 0(x; :=ll’x,';a, < x17)"°9xj7 = 01ﬁ02l° "l01,.-o,$nv >) =

<0,xn,...,x,-.,a =01,...,xj,:=02ﬁ---ﬂ0‘1,...,xm > iijEBIJV

<0,tl1,...,tln > otherwise

If x,- has acquired a legal value by a previous computation step, then we obtain
the remaining program sequence and a new state with x,- containing the leftmost
element of a string of binary representations of natural numbers separated by
delimiters, and 2:,- containing the string that remains after removing its leftmost

element. Otherwise, we return a state with coordinates set to )1.

Definition 4.6 The operational meaning of a program P E L(G) with 70 an initial

43

state, is given by:

0‘(P’70)9

where It indicates repeated composition of the operational semantic function with itself.
That is, the operational semantic function continues to manipulate the sequence of

program statements in the instruction register until termination.

Thus the operational meaning of a program is the computation sequence that
is induced by the functional we use operating on the program statements. From a

computation sequence we can extract the functional meaning of a program.

Deﬁnition 4.7 For any computation sequence induced by executing a program Q =

(p, lc,n, P), the function FQ computed by the program is deﬁned by

FQ(H1...;.(70)) = n1""‘(ng(03(Pa’70))) if Hi(0’(P.7o)) =< end.,7j >

undefined otherwise

Program P computes the partial function FQ((II1,,,k(70)) = f(x1,. . . ,xp).

At this point we give an example of how the operational semantics of a simple
program builds a computation sequence, and how we can use the sequence to obtain

the operational meaning of a program and the functional meaning of the program.

Example 4.1 Let Q =(1,1,1,while x > 0 do 2: := x — 1 od;end.) and let 70 = 2.
Then the operational semantics gives the computation sequence

60 =< while x1 > 0 do x1 := x1 -1 od;end.,2 >|-

61 =< x1:= 2 - l;while x1 > 0 do an: x, — 1 od;end.,2 >|-

62 =< while x1 > 0 do x1 := x1 -1 od; end.,1 >}-

63 =< x1:=l—1;while x1 > 0 do x1:= x1 —lod;end.,1>l-

64 =< while x1 > 0 do 3:, := x1 — 1 od;end.,0 >}-

65 =< end.,O >

44

We can see from examination of the computation sequence of our program that its
operational meaning is 60 l- 61 l- 62 l- 63 l- 64 l- 65. Furthermore, examination of the
sixth conﬁguration provides the additional information that the program terminates.

The functional meaning of the program can be identiﬁed by projecting onto the
output variables of the program vector of the last element of the computation se-
quence FQ(H1(70)) = I11(II§(05(P.70)) = 0-

Our Operational semantics allows us to use a projection operator and our state
valuation function 7 to investigate the intermediate stages of a computational chain
as a computation progresses, e.g. II,(II§(02(P, 70)) = 1. In the theory of ﬁxed points,
projection onto the computation sequence built by our functional allows us to obtain
the approximations to the function ﬁnally computed by the program. Note that the
least ﬁxed point of the function computed by our example Q is reached at the ﬁfth
conﬁguration, i.e., H1(H§(04(P,70)) = 0, since for i > 4 projection onto our output

vector returns the value 0.

4.2.3 Semantic Equivalence

Our operational semantics agree with our denotational semantics with respect to the
function value computed by a program, since J. is equivalent to undeﬁned.

We support this conclusion by proving equivalence between our operational se-
mantics and our denotational semantics, using two lemmas. The ﬁrst step is a lemma
that establishes that the function 0(5; 0, 7) is strict in the same sense that the func-
tion M (3,7) is strict, i.e., it is impossible for our machine to produce a meaningful
value for a partial function that is undeﬁned on the given input. The reason why we
wish to establish strictness is continuity. It is continuity that guarantees we can ob-
tain accurate approximations of ﬁnal results at intermediate stages of a computation
because the limit of a computation is predictable.

The second lemma deals with monotonicity. It says that if the execution of a

45

statement causes a state change, then we have moved one iteration closer to resolution.

The functional “;” has produced the next stage in the computational chain.

Lemma 4.1 Suppose the variables upon which S E L(G) depends are undeﬁned.
That is, let x;,...,xk E S = 11, where l S i,...,lc S n. Represent the fact that

particular undeﬁned variables exist in S with L. Then 0(S; 0, .L) =< 0, .L >.
Proof. Structural induction on S E L(G).

l. S E x := e, where e is not a natural number. 0(x := e; 0, .L) =< 0, J. >. Since
.1. ¢ I‘, i.e., the variables in e are undeﬁned, substitution achieved by computing
an expression cannot give deﬁnition to other program variables. Substitution
does not change the meaning of .L. The two cases where the concatenation

operator and the deconcatenation Operater are used have the same argument.

2. S E SI;S2. 0(Sl;52;0,.1.) = O(SZ;0,H§(O(SI,.L))
= O(S‘2.;0, .L) =< 0,.L > .

3. S E ifg then SI else 52 ﬁ. O(if Q then 51 else S2 fi;0,.L) = < 0,.L > by

deﬁnition of the operational semantics of if ﬁ.

4. S E while g do S od. O(while 9 do S od;0,.L) =< 0,J. >. G, the guard

function, maps a Boolean expression to the set TRUE, FALSE.

0 Case 1: g is TRUE in .L, (e.g., while TRUE do S od).
The operational semantic function produces the sequence
0(while TRUE do 5 od; 0, .L) = O(S;while TRUE do S od;0, .L) =
0(while TRUE do S od; 0, .L) = 0(S; while TRUE do S od;0, .L) . . .
which is inﬁnite because no statement/state pair is < end.,7j >, j =
0,1, . . . and because all 7,,j = 0,1,... 6 I‘, the only state we can return

is .L.

46

a Case 2: g is FALSE in .L. This follows directly from the operational

deﬁnition of the whiledo od statement.
5. S 5 end. O(end.; 0, .L) =< 0, J. > by deﬁnition.

Lemma 4.2 Let ¢,~,i = 0,1, . . ., be as in the denotational deﬁnition of the while 0
do S od statement. Then for every 7 E I‘ and 7’ 6 I‘ U {J.}, and for alli 2 0,
7’ = «tn-(7) if and only if there is a j,0 Sj < i, such that M(Sj,7) = 7’. [Comment:

7’ is the result of no more than i — 1 applications of 5.]

Proof. (“=>”) Induction on i.

Basis: If i = 0 then j = 0, so there is nothing to prove.

Hypothesis: Assume 7’ = ¢,(7),0 S j < i, i > 0.

Show: 7’ = ¢;+1(7),0 S j < i + 1. This is 7’ = A7.if Q then ¢;(M(S,7)) else 7 ﬂ.

0 Case A: Q is TRUE in 7. Then the integer j we need is greater than 0
since we will execute S at least once. This implies that 7” = M(Sj‘1,7’”)

for some 7” and 7’”, so 7” = ¢;_1(M (S, 7”’)). One more execution gives us

‘7' = ¢i(M(S:‘7")) = ¢i+1(7),0 Sj <i+1-

a Case B: Q is FALSE in 7. If g is FALSE then 7’ = 7,j > 0 since we
have executed S at least once because 7 6 I‘, i.e., 7 is deﬁned. Thus for
some 7”, ’7 = M (St .7”) = ¢.(S,7”) = 7’, which is by deﬁntion ¢a+1(5.’7), 80

05j<i+L

(“ <=”) Induction on i.

Basis: If i = 0, then ¢o = A7..L ¢ I‘, so there is nothing to prove.

Hypothesis: Assume 7’ = M(Sl,7), 0 S j < i, i > 0.

Show: If 7’ = M(Sj,7), O S j < i + 1, then 7’ = ¢,+1(7) =
if 9 then qS,-(M(S,7)) else 7 ﬁ.

d
E

47

0 Case A: G is TRUE in 7. Then 7’ = ¢.-(M(S,7)) which is ¢,(7”) a previous
element of the computational chain. We have assumed that there is a 1" such
that 7’ = M(Sj',7”). Lettingj = j' +1 gives us that 7’ = M(Sj,7),0 Sj <
i + 1.

a Case B: Q is FALSE in 7. If G is FALSE then 7 = ¢;(M(S,7”)) for some
previous element in the chain and there was a j such that 7 = M(Sj,7”), but

this is '7 = M(S’n”) = 7’ = ¢;+1('7),0 Si < i+1-
Theorem 4.1 0(S; 0,7) = M(S,7).

Proof. Let 0 = 0, and use structural induction on S E L(G). If S is not an iterative
statement, the result follows immediately from the deﬁnitions of operational and
denotational semantics. Now let S 5 while g do S od. Assume that 0(S, 7) = 7’.

Either 7’ 6 I‘ or 7’ = .L.

0 Case A: 7’ E I‘. Then there is aj 2 0 such that 7’ = M(Sj,7). Let 4’0 =
A7.J. and let <75,“ = A7.if Q then ¢i(M(S,7)) else 7 ﬁ,i = 0,1,.... The
denotational deﬁnition of S is M(S,7) = (Di-:0 ¢.-)(7). By Lemma 4.2, 7’ =
¢i(7)a0 51 < 5+1, 30 7' = Lil-3.3.0 ¢£(7) = ( .20 430(7) = M(Sﬂl-

a Case B: 7’ = .L. By Lemma 4.1 we have that our computation sequence is
inﬁnite and for all lc = 0,1,. . ., 452(7) = J_, since if for some i Z 0, ¢£(7) = 7" e
I‘, by Lemma 4.2 there would exist a j,0 S j < i such that 7” = M(Sl,7) and
this would give us that O(S,7) = 7” E I‘ and 0(S, 7) = .L, a contradiction.
Therefore for all k 2 0 45;,(7) = J. and this is the same as M(S, 7) = .L.

CHAPTER 5

Mathematical Foundation for
Reasoning About Nonterminating

Computations

In this chapter we give the mathematical foundation we use to reason logically about
unbounded and nonterminating computations. We have already given our machine
and its language, and we have deﬁned formally what we mean when we say that
program statements execute. Operationally this meaning is the computational se-
quence induced by our higher order function from program statements to program
statements. The computational sequence is the vehicle we use to reason about a
computation.

There are two types of postconditions for loops:

1. Descriptive postconditions deﬁne non-empty sets of program states. The Dijk-
stra/Gries [2], [21] method requires proof of termination by manipulation of an a
priori upper bound. In fact, the requirement of a known upper bound limits this
method to the primitive recursive class. Therefore, descriptive postconditions

can be written for every loop.

48

49

2. Nondescriptive postconditions, i.e., FALSE, deﬁne empty sets of program
states. Nelson [6] allows nontermination. In his generalization of Dijkstra’s
wp calculus, Nelson addresses recursively speciﬁed programs but provides a
method for showing only overall partial correctness of these partial functions.
In Nelson’s method the postcondition of a nonterminating recursion is FALSE
because a ﬁnal state cannot be reached, i.e., the set of ﬁnal states is empty.
Like Nelson, we consider FALSE an appropriate postcondition for a nonter-
minating loop. Unlike Nelson we use much more descriptive predicate logic
sentences for nonterminating computations than FALSE. We eschew the ini-
tial state/ ﬁnal state paradigm in these computations because we model them as
chains composed of intermediate stages, where each stage is an approximation
to the limit of the computation, so each stage has a predicate logic sentence

that is an approximation to the goal the loop’s designer intended.

Gries has said that “loops are designed for speciﬁc purposes—to establish the truth
of one particular postcondition” [21]. For total recursive functions the “speciﬁc pur-
pose” of a loop and the postcondition of the loop are identical. The “speciﬁc purpose”
or goal of the loop is the machine state at termination, and this state can be described
logically. Postconditions are assertions that hold about the output of a loop after the
loop terminates. Outside the total recursive class, the goal of a loop can still be
expressed logically, but it may not be the same as the postcondition of the loop.
The goals of some loops are achieved independent of termination, the loops produce
output and so require output assertions, but these assertions cannot be considered
“postconditions” using the accepted deﬁnition of the word.

Loops that are “deﬁned on their input” are loops that accomplish the speciﬁc
purpose of their designer whether they terminate or not. An example of a loop
that is deﬁned on its input and terminates is Ackermann’s function, a total recursive

function. Another example of such a loop is the primitive recursive function for

50

factorial. An example of a loop that is deﬁned on its input and does not terminate
is an Operating system service procedure that loops until it receives a request, then
fulﬁlls the request and returns to its waiting state. The example of the nonterminating
operating system service procedure highlights the need for a logical description of a
loop’s goal independent of the postcondition. Since the loop does not terminate its
postcondition must be FALSE, but the speciﬁc purpose of such a loop is certainly
more descriptive than that.

We are interested here in those partial functions with descriptive goals. These are
functions deﬁned on their input. When these functions are computed by programs,
the purpose of the program is to reach a state whose logical description is equivalent
to the designer’s speciﬁc purpose. For terminating loops the conjunction of this logical
expression, the loop invariant, and a false guard implies a descriptive postcondition.
For nonterminating loops deﬁned on their input we can use the conjunction of the
logical description of the loop’s goal and the invariant to prove that each iteration of
the loop is correct.

To achieve this goal we show that programs that use loops induce computational
sequences that are chains. The existence of computational chains guarantees that we
can obtain accurate information about the computation at intermediate stages (chains
have the property of monotonicity). Chains also guarantee that the information we
obtain is an approximation of the ﬁnal result because the limit of a computation is
predictable (chains have the property of continuity). From this we show that deﬁned
loops have descriptive goals that can be used with the loop invariant to prove the
loop is incrementally correct.

It follows from a result of Kleene that all chains have least upper bounds, and that
these are ﬁxed points of the computation [7]. Fixed points can be viewed as “closed
form” expressions of recursively speciﬁed programs [23], [6], or as approximations to

the solution of repetitive computations [5], [24]. The program state that occurs at the

51

least upper bound of a computational chain has a logical sentence that deﬁnes the
speciﬁc purpose of the loop because it is the ﬁrst true approximation to the function
computed by the loop; all other approximations are extensions of it [7].

In order to establish the existence of computational chains induced by programs
with loops we deﬁne a functional that maps program statements to program state-
ments. We prove that the functional is continuous for all noniterative statements,
that the functional is continuous over one application of our looping construct, and
that the functional is continuous over multiple applications.

To impose the structure we need for discussing continuity and for establishing
the correspondence we need between our mathematical foundation and the predicate
transformer of our proof method, we show that the state space composed of all possible
variable valuations of our programs is a complete lattice. Like Nelson [6] we provide
for the possiblity of a program mapping a deﬁned initial state to an undeﬁned set
of ﬁnal states. This is the mapping that occurs in the case of a nonterminating
computation, and it is the justiﬁcation for the FALSE predicate logic postcondition
of a loop which we use as our least element. Every continuous chain induced by
a program within this lattice has a least upper bound, and this gives us our top
element [7].

The organization of our lattice depends on a partial ordering relation “more de-
ﬁned,” imposed by our program statements which we, as others (Dijkstra [2], [l],
Hehner [8], Gries [21], Nelson [6]) view as commands mapping states to states. We
view the relation as a means of measuring the information content of the states our
commands map to, and use it to describe the quality of the approximation to a

solution each state in a computational chain represents.

52
5.1 The Semi-Lattice of Computations

More-deﬁned is a relational on the set of commands on a set of program states I‘.

Deﬁnition 5.1 Let C and C’ be two commands on F. We say 0 is more-deﬁned

than C’ , notation: C" -< C, if and only if
1. dom(C’) Q dom(C),
2. V7 6 dom(C’), 7.0 Q 7.C".
Proposition 5.1 -< is a partial ordering.

Proof:
0 C -< C. Therefore < is reﬂexive.

a Let C and C’ be two commands such that C’ -< C and C -< C’. From dom(C’) Q
dom(C) and dom(C) Q dom(C’) we have that dom(C) = dom(C’). For all
7 6 dom(C), 7.C Q 7.C’ and 7.C' Q 7.C, so 7.0 = 7.C’, so C = 0’. Therefore

-< is antisymmetric.

a Let C, C’ and C” be three commands such that C” -< C" and C" -< G. Then
dom(C’) Q dom(C) and dom(C”) Q dom(C’), so dom(C”) Q dom(C). Let 7 be
an element of dom(C”) so it is in dom(C'). From 7.0 Q 7.C’ and 7.C’ Q 7.C"

we have that 7.0 Q 7.C”. Therefore, -< is transitive. D

We want to show that this partially ordered structure is a lattice so we can use
the lattice properties of more-deﬁned to measure the information content of elements
in a computational chain. Given two commands C and C’ on I‘, we are interested
in the existence of lub(C', C"). The least upper bound of two commands represents
the sum of the quantities of input and output information contained in them. Those

quantities can only be summed if the two relations deﬁned by the commands have

53

at least one element in common. The property of monotonicity guarantees that the
application of successive commands in a computational chain does not disturb the
established ordering relation, i.e., if two commands have a common initial state then
the application of the commands must yield a state that is more-deﬁned than the
initial state. In this sense the application of commands in a computational chain
yields results that are approximations to their mutual least upper bound; they are
consistent in maintaining the ordering relation more-deﬁned on the lattice.
Consistency expresses the property of monotonicity and is a necessary and suf-
ﬁcient condition for the existence of a least upper bound in a computational chain

induced by commands in a lattice ordered by more-deﬁned. Mili, Boudriga, and

Mili [25] formalized this.

Proposition 5.2 Two commands C and C' satisfy the consistency condition

dom(C n C”) = dom(C) ﬂ d0m(C’)s

if and only ifC and C" have a unique least upper bound.

Mili et. al. [25] express the unique least upper bound as the union of the states

in C and in C’, unioned with the intersection of states in C and C":

lub(C, C') = (idr(dom(C) — dom(C’))C) U (idp(dom(C") — dom(C))C") U (C n C").

This expression is suitable for the commands of our language within a lattice ordered
by more-deﬁned. It is an upper bound because it is equal to dom(C) U dom(C"),
therefore larger than both dom(C) and dom(C"), condition one of our deﬁnition of
more-deﬁned. Informally, the expression is minimal because for any other possi-
ble upper bound, say C”, dom(C) Q dom(C”) and dom(C’) Q dom(C”). Thus,
dom(C) Udom(C’) Q dom(C”). Because of the expression of lub(C, C’), we have that

54

dom(lub(C,C')) Q dom(C”), so C” is more-deﬁned than lub(C,C').

In a sense, the least upper bound of two commands in a lattice organized by the
relation more-deﬁned can be compared to the weakest liberal precondition of the wp
calculus, because both address the expected result of program execution.

The greatest lower bound of two commands represents the amount of redundancy
between the quantities of information they carry. Greatest lower bounds provide
common initial information for pairs of commands. In a sense, glb(C’, C’) for two
commands C and C’ on I‘ in a lattice organized by the relation more-deﬁned parallels
the weakest precondition on a set of states in the wp calculus because both deﬁne the
largest set of initial states from which the two commands can execute correctly. The

greatest lower bound of any pair of commands always exists in this lattice.

Proposition 5.3 [Mili et al [25]. Any pair of commands C and C" have a greatest

lower bound, which is given by the expression

glb(C, C") = iddom(C)ndom(C')(C U 0’).

Since we want to map FALSE to some state, like Nelson [6] and Mili [25], we
deﬁne the everywhere undeﬁned relation, a relation capable of mapping deﬁned states

to no states:

C¢=Fx(l).

C. will be the minimum in our lattice.
For this relation we extend the deﬁnitions of domain and image set to have the

following identities:
O d0ﬂ1(Co) = F,
o V7,7.Co = 0.

As a relation Co is more-deﬁned than all other relations because it has the largest

55

domain which is condition one of our deﬁnition of more-deﬁned. According to con-
dition two of our deﬁnition of more-deﬁned, we see that any other relation is more
deﬁned than Cg, since for any other relation C, V7 6 dom(C), 7.Co Q 7.C.

In summary, the set of commands viewed as binary relations is partially ordered
by the relational more-deﬁned, and each pair of commands has a greatest lower bound.
Under a condition of mutual consistency, each pair of commands has a least upper
bound. This partial ordering deﬁnes a lattice on the state space.

Next we investigate the requirements for mutual consistency among commands,
and show that computations can be represented as ascending chains in the lattice of
our state space, and that in each such chain mutual consistency exists among all the
commands used to induce it. We show that because every ascending chain has a least

upper bound, our lattice is actually complete.

5.2 Fixed Points

Our programs Q = (p, lc,n, P) represent n-ary partial functions, n _>_ 0, from vectors
of natural numbers to vectors of natural numbers. That is, for every element of
N", f ((31,172, . . . ,xn) either terminates and yields some element of N“ or results in
a computational sequence of inﬁnite length which does not produce a ﬁnal value.
Guard functions are n-ary partial predicates that map N" into {TRU E, FALSE}.
Because we are dealing with partial functions and also because sequencing is
an element of our syntax it is possible that we may attempt to compute functions
undeﬁned on some x,-, 1 S i S n. We use w to represent variables for which deﬁnition
is impossible or no value is given, and so we extend our domains JV” and IE to

N" U {w} and IB U {to}. We denote these extended domains ML)" and 13“,.

56

5.2.1 Interpretation of Fixed Points

The operational semantics of our loops is based on a continuous functional operating
on program statements whose variables obtain their valuation from our extended
domain 0%,)". Our functional is “;” which we denote by the symbol 1’ for readibility.

In Chapter 4 the operational semantic function relied on r to distinguish the next
executable statement from the sequence of statements in the instruction register.
Recall, from Section 4.2.2, 0(S; 0,7) =< 0,7 >, for 0 a possibly empty sequence;
1' is functionally deﬁned by this statement and performs a task that parallels the
operational meaning of “;.”

Once we give valuation to the variables of our commands, the commands become
speciﬁc partial functions of the variables they manipulate. Other program variables
not appearing in a command are not affected by that command. We view speciﬁcally
valued commands as maps from program states to program states. That is, all of our
commands are functions and belong to the set {(Nw)" -—> (Nw)"}. We will prove that
these functions are monotonic.

The functional 1' maps a program statement to its logical successor in a program.
If the function is atomic, i.e., not iterative, then its logical successor is the next
sequential statement of the stored program. 7' is clearly a continuous functional for
noniterative functions. If the function r operates on is iterative, then the result 7
maps to depends on the condition of the guard. We will prove that r is continuous
for one application of our iterative functions, i.e., r correctly maps the sequence of
statements within the scope of a while do od statement when the guard of the
statement becomes false. We will prove that r is continuous for multiple applications
of our iterative functions, i.e., r correctly maps the last executable statement of a
looping construct to the ﬁrst executable statement when the statements in the loop

have executed and the guard of the loop tests true. With the proof of continuity we

57

ensure that whether we take the least upper bound of a chain 1' has built or apply 1' to
the least upper bound of such a chain we obtain identical results, because continuity
preserves limits. That is, because our program statements are monotonic and because
our functional 1' is continuous, the computational sequences that result are chains and
1' takes us to the statement in each chain that computes the least upper bound of the

chain. The least upper bound of a chain represents the limit of the computation.

Deﬁnition 5.2 The functional 1' maps the set of partial functions into itself, 1' :
{(Nw)” -+ (NL)"} -+ {(Nu)" H (Nw)"}. That is, for a program P = S;P’ in L(G)
where S is a statement in L(G) and P’ is a program segment in L(G), (we view P,

S, and P’ as partial functions f, f1, and f2 respectively in {(Nw)" —» (Nw)"}),

1'(P) = P’.

This mapping is deﬁned explicitly in Section 4.2.2.

Kleene’s First Recursion Theorem [7] states that every algorithmic description of a

partial function can be deﬁned in terms of a partial function and its arguments.

Theorem 5.4 First Recursion Theorem[Kleene]
For any n 2 0, let F (6; x1,...,x,,) be a partial recursive functional, in which the

function variable 6 ranges over partial functions of n variables. Then the equation

(€;$1,---.xn) = F(€;$1.---.xn)
has a partial recursive solution (t forﬁ such that any solution (25’ for{ is an extension
of d).

This theorem says that every continuous functional 1' has a least ﬁxed point that is

actually the least upper bound of the computational chain induced by the functional.

58

What this theorem means to us is that every value computed by a partial function
is computed by some program, and furthermore, that of all the programs capable
of computing that value (there are an inﬁnite number of such programs), there is
one that does the job with the least amount of information (or as Kleene phrases it:
“. . .on the smallest range of deﬁnition,” i.e., that subset of the domain where the
function is total).

One way of describing ﬁxed points is to say that the functional 1' maps a function to
itself (notation 1'( f ) = f). This is the “f (x) = x” view of Davis [24] who describes an
approximation relation that relates approximations of function values to the actual
function value, and also of Scott and Stoy [10]. When we view 1' in this way we
consider not so much the mappings from statement to statement (as when we are
building computational chains), but we see the chain of statements as code that is
itself a function that computes a value when it is executed. In this view, 1' maps the
code segment to the value it actually computes.

Nelson [6] and Manna [23] take the view that the ﬁxed point produces the “best”
deﬁnition of a recursively speciﬁed function. For example, consider the recursive spec-

iﬁcation of the factorial function:

Ill
5".

f(x) is defined as: if x = 0 then 1 else x * f(x — 1)
(1) (2)

In (1) we have the recursive speciﬁcation for a program. In (2) we have the “closed
form expression,” a non-recursive representation of the code. When we relate this
equation to Kleene’s theorem, we see that (1) is the algorithmic description of the
function, and (2) is the the primitive recursive function that computes it. xl is the
least ﬁxed point of this recursive speciﬁcation because it exactly deﬁnes the function

f(x) and it is minimal because it is deﬁned for all 0 S x < x + l, and undeﬁned

59

everywhere else. x! has the “smallest range of deﬁnition.”

In this latter view, ﬁxed points are used to describe the values we intend our
functions to compute. The translation to loops (that are not recursively speciﬁed)
is that the speciﬁcation of a loop (the right-hand side of Kleene’s equation) is the
“speciﬁc purpose” or goal of the loop. As discussed in the introduction to this chapter,
for total and primitive recursive functions this speciﬁc purpose is the postcondition.
For partial recursive functions which may have postcondition FALSE, we say the
speciﬁcation of the loop is a logical description of the goal of the loop. In both cases,
the conjunction of the loop invariant and the goal of the loop allows us to verify the
correctness of each iteration of the loop.

We view the ﬁxed point of a loop as the speciﬁcation of the loop because it

describes the value we expect to compute. Consider the equation for a loop:

while(x) is defined as : while (,7 do S od 5 R

(1) (2)

Notice that (1) is Kleene’s algorithmic description, or “formula” for computing and
(2) is a description of the value we expect the loop to compute. Our continuous
functional 1' maps the computational chain it induces to the least upper bound of
that chain, and this least upper bound is a program state that has logical description
R when the loop is correct. When the program executes there is an i,i Z 0, such
that the i‘“ iteration of while do od on a variable x, denoted while‘(x), computes
our intended value, and for all k > i, while(x) does it with the least amount of
information.

A good example of this is a program that computes the it“ prime number in
ascending order. (We assume there is a macro that tests whether a number is prime
by directing a search for divisors within the range 2 S i S number — 2, returning 1

if no divisor is found, because it is the while loop we are interested in for now.) By

60

“macro” we mean that there is a body of code that can be substituted inline for the
statement isprime := Prime(y). We formalize this notion of macro in Section 6.1,
and present the macro in Section 7.3.

Program Primes

z := 0;

:4 == 0;

while y 2 0 do

3/ == 3/ + 1;

isprime := Prime(y);

if isprime = 1 then

P i: 3/;
z := z + 1;

ﬁ
od

The least ﬁxed point of the entire program is the undeﬁned element because the
loop that computes it is nonterminating by design, so we can never match a descriptive
postcondition (we can never reach the postcondition, so we expect no ﬁnal value).
Thus, the established postcondition of this loop must be FALSE.

This corresponds to the denotational semantics we have deﬁned which say that
the meaning of a nonterminating loop is “everywhere undeﬁned” or i.

This also corresponds to our operational semantics because an inﬁnite computa-
tional sequence cannot produce ﬁnal results. The inﬁnite computational sequence is,
however, a concatenation of computational subsequences each of which is a chain as
we will show in Section 5.3. Since every subsequence has a least upper bound which
is its ﬁxed point, and these ﬁxed points are not the same as the least ﬁxed point of
the entire sequence, we have an inﬁnite number of intermediate approximations to

the set of prime numbers.

61

5.3 Theory of Fixed Points

Our primary objective is to show that our functional 1' induces computational chains
within our state space, and that each such chain has a least upper bound, giving us a
complete lattice. First we introduce the property of monotonicity and show that all
of our program statements have this property. We then formally deﬁne the properties
of monotonicity and continuity for functionals and show that our functional has these
properties for single and multiple applications of a loop. We also show that 1' is
continuous for all of our noniterative statements. Given that our program statements
are monotonic and that our functional is both monotonic and continuous, we are
assured that our computational sequences are chains. From this we invoke Kleene’s

First Recursion Theorem that guarantees all of our chains have least upper bounds.

5.3.1 Monotonic Functions

We wish to extend our notation for the relation more-deﬁned to states in the logical

(but consistent) way on our extended domain (Nw)”. We let

4

1. x-<x'forallx'€N”.
2. 545m ally'E (ALF—N" and alli’EN".

-<37andy”-<:i:'forallx,yEN".

Si

3.
This ordering has nothing to do with the natural ordering S on the natural numbers.
Deﬁnition 5.3 Monotonic Functions
An n-ary function f from (1%)" into ML)" is said to be monotonic if (x1, . . . ,xn) -<
(3/1, . . . ,yn) implies f(x1,. . .,x,,) -< f(yl, . . . ,yn) for all (x1, . . . ,xn), (y1,. . . ,y,.) 6

Win)"-

By this deﬁnition we require that whenever the “input” vector 37 is more-deﬁned than

or equal to the “input” vector 55, the “output” vector f (3,) is more deﬁned than or

62

.0

equal to the “output” vector f (x) The class of all monotonic functions mapping

(N...)” into (1%)” is denoted by {(Nw)" —»M (Nw)”}.

5.3.2 Properties of Monotonic Functions
The following properties hold for monotonic functions:
1. If f is a unary function, f : N“, —i N”, then f is monotonic if and only if either
a f(w) is w or
0 f(x) is c for some constant c E N and all x 6 NW.
2. For n 2 2, if an n-ary function f, f : ML)” ——> Uta)", is monotonic then either
a f(wl, . . . ,wn) is w or
0 f(x;, . . . , xn) is c for some constant 56 ML)" and for all 53' 6 ML)“.

Monotonicity will guarantee that our results will be predictable from one iteration to

another. We rely on the property of natural extension to ensure monotonicity.

Deﬁnition 5.4 An n-ary function f mapping (1%)” into (1%)" is said to be naturally

extended if f(xl, . . . ,xn) = w whenever at least one of the {135,8 is as.

Natural extension assures us that no undeﬁned computation sequence can map to
a meaningful value. Natural extension also ensures that functions undeﬁned on the

variables they manipulate cannot produce deﬁned results.
Example 5.1 Consider the extension of the decision construct in the following way:

0 if TRUE then 51 else to ﬁ(:i:') is 51(5). When the guard tests true we expect

S1 to be deﬁned and will execute it, regardless of the deﬁnition of S2.

0 if FALSE then no else 52 ﬁ(f) is 52(5). When the guard tests false, we expect
S2 to be deﬁned and will execute it, regardless of the deﬁnition of SI.

63

o if «2 then SI else 52 ﬁ(:i:') is (.0. When the guard is undeﬁned, we cannot

execute S1 or 52 regardless of their deﬁnition. ‘

The deﬁnition of natural extension allows us to apply the Natural Extension

Lemma of Manna [23]:
Lemma 5.1 Every naturally extended function is monotonic.

We have given the operational deﬁnition of our functions in Chapter 4. Now we

show that they preserve monotonicity because we can naturally extend them.
Definition 5.5 Natural Extension of Commands.

s The assignment statement naturally extended to yield the value to whenever its

right hand side is w is monotonic since we have w 4 w.

o The decision statement mapping {TRUE,FALSE} x N” into N” is deﬁned
for any 51, S2 6 L(G) as follows:

51(5) 515(5)::1'5115
52(5) ifg(5:')=FALSE

if 9 then 51 else S2 ﬁ(:E) =

This function can be naturally extended to a monotonic function mapping IB“, x

(Nw)” into ML)” by letting, for any SI, S2 6 L(G),

51(5) if QUE) = TRUE
if Q then 51 else S2 ﬁ(:i') = 52(5) ifg(5;‘) = FALSE
w 219(5) = w

 

‘While this function is not the natural extension of ifLﬁ, we can show it is monotonic by
showing that for input vectors 5." and x’ whenever if -< x’, (if G then 51 else S2 ﬁ)(5:') <

(if 9" then 51' else 52' 5)(&). Let 5 4 a? and assume g = TRUE. Then if 5(5) = 51(5) <
51(5) = 11' 5(5"). Let 5 < 5' and assume a = FALSE. Then if 5(5) = 52(5) < 52(5) = u: 5(5).
Let 5 -< 5" and assume 5 = w. Then if 5(5): 52 < w = if 5(5).

64

o The while do od function mapping {TRUE, FALSE} XN“ into N” is deﬁned
for any S E L(G) as follows:

5(5) ifg(§)=TRUE
5 119(5) =FALSE

while 9 do S od(i:') =

We extend this naturally into a monotonic function mapping IB“, x

ML)" into Wu)" for any S E L(G) by letting

5(5) if 9(5) = TRUE
while 9 do S od(5) = f ifg(;i‘) = FALSE
so if 9(5) = w

Monotonicity is an important property for commands as units and also for com-
mands composed into sequences. Composition allows sequences of functions to be
deﬁned in terms of simpler functions. If f is a function from (A0)” into (1%)” and g
is a function from Mfg)" into ML)“, then the composition off and g is a function from
(1)/w)” into (1%)" deﬁned by g(f(x')) for every 5 in (My)? If f and g are monotonoic
functions, then so is their composition since if f and g are monotonic, and if 5 -< 5."
then f(i") -< f((P), which implies g(f(:i:')) -< g(f(:i”) for all f, at" 6 (1)/w)”. So the

composition of f and g is also a monotonic function.

5.3.3 Least Upper Bound

We are using our functional syntactically to build computation sequences, and se-
mantically as a vehicle to produce a computation sequence. We view commands as
partial functions naturally extended to total functions. We restate “-<” in terms of

functions.

65

Deﬁnition 5.6 Let f, g E {(Nw)” —iM (Nw)”}. We say that g is more-deﬁned than
f, (f -< 9), if f(5) -< 9(5) for all 5 6 ML)“. This relation is a partial ordering an
{(Nw)” —>M (Nw)”} since we have 09 -< f for any f E {(Nw)” -+M (Nw)"}.

Deﬁnition 5.7 Let f, g E {(Nw)” -+M (Nw)"}. We say that f is equal to g, (f = 9),
if f(5) = g(5) for all 5 6 ML)".

Proposition 5.5 f = g if and only iff 4 g and g -< f.

Iff = 9 then dom(f) Q dom(g) and dom(g) Q dom(f), and for all 7 6 dom(f),
7.g = 7.]. Now suppose f -< y and g -< f. Then dom(f) Q dom(g) and dom(g) Q
dom(f), so dom(f) = dom(g). Since g 4 f, for 7 6 dom(g), 7.f = 7.g. But since

f<y.for1 6 dmn(f). 1-9 =1.f. 30 f =9- 0

Deﬁnition 5.8 Let fo,f1,f2, . . ., be a sequence offunctions in {(Nw)” —tM (.M,)"}.
We denote this sequence by {f,}. Then {f,-} is called a chain iffo -< f1 -< f2 -< .. ..

Deﬁnition 5.9 Let {fg} be a sequence offunctions in {(Nw)" ->M (Nw)"}, and let
I 6 {(Nu)" ->M (Nw)"}. We say that f is an upper bound of{f,-} if f.- < f for every
i Z 0. Additionally, iff -< 9 for every upper bound g of {f,-}, then f is called the
least upper bound of {f,-}, denoted lub{f,-}.

The least upper bound of {f,-}, if it exists, is unique since if both f and g are least

upper bounds of {ﬂ}, then f -< g and g -< f so f = g.
Lemma 5.2 hfili [25] Every chain {f,} has a least upper bound.

The least upper bound of a computational chain is the ﬁxed point of the compu-
tation [7]. In our model the ﬁxed point is the ﬁrst state in the computation where the
speciﬁcation is met. In the next section we prove that our computational sequences

are chains.

66

5.3.4 “;” When Viewed As A Functional Is Continuous

Our functional 1' over {(Nw)“ —1M (Nw)"} maps the set of functions {(N..)” ‘75!
(Nw)”} into itself. That is, 1' takes any monotonic function f deﬁned in a given state
7 as its argument and yields a monotonic function r( f) deﬁned in state 7’ as its value.

The properties of monotonicity and continuity are important for 1'. Monotonicity
and continuity guarantee that we can obtain accurate information about the computa-
tion at intermediate stages. Monotonicity ensures that 1' accurately maps a program
statement to its logical successor. Continuity guarantees that this mapping is correct

over an entire computational sequence.
Deﬁnition 5.10 Properties of the functional 'r

I. 1', a functional over {(Nw)" —>M (Nw)"}, is said to be monotonic iff -< g
.mp1... rm < To) for all f, g 6 {war —+M (Aer).

2. The monotonic functional 1' over {(Nw)” ->M (Nw)"} is said to be continuous

iffor any chain offunctions {f,}

1'(lub{f,-}) —:— lub{1'(f,-)}.

Note that since {f;} is a chain and 'r is monotonic, 1'(fo) -< 1'(f1) -< 1'(f2) -< . . .; i.e.,
1'({f,-}) is also a chain. Therefore, by Lemma 5.2, both lub{f,-} and lub{1'(f,-)} must
exist.

We view 1' as the composition operator of known monotonic functions, i.e., for
P0 = So; P6 with So a statement in L(G), and P0, P6 program segments in L(G), Pa =
So; P6 : So; P6 E 1'(Po) = P6. The following theorem shows that 1' is continuous. It

is a variant of a theorem by Manna.

Theorem 5.6 The functional 1' deﬁned by composition of monotonic functions is

continuous.

67

Proof:
If 1' consists of just S, a monotonic function, then 1' is clearly continuous. We
showed monotonicity of program statements by naturally extending them. We show

continuity of 1' for the while e do S od statement. The proof consists of showing

a (i) 1'(while 9’ do S od) is monotonic and continuous for one application of the

statement.

0 (ii) 1'(while 9 do S od) is monotonic and continuous for multiple applications

of the statement.

Proof. of (i).

The proof is in two parts. First, 1'(while 9 do S od) is monotonic, second,
1'(while 9' do S ad) is continuous. That is, you can operate on the least upper
bound of a chain and get the same results as if you operate on the least upper bound
of all of its elements, i.e., continuity perserves limits. Suppose while g do S 0d; and
S = S1;S2; - - - ; Sn is a chain of program statements.

r(while 9 do S od) is monotonic.

If G is initially false or g is undeﬁned, then while (4' do S ad is monotonic by natural
extension, so r(while 9 do S od) is monotonic. Suppose g is true for one application.
Then 1' maps 1'(Sl; S2; - - - ; Sn). We write this

J

T(:("'T[§))°") = T(T"(5))
ntimes
to denote that each Si, 1 S i S n, is mapped to its logical successor by 1'. We assume
that 1'", 1 S i S n, is monotonic because the Si, 1 S i S n, are not iterative, and
show that 1""11 is monotonic. First, if Si 4 Si’, 1 S i S n, then by monotonicity
of 1",1'“,...,'r" we have that rj(Si) -< rj(Si’), 1 S j S n. Then, since by natural

extension while 9 do S ad is monotonic, r‘+‘(1'"(Si)) -< ri+1('r"(Si’)). So 1"“(5i) is

68

a monotonic functional.

1'(while 9 do S od) is continuous.

Now we show that 1' is continuous, i.e., we show that r(lub{Si}) E lub{1'(Si)} for any
chain {Si} within the scope of the while 5 do S od statement. Since Si -< lub{Si}
for every i 2 0 (each command approximates the lub of the chain of commands by
the deﬁnition of least upper bound of a chain), by monotonicity of the functional
1", . . . , 1'" and the while 9 do S od statement, we have 1'(Si) -< 1'(lub{Si}) for every
i 2 0. Therefore, lub{1'(Si)} -< 1'(lub{Si}).

Now let 5 6 ML)". Since the Si, 1 S i S n, are not iterative, we as-
sume that 1'", 1 S i S n, is continuous. We have deﬁned 1'(while 9 do Sod) as
ri+l(,-i(. --1(.S')) . . .) so,
r‘+‘(lub{5i})(s a r‘+'(r‘(- - - (1(1ub{5i}(i’)) - - -))

E Ti+1(lub{Tl(T“l(' ' ' (TH-90(5)» ' ' °))})-
From Lemma 5.2 we know that for every j, 1 S j S 11, there is an i, such that for
every I: _>_ ij:

lub{Tj(Si)}(5) E Tj(Sk)(5).

(every chain has a tub).
Let i0 be the maximum of i1, . . . ,in (we have a series of statements Si). Then for
everyj, l Sj S n:

lub{rj(Si)}(5) z TJ'(52'0)(5),

and so
¢i+1(lub{1"(1'“1('"(T((5i)(5)))"'))l)
a ri+1(1-‘(r"1(-" (7(5i)(5)))”')))

5 ri+1(r‘(r"‘(- - - (1(Si)) ' ' ')))(5)

E 1‘+1(Sio)(5)

-< lub{r‘+‘(5;)}(5)

69

And since 5 was an arbitrary element of the domain,

eruuusm -< whirlwin-

r(lub{Si}) -< lub{1'(Si)}.

This concludes the proof of part (i). It shows that 1' is continuous for all of our
noniterative program statements and for one iteration of the while 9’ do S od. Next

we show that 1' is continuous for multiple iterations of the while Q do S od.

Proof. of (ii)

Let W denote while 9 do S od. From the operational semantic deﬁnition of W
in Chapter 4, we must show that for S a statement in L(G), while 9 do S od;=>
S; while 9 do S od 5 1'(while 9 do S od) = while 5 do S od. That is, 1' correctly
maps the last exectuatble statement within a while loop to the ﬁrst executable state-
ment when the guard tests true.

There are two clarifying remarks we can make about this part of the proof:

1. We will presently deﬁne 1'(while Q do S od) to be

T(f(- - ' T(W)) ° ' ']= T(T"(W))

V

ntimes

 

This is the case where we have termination. From here the proof is very similar
to the previous proof, except that now we have monotonicity of each one of
the 1"(Wi), 1 S i S n, and we use this to show that 1'(while 9 do S ad) is a

monotonic functional for multiple iterations.

70

For continuity, when showing that
lub{1'(Wi)} -< 1'(lub{Wi}),

we recognize that {Wi} -< lub{Wi} instead of that Si -< lub{Si} as we did

previously, because each occurrence of 1'(Wi), 1 S i S n, is now a chain.

2. Finally, we must show that the result holds in the general case when 1' contains

any number of occurrences of W.

The proof is in two parts. First, 1(while g do S od) is monotonic, sec-
ond, 1'(while 9 do S od) is continuous for multiple applications. Suppose
while g do S od = W, and g is true for multiple applications.

1'(while 9 do S od) is monotonic.

Since 9 is true for multiple applications, 1' maps 1'(W1; W2; - - . ; Wn). We write
this

r(r(- - ~1-(W)) - - -) = new»

ntimes

to denote that each Wi, 1 S i S n, is mapped to its logical successor by 1'. This
assumes that the loop terminates. In the previous proof we showed that 1'(W) is
continuous for one application, therefore it is monotonic, since continuity ensures
monotonicity. For each i, 1 S i S n, Wi is continuous, so 1'i is monotonic for each
i, 1 S i S 11. Now we show that 1"“(Wi) is monotonic. First, if Wi -< Wi',
1 S i S n, then rj(Wi) 4 rj(Wi’), 1 S j S 11. By natural extension, the function
whileg do Sod is monotonic, so r‘+1(r‘(Wi)) -< 1"+1(1'"(Wi’)). So 1"“(Wi) is
monotonic over 11 applications.
1'(while 9 do S Cd) is continuous over n applications.

That is, 1'(lub{ Wi}) E lub{r(Wi)} for any chain {Wi} (multiple applications of the

while g do S od statement). Since {Wi} -< lub{Wi} for every i Z 0, by monotonic-

71

ity of the functional 1'", 1 S i S n, and the while g do S od statement (from the pre-
vious proof, they are continuous therefore monotonic), we have 1'(Wi) -< 1'(lub{ Wi})
for every i Z 0. Therefore, lub{1'(Wi)} -< 1'(lub{Wi}).

Now let 5 E (1%)". We know 1", 1 S i S n, is continuous (therefore monotonic),
and since 1(Wi) is deﬁned as 1".“(1"'(---1'(W))- - ):
T‘+‘(’ub{Wi})(5) E T‘+‘(T‘(' ° ' (T(lub{Wi}(5)) ' ' °))

2 r‘+'(tub{r‘(r'-'(~- «(wean-~11».

From Lemma 5.2 we know that for every j, 1 S j S 11, there is an i,- such that for
every I: 2 ij:

Iub{~ri(wz')}(5) a ri(w1c)(5).

(every chain has a lab).
Let in be the maximum of i1, . . . ,i,, (we have a series of statements Wi). Then for
everyj,1 Sj S n:

lub{rj(l"Vi)}(5) E rj(l’Vio)(5),

and so
r‘+1(lub{1"(r"‘(--'(T((1‘Vi)(5)))”'))}l
E Ti+1(ri(r‘-1(---(1(Wi)(f)))-~)))

E 7i+1(ri(r‘-‘(- - - (1(Wi)) - - -)))(i")

E 1"+1(Wio)(5)

4 lub{r‘+‘(Wi)}(a‘=’)

And since 5 was an arbitrary element of the domain,

Ti+l(lub{l/Vi}) ‘4 [UbiTi+l(Wi)}

1'(lub{Wi}) 4 lub{1'(Wi)}.

72

This shows that 1'(W) is continuous for 11 applications, with n ranging over the

natural numbers since 11 is arbitrary. Cl

5.3.5 Fixed Points of the Functional 1'

Fixed points of continuous functionals are states in a computational chain where the
speciﬁc purpose or goal of the computation is met because they represent the best
approximation to the limit of the computation [7]. Formally, let 1' be a functional
over {(NL)” -+M (Nw)”}. We say that a function f 6 {(Nw)” -+M (Nu?) is aﬁxed
point of 1' if 1'(f) = f. If f is a ﬁxed point of 1' and f -< 9 for any other ﬁxed point g
of 1', then f is called the least ﬁxed point of 1'.

1' is a continuous functional over {(Nw)" -—»M (Nw)"}. Let 1'°(w) = o; be the totally
undeﬁned function. Consider the sequence of functions r°(w), 71(0)), 72(w), . . ., where
1"“(52) is 1'(1"(w)) for i Z 0. Each function 1‘(w) is a member of {(Nw)” -*M
(1%)”). By deﬁnition, to -< 1(5)), and since 1 is monotonic (it is continuous, therefore

monotonic), {1"(w)} must be a chain. That is:

w<r(w)<r2(w)~-.

So by the least upper bound lemma, liib{rl(w)} must exist. That is, for the continuous
functional 1' over {(Nw)" —>M (Nw)"}, the sequence {1"(w)} is a chain and has a least
upper bound.

Because of this property, we can invoke Kleene’s First Recursion Theorem.

Theorem 5.7 [First Recursion Theorem]

The continuous functional 1' has a least ﬁxed point that is the least upper bound of

{T‘(w)}-

Denote the least upper bound of {1"(w)} by f p,. f p, is a ﬁxed point of 1' because 1'

73

is continuous so

7(fP1) = 1'(lublr'lwl) = lub{T‘+‘(w)} = lul){T"(w)} == fPr-

f p... is a least ﬁxed point of 1' as well, i.e., f p, -< 9 for any ﬁxed point 9 of 1'. First of all,
1'°(w) = w -< 9. Then, if 1'“1(w) -< 9 for some i 2 1, since 1' is monotonic (because 7
is continuous) and g is a ﬁxed point of 1', we have that 1"(10) = 1'(1'“1(w)) -< 1(g) = g.
30 r‘(w) -< g for all i Z 0. This implies that g is an upper bound of {1"(w)}, but
since fp, is the least upper bound of {r‘(w)}, it must be that fp, -< g.

We have deﬁned operational syntax that constructs computation sequences using
the functional “;” that we have proven is continuous for all of our program statements.
This gives us the existence of a least upper bound for any sequence because we have
deﬁned our state space to be a complete lattice with 0 the least element. Note that
0 -_'=. FALSE -'._=. J. E [l -_=. w are used to represent undeﬁned at the various levels of
abstraction in our environment. Thus, even for partial functions for which no value
is deﬁned, we have that lub{} = FALSE, and for partial functions deﬁned on their
input and for all total functions, lub{O} = 7 6 P (where 0 represents a nonempty

sequence), which by deﬁnition has a descriptive logical sentence.

CHAPTER 6

The wpw Predicate Transformer

The wp predicate transformer uses the initial state/ ﬁnal state pair to reason about
correctness. In this model all program statements are atomic, even loops. While the
semantics of the wp predicate transformer allude to execution of a loop, the proof
of termination ignores it by focusing only on ﬁnal results. The class of functions
addressed by the wp method is the primitive recursive class. It is an easy exercise
to show that all primitive recursive functions are computed by bounded loop pro-
grams [4],]22],[26].

Our interest is in verifying the correctness of unbounded loop programs. Whereas
bounded loop programs require a given number of applications of a loop to its argu-
ments and then terminate, unbounded loop programs correspond to repeated appli-
cations of a loop to its arguments until some condition of the arguments is satisﬁed.
Unbounded loop programs are deﬁned by each iteration of the loop, as Sommerhalder

and van Westrhenen formalize [22].

Deﬁnition 6.1 The i-iteration of a function f is a function from (1%)“ to 0%,)"
denoted by fv" and deﬁned as follows.

I. Let V,(5) é {mlfm(5) is defined}.

That is, V,-(5) is the set of indexes m such that f(5) is deﬁned form iterations.

74

75

2. Let minV,(5) denote the least element of V,(5). Then f“ g A5[if (571(5) at 0
and f'”(5) l for all m S min V,(5)) then f'"“‘ “(5) else T].
Note that the ﬁxed point, fv‘(5), is the least upper bound of a well ordered

sequence of approximations that deﬁnes the loop.

In our model loops are not atomic because each iteration is represented as an
element in the computational chain. Dijkstra applied his iterative function to its
variables once and obtained a single predicate as his result, enabling him to deﬁne
iteration as a recurrence relation between predicates. We apply the iterative function
repeatedly, each time to updated values of the variables, and obtain a new predicate
at each iteration. In essence, we iterate through a family of functions. Because of
this we need a series of maps from predicate to predicate, so we deﬁne iteration
as a recurrence relation between predicate transformers. At this point Dijkstra’s

“. . .the semantics

statement about the difﬁculty of general recursion becomes clear:
of a repetitive construct can be deﬁned in terms of a recurrence relation between
predicates, whereas the semantic deﬁnition of general recursion requires a recurrence

relation between predicate transformers. This shows quite clearly why I regard general

recursion as an order of magnitude more complicated than just repetition” [l].

6.1 Macros

Writing programs that use only subscripted elements of a program vector can be
tedious. More importantly, because we wish to express the set of predicates that
describe each element of a computational chain, we need notation to distinguish
them. Like Hehner [8], we use the convention of inventing a name for a program
segment, using the name in place of the segment, and specifying the text of the
segment elsewhere. We use these names directly in our speciﬁcations to reason about

the code segment the speciﬁcation describes. Hehner referred to the use of a name

76

in place of some statement as a “call.” We use the term “macro.” In both cases
the process is one of simple inline code substitution. Hehner used his call names
as placeholders in a recursive reﬁnement. We use our macro names directly in our
speciﬁcations to reason logically about the correctness of the program segment that

uses them.

Example 6.1 The program Q = (p, k,n,P) = (2,1,4,x4 := x3;x1 := xg;while x1 74
0 do x1 := x1 +1;x4 := x441; od;end.) adds the value Of$2 to the value ofx1.

We allow giving variables arbitrary names that are strings of characters beginning
with a character. All of the registers used must be listed in a header that names the
macro. The program variables naming the registers must be listed in a speciﬁc order:
output variables ﬁrst, next input variables, last local variables.
macro ADD(registers: sum, x, 1 ,count);

count := y;

sum := x;

while count 31$ 0 do

sum := sum + 1;
count := count-11;

od;

To convert a macro into the program segment it represents, number the variables
in the register list upwards from 1 in the order given. Remove the header with the
register list.

To transform macro ADD into the code segment it represents:

1. Number the variables in the register list: sum = x1, x = xg,y = x3,count = x4.
2. Remove the header with the register list.

3. The program sequence is:

x., := x3; 4: count := y;

77

1'1 3: 1'2; 4: sum :2 x;

while x4 2,19 0 do (it while count at 0 do
x1:= x1 +1; (1) sum := sum +1;
x4 := x441; {it count := count-Ll;

od; 4: od;

Each occurrence of a macro name in a program sequence must be converted to the

program segment it represents before it is executed. To make use of a macro name in

a program we use a macro statement: x := ADD(x,y).

6.1.1 Syntax of Macros

Macros involve simple in-line substitution of program text. Macros may be composed
of any legal statement in our language. The syntax of a macro is:
macro< string > (registers : < stringl >, < string; >, . . . , < stringn >);

< sequence >;

< string >::=< character > I < string >< character > I < string >< numeral >

< character >::= AIBI - - - |Z|a|b| - - - |z

The macro statements are:

a (21,...,zk) := f(l‘un-s-Tp),

o (21,...,zk):= (21,...,zk)+f(1’1.---,$p),
a (21,...,zk) := (21,...,zk)4f(x1,...,xp),

where f : IN” —1 IN" is a computable function. The above macro statements stand for

a sequence P computing the function value f(x1,..., x,,) = (y1, . . . , yr) and assigning

78

the values of the variables y; to the variables 2,, 1 S i S k. The values of all other

variables occurring in the program containing the macro statement remain unchanged.

6.1.2 Use of Macro Names

We use macro names directly in our speciﬁcations. Macros allow us to name speciﬁc

code sequences.

Example 6.2 Suppose we have this code sequence:
S 1 ;
S2;

Sn;
We can name the sequence 51; S2; - . - ; Sn “S” and we can verify the correctness of

S by verifying the correctness of SI; S2; - - - ; Sn.

A transformation of a macro name to the code it represents consists of a direct
substitution of the code sequence for the macro name in such a way that side effects
are not allowed. A macro names the partial function computed by the code sequence
the macro represents. We reason about the correctness of a computation of the partial
function with the preconditions and postconditions we write for the code sequence
that computes it. Because a macro represents this code sequence, the preconditions
and postconditions of the code sequence are preconditions and postconditions for the
macro.

When we use a macro to name a partial function in a computational sequence, we

may interpret the function name as a predicate.

Example 6.3 Consider a representation of a computational chain of a simple code
segment, with precondition Q, invariant I, and postconditions Hi, 1 S i S 5. This

small program, similar to Example 6.1, is composed of two sequential statements (SI

79

and S2), followed by a loop containing statements S3 and S4 that executes twice. The

postcondition of the loop is R5.
{Q}SI; {R1}S2; {R2}{I}S3; {R3}S4; {R4}{I}S3; {R3}S4; {R4}{R5}

A macro will allow us to name a piece of code, say P = S3; S4 and verify its correct-
ness once. When we verify the entire code segment, we can substitute this name in
a computational chain. For veriﬁcation of the entire code segment the computational

chain becomes

{Ql51;{131}52; {R2}{IIP;{1}P;{R5}

We can write a postcondition asserting the correctness of the macro since we have
veriﬁed it elsewhere, say R5’ (because each execution of P should provide a better

approximation to the state where R5 is fulﬁlled ), and the computational chain becomes
{Ql51;{31}52; {RP-HOP;{R5'I{I}P;{R5'I{R5}

Since our computational chains are well-ordered we have a structure we can investi~
gate inductively. The result is a logical and consistent method for reasoning about

bounded, unbounded, and nonterminating computations.

6.2 The wpw Predicate Transformer

We denote our predicate transformer wpw. Like the wp predicate transformer our
wpw predicate transformer is a conjunction. The wp predicate transformer is a con-

junction of termination and partial correctness [I], [19]:

wp(A, R) E wp(A, TRUE) A wlp(A, R).

80

wlp(A, R) states that the computation will be correct if it terminates. wp(A, TRUE)
guarantees that the computation will terminate after a predeﬁned number of itera-
tions of any loop [1].

Our wpw predicate transformer includes the wl p predicate transformer which takes
a command and its postcondition as arguments because the wlp predicate transformer
asserts that the postcondition will be fulﬁlled if the command terminates.

The other conjunct of the wpw predicate transformer expresses incremental cor-
rectness. This conjunct deﬁnes a recurrence relation on an ascending chain of pred-
icate transformers. For noniterative commands, the chains are composed of a single
element and the arguments to the predicate transformer of that element are the com-
mand and its postcondition. For the iterative command the chains may be ﬁnite
or inﬁnite. The arguments to the predicate transformers in the chains of predicate
transformers are the command obtained by combining the statements of the guarded
command and the logical assertion of the command’s speciﬁcation. We interpret this
assertion as a logical approximation to the predicate describing the limit of the com-
putation for each iteration. Each appearance of this assertion in a computational
chain represents the least upper bound of a subchain within the chain, and describes
the most recent member of the family of functions to execute. We describe this as-
sertion by appending a prime (I) to the letter we use to represent the postcondition
(see Section 2.4).

We adopt the same semantic deﬁnition for statements where termination is not an
issue as Dijkstra, except that the semantic deﬁnition of our decision construct reﬂects

its deterministic nature. The semantic equations for our noniterative commands are:
1. Assignment: wpw(“x := e”, R) = R:

2. Sequencing: wpw(“S1;S2”, R) = wpw(“Sl”, wpw(“S2”, R))

3. Decision: wpw(“if Q then S1 else S2 ﬁ”, R) = 9 => wpw(“Sl”, R) A «9 =>

81
wpw(“S2”, R)

4. wpw(“end.”, R) = R since end., like Dijkstra and Gries “skip” is a no-op.

6.2.1 Formal Deﬁnition of an Unbounded Loop

Let WH I LEDO represent the command while 9 do S 0d. Let IF represent the
command if Q then S ﬁ. The formal semantic deﬁnition of our looping command
is given by cases using the predicate Ik(R) which describes the set of all states from
which WH I LEDO can execute k times leaving R true.

Deﬁnition 6.2 For guard Q, postcondition R, and approximation R’:

s 10(R) = FALSE. This predicate represents the set of states before the guard is

initially tested.

a Ik+1(R) = Ik(R) V wpw(IF,Ii.(R’)), k > 0. This predicate represents the set of
all states from which WH I LE DO has executed correctly k times such that either
so A R’ A R after I: iterations or g A R’ A -1R, i.e. either the loop has terminated
and R is true (Ik(R)) or another interation is required (wp(IF,Ik(R’))).

Note the similarity between this notation and Dijkstra’s notation [1]. The principal
difference is that our chains are ascending, while Dijkstra begins with a descending
chain that he proves is bounded from below by zero, since he always assumes ter-
mination a priori. Given this deﬁnition we can deﬁne our semantic operator for our

iterative command.
Deﬁnition 6.3 wpw(lVI-IILEDO, R) = (Vk: k > 0 : Ik(R)).

This deﬁnition says that either termination and Ik_1(R) is true or the computation

is correct to this point and one more iteration is needed wp(I F, Ik-1(R’)).

6.2.2 Incremental Progress

In the deﬁnition above we gave the formal deﬁnition of a loop in terms of the chain
of predicates that describe the computation. Next we propose a deﬁnition for a loop
in terms of the predicate transformers we use to evaluate the chain of predicates. We

will show that this proposed deﬁnition exactly deﬁnes the semantics of a loop in our

model.

Deﬁnition 6.4 Incremental Progress

wpw(WHILEDO, R) E wp,(S, R2) A wlp(WHILEDO, R),i = 0,1,2, . . .

where wp,-(S,R§) E wp(S, TRUE) /\ wlp(S, R2).

This predicate transformer captures the meaning of our formal deﬁnition be-
cause it addresses the situation where termination has occurred and R is realized
(wlp(WH I LEDO,R)) [1],[19],[6]. It also addresses the situation where more itera-
tion is required (wp;(S, R[)) but the computation is correct to this point. In this case
the statements within the loop have executed i times, and for each discrete execu-
tion j, l S j S i, we have reached a state that represents the least upper bound of
the computational subchain induced by those statements. Each of these least upper
bounds has a predicate logic sentence identiﬁed by the predicate Rg.

Continuity of our computational chains ensures we can obtain better and better
approximations to a computation’s limit as we map from predicate transformer to
predicate transformer. We will show that at each ﬁxed point the command of our
predicate transformer is more deﬁned than its predecessor because its nucleus is larger.

Monotonicity ensures that wp-1(S, R’l) => => wp,_1(S, Rf_,) => wp;(S,R:-) => -- -.

83

Theorem 6.1 Incremental Progress Theorem

wpw(WHILEDO, R) a wp,(5,12:.) A wlp(WHILEDO, R), i: o,1,2,...

where wp;(S, R:) E wp(S, TRUE) A wlp(S, R:).
Proof. Induction on i, the index of a state in a computational chain.

0 Basis: i = 0. This is the initial state before execution, described by 0, the
minimal element in our lattice. Since S has not executed, R3 = no, so
wpw(WHILEDO, R) = wp0(S,w) A wlp(WHILEDO, R)

= w A wlp(WHILEDO, R)

= {}
= FALSE

0 Hypothesis: We assume that for each index i > 0 in the chain, we have
that S executes once, i.e., wp(S, TRUE) and for that execution we know that
wlp(S, R:). Thus, because of the structure of our state space and by continuity of
computational chains, we have N(S‘) = (S’)(S‘)"l = wpg(S, 12:), i.e., our initial
states were such that after i iterations R:- is true, and iterated composition of S
with itself produces a nucleus of states that map into the lub of the chain, the

state described by R:.

0 Case A: Index i is the tub of the entire computation, i.e., the loop has
terminated. In this case we have Invariant A R:- A pg => R, since R: is
met and the loop has terminated we certainly have wlp(WHILEDO, R),
so wpw(WHILEDO, R) E wp(.(S, R:) A wlp(WHILEDO,R),O S k S i.

0 Case B: Index i is the lab of a subsequence of the entire computa-
tional chain, i.e., the loop has not terminated and R:- is an approxima-

tion to R. wlp(WHILEDO,R) insures partial correctness of the loop;

84

it is the set of initial states from which R will be satisﬁed if the com-
putation terminates. We have already shown by continuity of computa-
tional chains that wpk(S,R’k),0 S k S i, therefore to this point we have

wpw(WHILEDO, R) E wpk(S, R1.) A wlp(WHILEDO,R),O S k S i.

a Show: wpw(WHILEDO,R) E wpg+1(S,R:-+1) A wlp(WHILEDO, R). By
continuity of computational chains one more iteration of the loop produces the
result we need, because by iterated composition of the command S with itself
we have N(S‘“) = (S"S)(S’S)‘1 = wpg+1(S, R:+,). The two cases, either i +1
is a ﬁnal state or i + 1 is a non-ﬁnal state, are the same as we asumed in our
hypothesis, with i+ 1 replacing i. So wpw(WHILEDO, R) E wpg+1(S, R2“) A
wlp(WHILEDO, R), i = 0,1,2,. .. .

6.2.3 Pr0perties of the wpw Predicate Transformer

Like Nelson [6] and de Bakker [5] we eliminate Dij kstra’s Law of the Excluded Miracle:
wp(S, FALSE) = FALSE because nonterminating computations return an empty
set of ﬁnal states. There are other properties that are important to our reliance on

computational chains for verifying the correctness of programs.

a Property 1a: The predicate transformer wpw is monotonic for terminating

loops. Let (Q’ A Q) => (R’ A R). Then

wpw(S. (Q' A 62)) => wpw(S. (3 A R))-

Proof: (Q’ A Q) A (R’ A R) = (Q’ A Q). Therefore
wpw(S. (Q’ A 62)) = wpw(S, (Q’ A Q) A (R’ A R))
= tva(5, (Q’ A Q)) A wpw(S, (R’ A R))
=> wpw(S, (R’ A R)).

85

a Property 1b: The predicate transformer wpw is monotonic for nonterminating

loops. For iterations i and j, with i < j, let Q: => Q:. Then

wp'w(3.QZ-) => wpw(5.Q§-)-

Proof: Q: A Q:- = Q:. Therefore
wpw(S. as) = wpw(s, o: A c231
= wpw(S. on A wpw(s, (2;)
=> wpw(S. Q3)-

0 Property 2a: The wpw predicate transformer is continuous for terminating

loops.

wpw(S, Q’ A Q) V wpw(S, R’ A R) = wpw(S, (Q’ A Q) V (R’ A R)).

Proof:

(=>): Let 7 6 wpw(S,Q’AQ) or let 7 E wpw(S, R’AR). Then 7 6 wpw(S,(Q’A
Q) V (R’ A R))-

(<=): Let 7 6 wpw(S, (Q’ A Q) V (R’ A R)). Then either 7 E wpw(S, Q’ A Q) or
7 e wpw(S, R’ A R), or both. If both, then we are done. If 7 e wpw(S, Q’ A Q)
then 7 E wpw(S,(Q’ A Q) V wpw(R’ A R). If 7 E wpw(S,R’ A R) then 7 6
wW(5,(Q’ A Q) V (R‘ A R))-

0 Property 2b: The wpw predicate transformer is continuous for nonterminating

loops. For iterations i and j, with i < j:

wpw(S. on v wpw(s, as) = wpw(s, o:- v C23).

86

Proof:

(=>): Let 7 E wpw(S,Q:) or let 7 E wp-w(S,Q:-). Then 7 6 wpw(S, Q: V Q:).
(4:): Let 7 6 wpw(S, Q:VQ:). Then either 7 E wpw(S, Q:) or 7 E wpw(S,Q:),
or both. If 7 is in both, then we are done. If 7 6 wpw(S,Q:) then 7 E

wpw(S,Q:)prw(s,Q;-). 117 e wpw(S, as) then 7 e wpw(s.os)prw(s.Q:-).

Property 3a: The wpw predicate transformer distributes over conjunction in

a terminating computation.

wpw(S, Q' A Q) A wpw(S, R' A R) = wpw(S, (Q' A Q) A (R’ A R)).

Proof:

(=>): Let 7 E wpw(S, Q’AQ) and let 7 E wpw(S, R’AR). Then 7 E wpw(S,(Q’A
Q) A (R’ A R)).

(<=): Let 7 E wpw(S,(Q’ A Q) A (R’ A R)). Then 7 E wpw(S, Q’ A Q) and
7 E wpw(S, R’ A R). Therefore, 7 E wpw(S, Q’ A Q) A wpw(S, R’ A R).

Property 3b: The wpw predicate transformer distributes over conjunction in
nonterminating computations, provided that the index range of the predicates
it takes as arguments is not empty. This restriction ensures we cannot map an
undeﬁned intermediate state to an deﬁned state. For iterations i and j, with
i < j:

wpw(S, Q:) A wpw(S, Q:) = wpw(S, Q:- A Q:).

Proof:

(=>): Let 7 6 wp'w(S,Q:-) and let 7 E wpw(S,Q:). Then 7 6 wpw(S,Q:- A Q:).
(<=): Let 7 E wpw(S,Q: A Q:). Then 7 E wpw(S,Q:) and 7 6 wpw(S,Q:).
Therefore, 7 E wpw(S, Q:) A wpw(S, Q:).

87

6.2.4 Relationship Between I, R’, and R.

The logical relation between the invariant (I), the approximating predicate (R’), and
the postcondition (R) of a loop is implication: I => R: => R5, => - - - => R whenever a
loop is terminating.

If the loop is bounded then the invariant and the approximation may be the same.
This work is not intended to address this case because it has been fully explored by
others, and, given that we have a priori knowledge of the moment of termination, an
approximation to the postcondition is superﬂuous. We have the fact in advance that
the postcondition is the loop’s speciﬁcation and that it will be fulﬁlled. This research
is valid for this case because R’ can certainly be deﬁned, but is intended to be used
beyond the primitive recursive class of functions.

If a loop is unbounded but terminating (it computes a total recursive function), it
is “controlled” by a Boolean guard that is a logical sentence describing the condition
of the loop’s variables (usually the condition we expect them to be in at termination).
It may be the case here that several iterations are required before anything nontrivial
can be said about the loop’s variables. The example we give in Chapter 7 of a total
recursive function is a good example of this phenomenon. Before the loop iterates
at all the only variables it manipulates that we can comment on are the variables
set elsewhere in the program. But one pass of the loop allows us to say much more
because the loop has been able to compute a partial solution and set its variables to
reﬂect this.

Where the invariant of a loop deﬁnes upper and lower bounds for some variables in
the loop, the approximating predicate allows us to be more speciﬁc. First, it enables
us to pinpoint the values within the bounds set by the invariant (for those variables the
invariant can describe). Second it allows us to make a statement after each iteration

about the variables involved with the guard of the loop (that the invariant may not

88

apply to). Third, it allows us to make a statement about the variables speciﬁc to the
computation but not involved with the guard or the invariant. We do this by showing
that each pass leaves I A R’ = TRUE.

If the loop is nonterminating then its postcondition is FALSE. The approxima-
tion predicate, true after each iteration, allows us to actually say something about the
variables (Dijkstra could say nothing, Nelson could say FALSE, which is not very
useful). In this case the relationship between the invariant and the approximation is
still implication. The postcondition is not involved because it will never be reached.

Technically, it doesn’t exist. We have: I => R’1 => R: => - - -

CHAPTER 7

Application of the wpw Predicate

Transformer

7 .1 Description of the Method

We use the Incremental Progress Theorem to help us develop programs that compute
recursive functions. The wp calculus method of predicate transformers is the moti-
vation for our method and, while we have extended the range of programs for which
proofs of correctness can be written using our method beyond what the wp calculus
can do, we have attempted to design a method that is easy to use.

The concept of an invariant is fundamental to the correctness of all loops, bounded
and unbounded. We write Invariant A g => wpw(I F, Invariant) to mean that one
execution of the guarded command list S encompassed by while 9 do S ad, which
is equivalent to executing if Q then S ﬁ one time will not affect the truth of the
invariant, provided it is true before execution commences. Given this, any number of
iterations leaves the invariant true. Furthermore, since the invariant is independent
of the guard of a loop it remains true if the loop terminates.

Our proof of correctness method addresses the truth of the loop invariant, both

before execution and after each increment. Our proof of correctness method also

89

9O

recognizes the important role of the speciﬁcation of the code that comprises the loop
body (the approximating predicate). Since it is the deﬁnition of the purpose of the
code within the loop it must be fulﬁlled after the ﬁrst iteration and remain true for
all subsequent iterations. Finally our method recognizes that in conjunction with
the invariant of the loop and a false guard the speciﬁcation of the loop body implies
the truth of the postcondition. Unfortunately, in this class of functions termination
cannot always be predicted and so in the face of nontermination, we depend on the
truth of the conjunction of the invariant and the speciﬁcation of the loop body at
each ﬁxed point in the computational subchain to verify that our code can execute
correctly as written.

To prove correctness using our method it is necessary to show the truth of the
entites we have been discussing for every loop. We provide a checklist so that a pro-

gram developer can be certain that nothing has been forgotten.

Checklist for showing correctness of a loop:

1. Show that the invariant (I) of the loop is true before execution of the loop

begins.

2. Show that an execution of the loop body terminates with the invariant of the
loop and the speciﬁcation of the code within the loop both true. For postcondi-
tion R and the approximation to R, R’, this means show that I A R’ = TRUE.
R’ is an approximation to the postcondition R. It is obtained by combining
the postconditions of each statement within the loop by conjunction, and then

simplifying the predicate logic sentence that results.

3. Show that if termination occurs the postcondition is true, i.e., show that I A

R’A-Q=>R.

91

4. For S (the statement list within the scope of the guard) show wp;(S,R:),i =
1, 2, . . ..

7.2 Examples

Code for the programs we use may be found in Section 7.3 at the end of this chapter.

7.2.1 Proof of Correctness of a Total Recursive Function

We demonstrate our method on a total recursive (but not primitive recursive) func-
tion. The program that computes this function requires an unbounded loop, so even
though it terminates, the methods of Dijkstra and Gries cannot be used to prove that
it is correct.
We write gm(x) for the result of composition of g with itself m times. In particular,
9°(z‘) = 1%
f(x) = 906).
92(3) = g(9(a=)).
and so on. In general we can write this as the recursion
9°(x) = x,

y'"“($) = 9(9’"(1‘))-

For the function we want to compute we deﬁne

x+l ifx=00rx=1
fut”):

x + 2 otherwise,

fn+1(1‘) = f§(1)- Where fn+1(€v) = 5(1) = fn(fn ' ' ' (fn(1))'°°)

.1: times

A basic property of this function is given by a lemma found in Davis and Weyuker [26].

Lemma 7-1 fn+1(33 '1' 1) = fn(fn+1(1'))-

Proof:
fa+1(x +1) = fif“(1)
= fn(f.f(1))
= fn(fn+1(1‘))

With this lemma we can show that f,,(x) = A(n,x):

fi+1(-’L' +1) = f£(f£+1($);

and

A(i+1,x +1) = A(i,A(i+1,x)).

For the base cases we have

A(i,0) = 1 = f;(0)

x+l ifx=0,l
A(Oa'T): =f0($)
x+2 ifx>1.

The recursively speciﬁed function A(i, x) is a variant of a function introduced by W.
Ackermann.

We note that fn(0) = 1,71. 2 O and fn(1) = 2,n Z 0 since f,,(1) = f,,_1(1) =
- - - = fo(1) = 2. We can prove that this function is total by showing that f,,+1(x) =
f,,(fn - - - (fn(1)) . - ) = ff(l), for all n 2 1 and x _>_ 0, i.e., the function is deﬁned on
all of its arguments. We demonstrate that it is computable by giving an algorithm that
computes it and showing the proof of correctness using our method. We demonstrate
that this function is not primitive recursive by the fact that it contains an unbounded
loop. We must use an unbounded loop because the function f,- is monotonically
increasing for all i Z 1, i.e., we cannot ﬁnd an a priori upper bound for the function

in general because the runtime is dependent on the index of the function for all indices

93

greater than or equal to one.

We present our algorithm in the form of a macro to make it more easily readable.
See Figure 7.1 in Section 7.3. The program calls one small macro that represents the
base case of our functional speciﬁcation, see Figure 7.3. The program calls the macro
that computes values other than the base (see Figure 7.2) from within a bounded
loop.

We prove the correctness of macro F1111. In this proof we show how our method
works for bounded and unbounded loops, assignment statements, sequencing, and
decision statements. Once the correctness of macro F M 1 is shown, the proof of the
bounded loop in macro Examplel in Section 7.1 is an easy exercise of the notation.
The sequence operators II and V have been deﬁned in Chapter 4, Section 4.2.1 and
Section 4.2.2. We use them here to manipulate a register we call Stack.

Proof of the bounded loop:
j := 0; i := i — 1; x :=]]’Stack; x := x — 1;
{Pre :j = 0 A pushing > 0}
{IzOSjSpushingAOSxSm—I}
{Bound : t = pushing — j}
whilej < pushing do
Stack := x [I Stack;
i := i + 1;
i ==j + 1;
{R’:1SjSpuslzingAStack:,-=x:i—jSiSi+j}
od

{R :j = pushing A Stack,- = x : i — pushing S i S i + pushing}

1. Show that the invariant I is true before execution of the loop.

94

o wpw(“j := 0”, 0 Sj S pushing)
a 0 S 0 S pushing

a TRUE

2. Show that an execution of the guarded command terminates with I A R’ true.
a wpw(“Stack := x l] Stack;i:= i+1;j :=j+1”, 0 S j S pushing Al S
jSpushingAStackgzxzi—j SiSi+j)
s wpw(“Stack := x [I Stack;i := i+1”, wpw(“j := j + 1”, 0 S j S
pushingAStackgzxzi—j SiSi+j))
o wpw(“Stack := x I] Stack”, wpw(“i z: i+ l”, 0 S j +1 S pushing A
(Stack;=x:i—j+1SiSi+j+1)=w)
s wpw(“Stack := x H Stack”, 0 S j+ 1 S pushing A (Stacie-+1 = x :
i+l—j+1 Si+1Si+1+j+1)=co)
a O S j S pushing A Stack,- = x : i -j S i S i+j. Implied by the invariant.
3. Show that upon termination the postcondition is true, i.e., show that I A R’ A
“(9) => B.
a 0 Sj S pushingAl Sj S pushingAStack; = x : i-j S i S i+jA-1(j <
pushing) => j = pushing A Stack,- = x : i — pushing S i S i + pushing.

a j = pushing A Stack,- = x : i — pushing S i S i+ pushing.
4. Show wp,(A,R:),i=1,2,...

0 Basis: If the index of the computational chain is 1 then we have executed
once and j = 1 and by 2 we have that 0 S j S pushing A Stack,- = x :
i—jSiSi+j. Sol SjSpushingAStack;=x:i—jSiSi+j.

o Hypothesis: Assume for index k > 1 that 1 S j S pushing A Stack,- =

x:i-—jSiSi+j.

95

0 Show: For index k + 1.
Case A: j = pushing. Then termination has occurred and by 3 we have ‘
that I A R’ A “(9) => R, i.e., j = pushing A Stack,- = x : i— pushing S
i S i + pushing.

Case B: j < pushing. Then the computation has advanced one more step
and by2 wehaveO Sj+1SpushingAStack,-+1 = x :i—j+2 Si+l S

i+j+2, i.e., 0 Sj SpuslzingAStackg+1 = x : i+1—j S i+l S i+l+j.

Proof of the major IF...FI statement:

if top 2 1 then

{j = pushing A Stack,- = x : i — pushing S i S i + pushing}

else

val := val + F0(1);
ﬁ
{(I = pushingAStack, = 33 i i—pushing S i S i+Pushing)V(top = 0Aval =
val+ F0(1))}
Proof:
wp(IF...FI,R’) = (top 2 1V top = 0)/\

s (top 21=> wp(“IF...FI”,j = pushing A Stack,- = x: i—pushing S i S

i + pushing)A

(top = 0 => wp(“val := val + F0(1)”, val = val + F0(1))

TRUEA(top _>_ 1 =>j = pushingAStack, = x : i—pushing S i S i+pushing)

A(top = 0 => val = val + F0(1))

TRUE A TRUE A TRUE.

96

Proof of the unbounded loop:
i := 1; Stack := index || Stack; x := index;
{Pre:Stack1 = m — 1 A val 2 0}
{IziZOAOSxSm—I}
{Bound : none}
while i at 0 do

if top _>_ 1 then
else

6

{(j = pushingAStack; = x : i—pushing S i S i+pushing)V(top = OAval =
val+ F0(1))}
i := i - 1; top :=[]’Stack;

{R’:(top=0Aval=k*F0(1):l S k Spushing)V(top21AStack,- =x:

i —pushing S i S i + pushing)}

od

{R : i = 0 A val = pushing =1: F0(1)) and pushing * F0(I) = FO”““”‘9(1)

1. Show that the invariant I is true before execution of the loop.

0 = 0 S x S m — 1 is true by the Precondition of the loop, since the stack

only holds the value m — 1.

a = TRUE.

2. Show that an execution of the guarded command terminates with I A R’ true.

a wpw(“IF...FI;i:=i— 1”, IAR’)

97

s = wpw(“IF...FI”, wpw(“i :2: i — 1”, IA R’)
s = wpw(“IF...FI”, IA R’)

a 2 (top 2 lAj = pushing A Stack,- = x : i -pushing S i S i+pushing) V
(top = 0 A val = k :1: F0(1) : 1 S k S pushing)} which is true from the
proof of the if...ﬁ statement, the truth of the invariant, and continuity of

computational chains.

3. Show that upon termination the postcondition is true, i.e. show that I A R’ A
-(Q) => R.

s i 2 GAO S x S m—1A(top 2 1AStack,~ = x:i—pushing SiS
i +pushing V top = 0 A val = k =1: F0(1):1 S k S pushing) A -1(i 79 0) =>
i=0Aval=k*F0(1).

a OSx Sm—lAi=0Aval= k*F0(1)A1 S k Spushing=>i=0Ak=
pushing A val = pushing =1: F0(1), because the stack is empty, there were
pushing copies of index 0 on the stack, and the stack is decrimented at the
end of each pass of the loop, so the line “val := val+ F0(1)” was executed

exactly pushing times.
4. Show wp,-(A,R:-),i=1,2,...
0 Basis: The index in the computational chain is 1. Then by 2 we have that
iZOAOSxSm—IAR’.
o Hypothesis: Assume that for index k > 1 we have i Z 0 A 0 S x S
m — 1 A R’.

a Show: For index k + 1.
Case A: i = 0. Then the stack is empty and termination has oc-
curred. So by 3 we have I A R’ A -‘(g) => R, i.e., i = 0 A val =
pushing =1: F0(1). But val = pushing =1: F0(1) = FO”“”“"9(1), but this

98

is fm_1(fm-2("'(f0(1))"')) = f,,,_1(1), because each time we iterate

through the loop, the variable representing the index (x) is decrimented.

0 Case B: i 75 0. Then the computation has advanced one more step and

by 2 we have IA R’.

Using the foundation of Dijkstra, neither Dijkstra nor Gries are able to say any-
thing about the correctness of this program because of the a priori demonstration of
termination that is required. Using our foundation we can show that the invariant
we write for a loop is a true invariant. We can show that the conjunction of the
loop’s invariant and the approximation to the postcondition imply that each incre-
ment of the loop is correct. We can show that the conjunction of a loop’s invariant,
the approximation to the postcondition of the loop, and a negative guard for the
loop implies that the postcondition is true. We can apply induction to each index
of the computational chain induced by the program statements, and show that as
the computation progresses each element of the computational chain has a logical de-
scription that either accurately approximates the limit of the computation or is itself
the limit of the computation, depending on the condition of the loop’s guard. With
our method we can show the total correctness (partial correctness and termination)

of this total recursive function.

7 .2.2 Proof of Correctness of a Partial Recursive Function

This program reads a sequential stream of 8-bit ASCII characters; these characters
are represented as natural numbers in the range 0 . . .255. We assume that end of ﬁle

(eof) is < RETURN >, so the program will read the input stream

cliar1,c/1ar2,clz.ar3,...,char1,,< RETURN > .

99

In ASCII, < RETURN >= 10. The value of k is unknown until the program
ends. We use the notational convenience of multiplication in this example for clar-
ity. A macro for multiplication and its transformation into our language is given
at the end of this section. This macro could be invoked with the macro statement
y := MULT(y,thousand) with thousand = 1000, and the register list changed to
reﬂect this.

macro Example2(registers : y, x, co], 2, count);

2 := x;
3! == 0;
count := 0;

while x 75 eof do

count := count + I;

y:=y*1000;
y:=y+z;
z:=x;

od

This simple program works by concatenating the current value in the input register
onto the right end of the string held in the output register by ﬁrst multiplying that
value by 1000 and then adding the new value. No a priori bound can be deﬁned
for this loop because the number of characters read (the ﬁnal value of count) will
be unknown until the program terminates. None of the current methods based on
the wp predicate transformer is able to verify the correctness of this loop because it
is unbounded. Since the loop has no a priori upper bound, Nelson, Hesselink, and
de Bakker would have to assign the postcondition FALSE to this loop. We use our
method to say much more than FALSE in a proof that it is correct.

Proof of the unbounded loop

{Pre:countzOAy=O}

100

{1:0 S 2 S 255}
{Bound : none}
while x 75 eof do

count := count + 1;

y:=y*1000;
y==y+2;
z:=x;

{R’ : y = y *1000 + xcoum}
od

{R;x=eof/\y=$:0SiScoui'ztzy=y*1000+$.'}

1. Show the invariant I is true before the loop executes:

a wpw(“z := x”,0 S 2 S 255)

a TRUE

2. Show that an execution of the guarded command terminates with the invariant

and the speciﬁcation of the code within the loop (R’) true.

a wpw(“count := count + 1;y :2 y :1: 1000;y := y + z;z := x”,0 S 2 S
255 A y = y *1000 + xcoun,))

IA
5;
IA

0 wpw(“count := count + 1; y := y * 1000; y := y + z”,wpw(“z := x”,0

255 A y = y *1000 + seem)
a wpw(“count := count+1; y := y*1000”,wpw(“y := y+z”,0 S 2 S 255Aw))
o wpw(“count := count + l”,wpw(“y := y =1: 1000”,0 S 2 S 255 A w))
s wpw(“count :2 count + 1”0 S 2 S 255 A w)

s 0 S 2 S 255 A y = y =1: 1000 + xcoum. Implied by the invariant.

101

3. Show that if termination occurs as we expect the postcondition is true, i.e.

show that I A R’ A -(g) => R.

s 0S2S255Ay=y*1000+xcoumA-(x#eof)=>x=eofAy=E:0S

iS count:y* 1000 +x,-

s0S2S255Ay=y*1000+xcoumAx=eof=>x=eofAy=E:OS

i S count:y*1000 +x,-

0 x=eofAy=Ez0SiScount:y*1000+x,~
4. Show wp;(A,R:),i=1,2,...

0 Basis: Index = 1. Then we have executed the loop one time and count = 1.

By step 2 we have y = y :1: 1000 + x,

s Hypothesis: Assume for index k > I we have count > 1 and y = y :1:

1000 + xcount, i.e., the computation is correct to this point.
a Show: Show that the hypothesis holds for index k + 1.

0 Case A: x = eof. Then termination has occurred and by step 3 and
our hypothesis we have that x = eof A y = E : 0 S i S count : y =

y :1: 1000 + x,- because count was not incremented.

0 Case B: x 75 e0 f . Then the computation has advanced one more step

and by step 2 we have that y = E : O S i+1 S count+1 : y*1000+x;+1.

We now give code that could constitute a macro to perform multiplication.
macro MULT(registers : y, x, z, eof, count, thousand, sum);
sum := 0;
while thousand 75 0 do
sum := sum + y;

thousand := thousand; 1;

od;
thousand := 1000;

y := sum;

To convert this macro to a code segment in our language:

1. Number the registers: y = x1, x = x2, 2 = x3, eof = x4,count = x5,thousand =

226,811”! = $7

2. Remove the header with the register list:
x7 := 0;
while x6 76 0 do
$1 1= 1'7 + 1'1;

333 i: 5176—1;

od;
1:6 2: 1000,
$1 3: 337;

7.2.3 Proof of Correctness of a Nonterminating Computa-
tion

The program we present here computes the z’“ prime number in ascending order,
see Figure 7.4. The program is designed to be nonterminating, so no method that
depends on the wp predicate transformer alone can be used to prove it is correct. The
program uses two macros, one that performs division without remainder returning
the value 1 when a divisor for the natural number being tested is found (Figure 7.5,
Section 7.3), the other that checks the range 2 S i S x — 2 for possible divisiors of the
natural number x (Figure 7.6). Both of these programs use bounded loops. The main

macro, Example3 (Figure 7.4) uses an unbounded loop to calculate the set of prime

103

natural numbers in ascending order. We prove the bounded loop in macro divides,
use this proof to show the correctness of macro Prime, and then use the correctness
of macro Prime to prove the unbounded loop in Example3 is correct in all of its
increments.

Proof of the bounded loop of macro divides:

Let IF. . . FI stand for the decision construct.
1. Show the invariant I is true before the loop executes.

a wpw(“t := x”,x > 0)
o x>Osincex7$0
a TRUE
2. Show that an execution of the guarded command terminates with the invariant
and the speciﬁcation of the code within the loop (R’) true.
a wpw(“t :=t+x;IF...FI”,x> 0A(t =yAz =1)V(t<yAz=0))
s wpw(“t := t+x”,wpw(“IF...FI”,x > 0A(t = yAz =1)V(t< yAz = 0)))
a wpw(“t := t + x”,x > 0 A w)
s x > GA (t = y A z = 1) V (t < y A z = O). Implied by the invariant.

3. Show that upon termination the postcondition is true, i.e., show that I A R’ A

«(G)=>R.
o x>0A(t =yAz =1)V(t <yAz=O)A-1(t <y)=>(t=yAz= 1)V(t>
yAz=0)

s x >0A(t = yAz =1)V(t < yAz = 0)A-1(t < y) => (t =yAz= 1)V(t >

yAz=0)

o (t=yAz=1)V(t>yAz=0)

104
4. Show wp,(A,R:), i = 1,2, . ..
0 Basis: Index = 1. Then we have executed the loop one time and by step
2wehave(t=xAz=1)V(t<xAz=0).

o Hypothesis: Assume for index k > 1 we have (t = y A z = l) V (t <

y A z = 0).
a Show: Show that the hypothesis holds for index k + 1.

0 Case A: t _>_ y. Then termination has occurred. By step 3 we have
that x>0A(t=yAz =1)V(t>yAz=0),sincetheloopdidnot

iterate again, and t was not increased.

0 Case B: t < y. Then the computation has advanced one more step,

sot=t+xandby2wehavethat (t=yAz=1)V(t<yAz=0).

Proof of the bounded loop in macro Prime

Let IF. . . FI denote the decision construct.
1. Show the invariant is true before the loop executes.

o wpw(“i := 0”,0 S i S count)
0 0 S 0 S count
a TRUE

2. Show that an execution of the guarded command terminates with the invariant

and the speciﬁcation of the code within the loop (R’) true.
0 wpw(“z :2 divides(d,x); IF. . . FI;d :2 d +1;i :=i+1”,0 S i S count A
R’)
s wpw(“z := divides(d,x);IF. . . FI;d := d +1”,wpw(“i :=i+1”,0 S i S

count A R’)

105

wpw(“z := divides(d, 1:); IF. . . FI”,wpw(“d := d+1”,0 S i S count Aw))

wpw(“z := divides(d,x)”,wpw(“IF. . . FI”,0 S i S count Aw))

wpw(“z := divides(d,x)”,0 S i S count A w)

o 0 S i S countA3 S d < xA((divides(d,x) = TRUEAy = 0)V
divides(d, x) = FALSE A y = 1)). Implied by the invariant.

3. Show that when termination occurs the postcondition is true, i.e. show that

IAR’A-w(g)=>R.

s 0 S i S count A R’ A -1(i < count) =5 i = count A ((divides(d,x) =
TRUE A y = 0) V (divides(d,x) = FALSE A y = 1))
o i = count A ((divides(d, x) = TRUEAy = 0) V (divides(d,x) = FALSEA

:1 =1))-
4. Show wp,(A,R:-), i = 1,2,...

0 Basis: Index = 1. Then we have executed the loop one time and d = 3,
so by Step 2 we have that 3 S 3 < x A ((divides(3,x) = TRUE A y =
0) V (divides(3,x) = FALSE A y = 1)).

s Hypothesis: Assume for index k > 1 that 3 S d < x A ((divides(d,x) =
TRUE A y = 0) V (divides(d, x) = FALSE A y =1)).
0 Show: Show that the hypothesis holds for index k + 1.

0 Case A: i = count. Then termination has occurred and by Step 3 and
our hypothesis we have that i = countA((divides(d, x) = TRUEAy =
0) V (divides(d,:lr) = FALSE A y = 1)).

0 Case B: i < count. Then the computation has advanced one more
step and d = d+1, so by Step 2 we have 3 S d S xA ((divides(d,x) =
TRUE A y = 0) V (divides(d,x) = FALSE A y = 1)).

106

Proof of the unbounded 100p in macro Example3

Let IF . . . F I denote the decision construct.

1. Show the invariant is true before the loop executes.

0 10PM“?! == 0”,.1/ Z 0)
o 0 Z 0
a TRUE
2. Show that an execution of the guarded command terminates with the invariant
and the speciﬁcation of the code within the loop (R’) true.
0 wpw(“y := y +1;isprime:= Prime(y); IF. . . FI”,y Z 0 Ap, S y)
o wpw(“y := y +1;isprime := Prime(y)”,wpw(IF. . . FI”,y Z 0 A p, S y))
o wpw(“y := y + 1”,wpw(“isprime := Prime(y)”,y 2 0 A y))
0 wpw(“y == 5 +1”,y 2 0 A y)
o y 2 0 A pZ S y. Implied by the invariant.

3. Show that since termination will not occur FALSE is the correct postcondition.

s yZOApzSyAp(y>0)=>F/1LSE
s TRUEATRUEAFALSE: FALSE

0 FALSE
4. Show wp,-(A,R:-), i = 1,2,...

0 Basis: Index = 1. Then we have executed the loop one time, y = 1, z = 0

or z = 1, so by Step 2 we have pz S y.

o Hypothesis: Assume for index k > 1, with y = k and 2 S y, that p, S k.

107

a Show: Show that the hypothesis holds for index k + 1. y + l = I: +1 and
2+1 S k+l so 2 S k+1. Then by Step2 we have that p2.” S k+1.

This proof shows that it is possible to verify the correctness of a nonterminating
loop that is deﬁned on its input. With his method Dijkstra could say nothing about
such a loop. With their methods do Bakker and Nelson could say only that the
loop does not terminate since the postcondition is FALSE. With the availability of
computational sequences and a recurrence between predicate transformers we can say
that while the loop is nonterminating, each iteration produces the z‘“ prime number

in ascending order.

108

7 .3 Annotated Program Code for Examples

macro Example1(registers : val, m, 11, index, count, i, stack, top, pushing,j, x);
{m _>_ 0 A n 2 0}
val := 0;
if m = 0 then
val := F0(n);
{m = 0 A val = F0(n))
else
ifn = 0 then
val := F0(n);
{m >0An=0Aval= F0(0)}
else
val := 1; index := m — 1;
count := 0;
{Pre:m>0An >0}
{Inv :0 S count S n}
{Bound : t = n - count}
while count < 12 do
val := Fhll(index,val);
count := count + 1;
{R’ : 1 S count Sn A val = count * Fhll(m — 1,val)}
od
{R : count = n A val = n =1: thl(m — 1,1)} since val was ﬁrst set to 1
ﬁ
{(n = 0 A val = F0(0)) V (n > 0 A val = n =1: FM1(m — l,l))} and
n =1: FM1(m — 1,1) is FMl"(m — 1,1)
ﬁ
{(m = 0Aval = F0(n))V(n = OAval = F0(0))V(n > OAval = n*FM1(m-—l,1))}

When the index of the function (variable m) is zero and the argument of the function is
greater than zero, we compute the base case (macro F 0(n)) and the output (variable
val) is equal to fo(n) = n+1. When the index of the function is greater than zero, but
the argument equals zero, we compute the base case (macro F 0(n)) again because of
the function’s behavior (see the note after the function deﬁnition). Here, the output
val is equal to fm(0) = 1. When both the function index and the function argument
are greater than zero we compute n * FM 1(1) = FM I"(1) since we initialize the
output variable val to 1 before executing the bounded loop. This is equivalent to the
functional speciﬁcation in the second deﬁnition by cases. The ﬁrst variable used by
macro F M 1 is the largest index in the family of functions used in the computation.

Figure 7.1. Example 1, A Total Recursive Function.

109

macro FM1(registers : val, m, 11, index, count, i, stack, top, pushing,j,x);
i := 1; Stack := index || Stack; x := index;
{Pre : Stack,- = m — 1 A val Z 0}
{Inv:iZOAOSxSm-l}
{Bound : none}
while i719 0 do
top :=]]’Stack; Stack :2 top I] Stack;
if top 2 1 then
if val = 1 then
val := F0(1);
else
if val = 0 then
val := F0(1); pushing := val;
else
pushing :2 val; i :- i+1; val := 0;
ﬁ
{pushing > 0}
j := 0; i := i — 1; x :=]]’Stack;x :2 x -— 1;
{Pre :j = 0 A pushing > 0}
{Inv:O Sj SpushingAO S x S m— 1};
{Bound : t = pushing — j}
whilej < pushing do
Stack := x [I Stack;

i := i + 1;
j:= i + 1;
{R’ : 1 Sj S pushing A Stack,- = x : i —j S i S i +j}
od
{R :j = pushing A Stack,- = x : i — pushing S i S i + pushing}
ﬁ
else

val := val+ F0(1);
{top = 0 A val = val + F0(1)}
ﬁ
“.7 = pushing A Stack,- = x : i — pushing S i S i + pushing) V (top = 0 A val =
val + F0(1))}
i := i — 1; top :=|]’Stack;
{R’ : (top = 0 Aval = k=1= F0(1):1 S l: S pushing) V (top 21A Stack; = x:
i - pushing S i S i + pushing)}
od
{R : i = 0 A val = pushing * F0(1)} pushing ... F0(1) = F0”"”""9(1). But this is the
result of functional iteration, since we only decriment the index (denoted by x), so
we compute fm_1(fm-2(' ' ' fo(1)) ' ' '))-

Figure 7.2. Major Macro for Example 1.

110

macro F0(registers : val, m, 71, index, count, i, stack, top, pushing,j, x);
ifn=00rn=1then

val := n + 1;
else
val := n + 2;

fl

Figure 7.3. Minor Macro for Example 1.

macro Example3(registers: z, y, x, isprime, t, count,d, i);
z := 0;
31 == 0;
isprime := 0;
{Pre : z = 0}
{Inv : y 2 0}
{Bound : none}
while y 2 0 do
:1 == y + 1;
isprime := Prime(y);
if isprime = 1 then

9 == y;
z := z + 1;
ﬁ
{R’ : pz S y} Where p, represents the 2"” prime

od
{R : FALSE}

Figure 7.4. Example 3, A Nonterminating Program.

1H

macro divides(registers : z, y, x, isprime, t, count,d, i);
z := 0;
ifx7€0Ay5£0 then

t := x;

{Pre:x>0Ay>0}

{Inv : x > 0}

{Boundzbzy—t}

while t < y do

h=t+x;
ift=ythen
z:=1;
ﬁ
{R’:(t=yAz=l)V(t<yAz=0)}
od

ﬁ
{S:(x750Ay#0A((t=yAz=1)V(t>yAz=0))}

Figure 7.5. Example 3, The Macro divides.

macro Prime(registers : z, y, x, isprime, t, count, (I, i);
z := 0;
ifx S 1 then
:1 == 0;
else
count := x42;
:1 == 1;
d := 2;
i := 0;
{Pre:countsz2Ay= 1Ad=2}
{Inv :0 S i S count}
{Bound : t = count — i}
while i < count do
2 := divides(d,x);

ifz=1then
y==0;

ﬁ

d:=d+1;

i:=i+1;

{R’ :3 S d < x A ((divides(d,x) = TRUE A y = 0) V (divides(d,x) = FALSEA y =
1)}
od

{R: i = countA((divides(d,” = TRUE/)3! = 0V(divides(d,x) = FALSE/W =1)”
ﬁ

{S : (((x S lVdivides(d, x) = TRUE)Ay = 0)V(divides(d,x) = FALSEAy = 1)))}

Figure 7.6. Example 3, The Macro Prime.

CHAPTER 8

Conclusion

Current techniques using the wp predicate transformer are unable to deal with pro-
grams computing functions in the total recursive and recursive classes because they
use the initial state/ﬁnal state model that relies on termination in proofs of correct-
ness.

We have given a language and a computing environment for it. We have given
the denotational semantics and operational semantics for the language in terms that
allow us to write programs to compute partial functions, and we have shown that
these programs can compute only the results we expect because side effects are not
possible.

We have also shown that as programs in our language are run they induce compu-
tational chains in our variable state space whose elements are both logical extensions
of their predecessors (they are monotonic) and are faithful approximations to the
computation’s limit (they are continuous). That is, our computational chains are
structures that contain valuable and reliable information about a computation in
progress, whether it will eventually terminate or not.

We have deﬁned a new predicate transformer as a conjunction of partial correct-
ness and a recurrence relation between wp predicate transformers. This relation is

the basis for our inductive proof method for program correctness.

113

114

Our results provide a mathematical foundation for reasoning about terminating
and nonterminating processes, and a concrete method with which to reason about

such processes.

8.1 Future Work

A basic property of the function speciﬁed in Example I of Chapter 6, Section 7.1 is

given by a lemma found in Davis and Weyuker [26].

Lemma 8.1 fn+1($ + 1) = fn(fn+l($))v

Proof:
fn+1($ +1) = ffoll
= fn(f.f(1))
= fa(fn+1(:v))

With this lemma we can show that f,,(x) = A(n, x):

fi+1(17 + 1) = fi(fi+1(l'));

and

A(i+1,x +1) = A(i,A(i+1,x)).

For the base cases we have

A(‘t,0)= 1: fi(0)

x+1 ifx=0,l
A(0111’) = = f0(5'3)
:l' + 2 if .1? > 1.

The recursively speciﬁed function A(i, x) is a variant of a function introduced by W.

Ackermann.

115

Unbounded looping and general recursion are equivalent methods for computing
functions in the recursive class. Both methods work with families of functions.

In this example we have related the indices of a speciﬁc family of functions in a
one-one fashion to two structurally equivalent but syntactically different functional
speciﬁcations. Is the relationship shown by Davis and Weyuker an exception to or
an example of a rule that can be used to relate a compositional syntax to a general
recursive syntax? That is, is there a consistent system of transformations between
recursively speciﬁed and compositionally speciﬁed (but structurally equivalent) func-
tions? If such a system exists, we can use our proof technique on the version expressed
compositionally, apply the transformation, and be sure that the recursive version is
also correct.

A second issue deals further with recursive syntax in programming languages. The
computational model we have used is deterministic and so continuous. The model
Dijkstra used was nondeterministic, but because he insisted on bounded nondeter-
minism his model was also continuous. In both cases this makes sense because in
models that use looping constructs an unbounded number of alternatives within the
loop is not computationally possible. On the other hand bounded nondeterminism is
a detriment when the computational model is recursive syntactically, because the re-
quirement of continuity prohibits unlimited backtracking. In his paper Nelson [6] was
careful to use a limit theorem that did not require continuity so that he could apply
his model to partial functions (backtracking may not be bounded in a nonterminating
computation). This question was also addressed by Hesselink [12], who showed that
for syntactical recursion the Law of the Excluded Miracle holds, so continuity can be
maintained in his model.

This raises two questions. First, can our wpw predicate transformer be conformed
to a model that relaxes the continuity requirement somewhat. Because it deﬁnes a

recurrence relation between predicate transformers in a repetitive situation we have

116

subchains of a computational chain at our disposal to investigate the computation’s
behavior. Is continuity of a subchain sufﬁcient for recursive computations? If the
answer is yes, then we ask whether a multiple induction scheme can be used in

veriﬁcation proofs involving the wpw predicate transformer.

BIBLIOGRAPHY

BIBLIOGRAPHY

[I] E. W. Dijkstra, A Discipline of Programming. Prentice-Hall, Inc., 1976.

[2] E. W. Dijkstra, “Guarded commands, nondeterminacy and formal derivation of
programs,” Communications of the ACM, vol. 18, pp. 453—457, August 1975.

[3] C. A. R. Hoare, “An axiomatic basis for computer programming,” Communica-

tions of the ACM, vol. 12, pp. 576-583, October 1969.

[4] A. R. Meyer and D. M. Ritchie, “Computational complexity and program struc-

ture,” IBM research paper RC-1817, IBM, Yorktown Heights IBM Watson Re-
search Center, 1967.

[5] J. W. de Bakker, Mathematical Theory of Program Correctness. Prentice-Hall
International, 1980.

[6] G. Nelson, “A generalization of Dijkstra’s calculus,” ACM Transactions on Pro-
gramming Languages and Systems, vol. 11, pp. 517—561, October 1989.

[7] S. C. Kleene, Introduction to Meta Mathematics. Princeton, NJ: D. Van Nos-
trand, 1952.

[8] E. C. R. Hehner, “do considered odd: A contribution to the programming
calculus,” Acta Informatica, vol. 11, pp. 287—304, 1979.

[9] A. R. Meyer and D. M. Ritchie, “The complexity of loop programs,” in Proceed-
ings of the ACM National Meeting, pp. 465—469, 1967.

[10] J. E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Program-
ming Language Theory. The MIT Press, 1977.

[11] E. C. R. Hehner, “Predicative programming part 1,” Communications of the
ACM, vol. 27, pp. 134—143, February 1984.

[12] W. H. Hesselink, “Predicate-transformer semantics of general recursion,” Acta
Informatica, vol. 26, pp. 309-332, 1989.

117

118
[13] E. W. Dijkstra and A. J. M. van Gasteren, “A simple ﬁxpoint argument without
the restriction to continuity,” Acta Informatica, vol. 23, pp. 1—7, 1986.

[14] R. W. Floyd, “Assigning meanings to programs,” in Proceedings of the American
Mathematical Society Symposia in Applied Mathematica, vol. 19, pp. 19-31, 1967.

[15] I. Greif and A. R. Meyer, “Specifying the semantics of WHILE programs: A
tutorial and critique of a paper by Hoare and Lauer,” ACM Transactions on
Programming Languages and Systems, vol. 3, October 1981.

[16] H. D. Mills, “The new math of computer programming,” Communications of the
ACM, vol. 18, pp. 43—48, January 1975.

[17] M. H. V. Emden and R. A. Kowalski, “The semantics of predicate logic as a
programming language,” Journal of the ACM, vol. 23, pp. 733-742, October
1976.

[18] E. Cohen, Programming in the 19903 An Introduction to the Calculation of Pro-
grams. Springer-Verlag, 1990.

[19] E. W. Dijkstra and C. S. Scholten, Predicate Calculus and Program Semantics.
Springer-Verlag, 1990.

[20] R. Conway and D. Gries, An Introduction to Programming. Cambridge, MA:
Winthrop Publishers, Inc., 1973.

[21] D. Gries, The Science of Programming. Springer-Verlag, 1981.

[22] R. Sommerhalder and S. C. van Westrhenen, The Theory of Computability: Pro-
grams, Machines, Eﬂectiveness and Feasibility. New York, NY: Addison-Wesley,
1988.

[23] Z. Manna, Illathematical Theory of Computation. MCGraw-Hill, 1974.
[24] R. E. Davis, Truth, Deduction, and Computation. Computer Science Press, 1989.

[25] A. Milli, N. Boudriga, and F. Mili, Towards Structured Specifying: Theory, Prac-
tice, Applications. New York, NY: Ellis Horwood Limited, 1989.

[26] M. D. Davis and E. J. Weyuker, Computability, Complexity, and Languages. New
York, NY: Academic Press, Inc., 1983.

"Illllllllllllllllt