Courant Computer Science Report # 12

September 1977

Correct-Program Technology/
Extensibility of Verifiers

Two Papers on Program Verification

Martin Davis and J.T. Schwartz

Courant Institute of
Mathematical Sciences

Computer Science Department

New York University

Report No. NSO-12 prepared under Grants No.
NSF-MCS7^24212, NSF-MCS71 -02039, and NSF-MCS 76-0011 6
from the National Science Foundation; and
U.S. Energy Research and Development Administration
Contract No. EY-7^C-02-3077*000.

COURANT COMPUTER SCIENCE PUBLICATIONS

Price

COURANT COMPUTER SCIENCE NOTES

, J. Cocke and

ril 1970, iii+767 pp

$23.00
20.50

v+201 pp. 6.25

URANT COMPUTER SCIENCE NOTES

Programming Languages and Their Compilers, J. Cocke and
J. T. Schwartz, 2nd Revised Version, April 1970, iii+

On Programming: An Interim Report on the SETL Project.
J. T. Schwartz, Revised June 1975, xii+675 pp.

A SETLB Primer. H. Mullish and M. Goldstein, 1972, v+2^^ ^^.

Combinatorial Algorithms. E. G. Whitehead, Jr., 1973, vi+104 pp. 3.25

COURANT COMPUTER SCIENCE REPORTS

No. 1 ASL: A Proposed Variant of SETL
Henry Warren, Jr., 1972, 226 pp.

0 . 2 A Metalanguage for Expressing Grammatical Res
in Nodal Spans Parsing of Natural Language.
Jerry R. Hobbs, 1974, 266 pp.

0 . 3 Type Determination for Very High Level Langua
Aaron M. Tenenbaum, 1974, 171 pp.

mprehensive Survey of Parsing Algori'
uages . Phillip Owens. Forthcoming .

COURANT INSTITUTE OF MATHEMATICAL SCIENCES
251 Mercer Street
^ New York, New York 10012

/

COURANT INSTITUTE OF MATHEMATICAL SCIENCES

Computer Science NSO-12

CORRECT-PROGRAM TECHNOLOGY/EXTENSIBILITY OF VERIFIERS
Two Papers on Program Verification

Martin Davis and J. T. Schwartz
with Appendix by E . Deak

Report No. NSO-12 prepared under Grants
No. NSF-MCS76-24212, NSF-MCS71-02039 ,
and NSF-MCS76-00116 from the National
Science Foundation; and U. S. Energy
Research and Development Administration
Contract No. EY-76-C-02-3077*000 .

TABLE OF CONTENTS

Page

On Correct-Program Technology J. Schwartz

Appendix E. Deak 110

Metamathematical Extensibility for Theorem Verifiers

and Proof Checkers M. Davis & J. Schwartz... 120

111

On Correct Program Technology
Jack Schwartz

1 . Introduction

By now the potential importance of formal techniques
for proving program correctness has been recognized for
over two decades, and something between four and seven
hundred papers principally devoted to the development of
such techniques have been published (see [London, 1970],
[1972] for useful reviews of existing literature) . A wide
variety of formalisms have been proposed; among these, the
inductive assertion technique of [Floyd, 1967] , and the
variant of it proposed and repeatedly extended by Hoare
[1969] , [1971] [1972] seem most convenient. But in spite
of all this work, a truly practical program verification
technology has been slov; to develop. The essential diffi-
culty not yet overcome is economic: the cost of formal
program verification using existing teachniques is still
much too high. This objection is best understood if we
consider the way in which a fully formal variant of the
Floyd technique would operate. In this approach, one is
given a program text P, to which an input assumption I
and an output assertion are attached. (These assertions
are written in any convenient, sufficiently powerful,
logical formalism, e.g., predicate calculus supplemented
by Zermelo-Frankel set theory. In general, we shall use
LF to denote whatever logical formalism is used.) Call a
program text thus annotated (i.e., carrying attached assump-
tions and assertions) a praa. To prove a praa Q correct
by the Floyd method, one begins by attaching

-1-

additional assertions to its text. Generally speaking, at
least one such additional assertion needs to be attached to
each loop (also each procedure) in the program text of the
praa; in effect, this assumption captures and formalizes the
fragment of technique which guided the programmer to write the
loop. (As a matter of fact, recent work has shown that at least
for some simple loops these assumptions can be supplied autom.ati-
cally, see [Wegbreit, 1974], [Morris and Wegbreit, 1976],
[Misra, 1975] . While the techniques used to do this are
interesting and ingenious, the approach to be developed in
the present paper suggests that the possibility of pro-
ceeding in this way is not of primary importance.) The
praa Q ' developed by adding these additional assertions
to Q is then processed by a verification condition generator
(sometimes also called a verifying compiler , though the
term verification compiler would be better) , which by a
straightforward process converts Q into a set S of statements
of the logical formalism LF . Then to complete the
verification one must prove all of the statements of the
set S. In principle, these proofs must themselves be
verified mechanically, i.e., each proof must be expressed
in a fully formal way and certified by a proof verifer
program PV able to recognize correct LF-proofs. It is at
this stage of a verification that we must expect the
greatest expenditure of labor to occur; although in
principle the verifier program PV could supply part of
the necessary proof itself, the present state and prospects
of automatic proof technology make it appear likely that
PV will have to be guided quite closely by the supply of
numerous very detailed proof steps. (However, energetic
development of proof-verifier technology can be expected
to reduce the number of formal steps which must be supplied
in typical proofs, and to allow these proofs to be supplied
in intuitively comfortable forms.) A secondary difficulty
is that the substitutions and other formal manipulations
applied by a verification condition generator will typically

-2-

convert the assertions occuring in a praa, the intuitive
content of which may already be somewhat obscure, into
still murkier forms, adding to the burden and difficulty
of supplying the necessary formal proofs.

Having thus briefly reviewed existing technique,
let us now contrast the approach proposed in the present
paper, in order to highlight the pragmatic differences
that characterize our approach. In the first place,
rather than starting with large unannotated program texts
and attempting to prove their correctness, we shall prefer
to work systematically with praas known to be correct,
stating rules for the manipulation and combination of
aorreat praas, using which new, necessarily correct praas
can be derived. Thus our approach will conform and give
formal realization to an insight of Dijkstra: that
proarams should not so miuch be proved correct as developed
in such a way as to make their correctness e/ident. In
this sense, the class of correct praas is to be compared
to the set of universally valid formulae of the logical
formalism which underlies them, and the rules for praa
combination which we shall state correspond to the formal
proof rules of substitution and deduction which allow new
universally valid formulae to be deduced from old- In
pragmatic terms, we may claim that the approach to be
described gives formal expression to the generating steps
by which programmers construct programs in the first place,
and accordingly can object to the standard Floyd-Hoare
approach by noting that, starting always from an externally
given program text, it necessarily loses sight of a
program's genetic origins. A central claim of the present
paper is that by remedying this defect the task of deducing
a praa ' s correctness can be much alleviated.

-3-

In our approach then, correct praas can be used to
generate new correct praas, in much the same way as new
correct algebraic or logical formulae can be gererated
by combining old formulae. This suggests the following
view of the programming process: that it amounts to a
type of formal manipulation roughly analogous to algebraic
computation, in which text fragments expressing elementary,
essentially irreducible, correct algorithms are combined
to yield correct programs adapted to one or to another
intended application. (And developed to the point at
which program efficiency becomes acceptable.) From this
point of view, what has been lacking till now is simply
a sufficiently full and formal statement of the rules for
manipulation and composition of correct praas; here it
should be noted that these rules neaes sarily relate to
correct praas and not simply to program texts, which
may perhaps help explain why full statement of them has
been so long delayed. Observe then that, regarding
programming as a type of formal manipulation akin to the
algebraic manipulation of (possibly very large) formulae,
we can understand why much but not all of it is experienced
psychologically as having a routine flavor rather than
smacking of the intensely creative. From this same point
of view we may say that, just as the generation of reliably
correct large algebraic formulae must rest on the use of
a formula manipulation program, so the reliable generation
of large correct praas must rest on the formal use of a
programmed praa manipulator; In both cases, the probability
of error becomes overwhelming if one tries to work manually
with large texts. Extending this analogy, we may liken
the informal procedures which characterize much of today's
programming to what algebraic calculation might be if,
without making systematic use of formalized rules, one

-4-

operated on the basis of informal reasoning and informed
intuition; can then liken the process of structured
programming advocated by Dijkstra to a still manual
process of calculation guided by systematic reference
to formal algebraic rules, and can liken the correct-praa
technology which we shall describe to the use of a formula
manipulation program.

The most elementary fragments to which our rules of
modification and combination will usefully apply will be
correct praas, generally rather small, each of which
expresses some fundamental and essentially indecomposable
element of algorithmic technique. Some of these 'root'
praas can be very simple, e.g. those which describe the
standard techniques for zeroing an array or adding up
the components of a vector; others will be more complex,
and will e.g. describe the 'treesort' technique or the
techniques used to maintain B-trees; others may be re-
latively profound, and describe, e.g., the essential
ideas of Tarjan high-speed technique for determining
flow-graph reducibility . To establish the correctness of the
'root' praas corresponding to these algorithms, we
have no choice but to use a variant of the general Floyd/
Hoare program verification technique. (The formrlism
that we will use for this is rather close to that of
Hoare, but in detail differs significantly from Hoare 's
formalism; these purely pragm^atic differences adapt our
formalism to our larger purposes, but also seem to make
the proof formalism that we shall describe somewhat more
comfortable to use than Hoare ' s technique, and perhaps
also a mite more general.) That the full power of the
logical formalism LF should have to be invoked to prove
the correctness of each 'root' praa is after all not
surprising, since each such praa expresses an essentially

-5-

new mathematical fact: in heuristic terms, we may say-
that on first meeting such a praa, we are bound to find
the fact that it works surprising until we have been
presented, at least informally, with a mathematical proof
that it does. On the other hand, in our approach the
correctness of 'composite' praas will follow in relatively
routine fashion from the way in which they are built up.
Thus a second pragmatic objection that we may raise to
the Floyd/Hoare technique as it is ordinarly used is that
it applies , to composite programs ^ techniques that only
need to he applied to elementary programs , thereby rending
formal verification over-expen sive .

Concerning the logical formalism LF that we shall
use and the level of programming language to be used along
with it, the following remarks should be helpful. For
expressing logical relationships and formal proofs, it
is clearly most advantageous to use a maximally powerful
logical language, which dictates the use of something like
predicate calculus supplemented by Zermelo-Frankel set
theory. Indeed, if one uses any significantly less
powerful logical framework, then certain relationships
which would have very direct expression in the more
powerful language will be unstateable or at any rate
stateable only in very crabbed and roundabout ways in the
less powerful formalism; moreover, certain proofs which
in the more powerful formalism would be short and direct
will be rendered long and complex, and may even become
impossible. If one mistakenly foreswears the use of
set theory, this consideration applies, e.g., to any use
of the 'box principle', i.e., that any assignment of n
objects to fewer than n boxes must put at ]east two objects
into some one boxf as part of a correctness proof. But
then, since it is desirable that no limitation inherent in
the programming language we use should deprive us of any

-6-

expressive or proof-theoretic possibility which our
underlying logical formalism would allow us, we shall also
want to allow our programming language to m.anipulate
perfectly general set theoretic objects. We shall do
this with a vengeance, initially foreswearing all con-
siderations not only of efficiency but even of im.plonentability ,
and thus working with a formal programming language in
which any set-theoretic object, whether finite, infinite,
or even transfinite can be 'manipulated ' . Note that since
our concern is initially not to execute programs but
simply to prove the correctness of praas, this manner of
proceeding, which may at first sight seem counterintuitive,
is not only harmless but desirable and necessary. However,
this does not mean that our considerations will apply only
to praas written in a language of some unrealistically
high level. Quite to the contrary, the methods to be
described will facilitate the proofs of correctness even
of programs written in assembly language. After all, in
developing such a proof one is concerned only to exhibit
a minimum-length path of argument from a given set of
axiomatic foundations to a final assembly-language
program.; the fact that transfinite modes of expression
have been used along the way to shorten this path is as
little harmful as the numerical analyst's use of properties
of the transfinite set of real numbers is harmful to the
efficiency of some entirely finite root-finding procedure
which he can justify by reasoning about these properties.
We note that in a very interesting paper [Wegbreit, 1976]
has shown how program-verification techniques can be
adapted to give formal proofs that algorithms are efficient;
even in such proofs, the use of very high level and even
potentially transfinite modes of expression can be
advantageous, since (we emphasize once more) the efficiency
of an algorithm and the implementability or efficiency of

-7-

the expressions used to study it are two entirely different
things.

Since the programming language that we will use will
allow arbitrary set-theoretic objects as data objects,
it will be relatively easy for us to deal with any of
the data structures coiranonly encountered in programming
practice, e.g. , arrays, structures, and even pointer systems
which we will be able to represent explicitly using maps.

In the above connection it is worth noting that the
present paper concentrates exclusively on the question
of 'partial' correctness of praas. That is, we
prove only that, as a praa runs, and given that all the
assumptions in it are correct, it must follow that each
assertion in it will be confirmed whenever control passes
through the place in the path to which the assertion
attaches. Note that if control never passes through a
given place, then any assertion at that place is correct
a vviori. Since we concern ourselves only with partial
correctness, neither loops which never terminate or
operations with illegal operands will create any special
problems for us. In particular, we can write iterations
(VxSs) oode; end V; over infinite sets freely.

The techniques of praa modification and combination
central to the approach advocated in the present paper
are very much anticipated in [Gerhart, 1975a] , [1975b] ,
[1976] . Significant technical differences between our
treatment and that of Gerhart are as follows: (a) Basing
herself on the Hoare formalism, Gerhart confines her
attention to the somewhat special class of praas in which
assumptions and assertions appear only at the heads of
»^ile loops, and focuses rather more strongly on the
'forward' and 'backward' Floyd verification conditions

-8-

than is entirely appropriate for the development of a
smooth formalism,. (b) Gerhart tends to make use of a
logical formalism considerably narrower than the set-
theoretic system which we assume. This does not make
the possible range of praa transformations stand out
in its full generality; in particular, certain important
technical issues connected with the set-theoretic operator
'^', which selects an arbitrary element from a set, are
m.issed. (c) Our treatment is rather more polished and
systematic than that found in the papers cited.
Although these differences cumulatively seem to have
significant implications for the usability of a correct-
praa system, perhaps it is fairest to say that our approach
differs from that of Gerhart more in pragmatic than in
theoretical terms .

The techniques sketched below seem to the author to
open the way toward a practical technology guaranteeing
program correctness; in this, we agree enthusiastically
with Gerhart. To bring this technology into existr^nce,
one would have to implement a praa-verif ication/manipulation
system like that which we will describe; features which
can strengthen this system from the human-factors point
of view should be energetically sought out and incorporated
into it. Of course, a correct-praa manipulation system
should be interactive. Once such a system was established,
one croup of algorithm developers c3ould enter root
praas, with full, formally verified proofs of their
correctness into it; the application programmers who were
the verification system's main users would then inter-
actively combine these root praas into the larger programs
that they required. An intermediate group of 'subsystem
developers ' might expand important, initially succinct and
highly general, root praas into forms particularly convenient
for particular classes of applications, and also supply

-9-

fleshed out praas and groups of praas as verified code
blocks, procedures, and procedure libraries of intermediate
size.

In section 2, following, we will develop all
the bases of our method. In section 3 we illustrate the use
of the method, specifically by proving the correctness of a
simple high level algorithm ('sorting by counting') , whose
root form we will initially describe by a succint, very
high level text, which will then be manipulated systematically
and converted by stages into a correct assembly-language
version of the same algorithm. The material in section 3
is best viewed as a partial hand simulation of the use and
nature of a verification/manipulation system of the
sort we envisage.

Note that since the present paper is intended to be
a convincing description of such a verification/manipulation
system rather than a detailed specification for
a particular system of this kind, we shall formalize
only to a degree felt to he helpful and intuitively
convincing , but not more. In particular, full syntactic
specifications and inductive definitions, which the
authors of papers on program correctness are sometimes
zealous to present, will be painted in with no heavier
a brush than seems appropriate.

Techniques like those which we will now describe
can be used to develop correct parallel programs and also
to prove the correctness of logical circuit designs.
Note that the problem of proving the correctness of logical
circuit designs, especially for logical circuits which
store information internally and thus have very large
niombers of states, is an important though little-studied
problem.

-10-

2* ?J25£?r'Fip2"-P^Si:'5'3?.'_?fPP^ J?^?^li^?' H"'"- ^'J*^£/_%l5£'
Code Transfornatior P^Jlfs^

a . Prograirnning i,an gu a cje .

Our prograrurting language SL adr.iits all the objects of
(Zernielo-Frankel ) set theory into its semantic universe;
this includes all sets whether finite or infinite, all irappings,
plus integers and the set of all integers in their ordinary set-
theoretic sense. We are even happy to adndt transfinite
ordinals and cardinals, etc., though as a natter of fact in
the present paper we shall rriake no use of these esoteric objects.
We allov/ the rdnimal basic vocabulary of set theory to be extended
in the usual way by the definition of new sets, predicates, and
terms. Thus, for example, we will feel free to write oneone(s,t)
for the set of all one-to-one mappings from the set s into the
set t, etc. It is left to the reader to work out or look up
the detailed definitions which reduce this notion and all others
like it to the very spartan collection of primitives actually
present in the axioms of set theory. /ny valid expression of
set theory is also a valid expression of our programining language.

^,side from all of this, which we swallow at a gulp, our
language is very conventional. Each program in it consists of
a main hlocJ< , whose first st8tem:ent is its entr-y , plus some
finite numb;er of auxiliary functions . The syntactic form of a
function is illustrated by

(1) function /name (pa2'-, ... ,par ) ;

function _body
end;

Both fname and par,,...,par are simple tokens, fname is the
name of the function and pav^, . . . ,par^ are its parameters.
The function_body in (1) is a block, that is, a list of
statements. All the functions appearing in a program are
required to have different names. It will be convenient
for us to assunie that function names are distinguished lexically

-11-

from the variable names appearing in a program. VJe assumie
that none of the arguments or variables appearing in any

function appear in any other function; that is, all

variables and arguments are strictly local to the function
in which they appear.

Statem.ents may be labeled, and with more than one label

if desired. The form of a labeled statement is

(2) L, :L„:...:L : unlabeled statement .

1 2 n —

A given label can precede only one statement, and that only once

We allow unlabeled statemerts of only a few forms:

(a) Simple assignment statement:

variable = expression',

(b) Conditional transfer statement:

if boolean_expression then go to label;

The unconditional transfer is regarded as an abbreviation
for i_f true then go to label.

(c) Function-call statement:

variable = fname {expn^ , , . . ,expr ) ,

where fname is the name of a function having n parameters,
and expn, , . . . ,expn are a like number of expressions.

(d) Selection operator and selection statement:

the operator sexpn selects an arbitrary element of
the set-valued expression expn, and aborts if expn has the
null-set value nl_. We allow the selection-statement form

variable = 3expn .

(e) Return statement:

return expression;
where expression is an arbitrary expression.

-12-

This completes the list of the statements of our basic
language. Subsequently we will find it convenient to allow
other more or less conventional language forms and language
features (e.g. while loops, if- then-else constructions) as well,
but in every case these additional features will be regarded
merely as syntactic abbreviations for combinations of the
fundamental statenients (a) -(e).

All of the statemient forms (a) -(e) are given their
conventional semantics. Concerning function calls, our semantic
assuiTiption is that calls are allowed to be recursive,
and that arguments are transmitted 'by value with delayed
value return', that is, by incarnating an instance of the
function for each call, and setting its parameters equal to
the arguments of the call when the call operation begins,
and then by setting the target variable of the call (c) to
the value of the return expression (set (e) ) when luxe caii
o::jeration is terminated by a return statement.

We assume that a statement if^ C then go to L can never
appear in a function unless the label L appears in the same
function. A function is assumed never to modify its parameters.
(b) Proof Formalism and Proof Rules

The variables of a program Q consist of the variables
which occur explicitly within it, plus an indefinite collection
of additional variables wh.-' ch we keep in reserve for use
during manipulation of the program, (more properly, of a praa
obtained by adding assumptions and assertions to the program) .
We regard these extra variables as denoting values which the
original form of the program Q neither reads nor writes.
The Tplaces it of a program are all those (syntactic) points
in the program text which either immediately precede (the
body of) an unlabeled statement, follow (the body of) such
a statement, or which either precede or follow a label in
the program. The entry _place of a program is the place
preceding its first statement. A -program proposition P
is any syntactically well-formed predicate formula of set-

-13-

theory involving only the variables of the program as free
variables. A propositioti-at-a-place is a pair (P,it) consisting
of a program proposition P and a program place tt . We shall
often choose to use the symbol P to denote (P,it) . A
proposition-at-a- function is a pair (P,fnaine) consisting of
the name of one of the functions appearing in (the program of)
a praa, together with a syntactically well-formed set- theoretic
predicate P containing exactly n+1 variables, where n is
the number of parameters of the function fname; thus P may
be written as

P = P (res,a^, ,a^) .

By E we shall always denote some finite set of proposi-
tions-at-a-place or -at-a-f unction in a praa R that we are
studying. The central formal elements of our proof formalism
will be assertions of the form E | — P where P is a proposi-
tion-at-a-place or -at-a-f unction. VJe will begin by explaining
the meaning of such assertions, and then by listing a number
of properties of such assertions which foil cw easily from
the semantics which we have assigned to our language SL (and
which could readily be proved formally if we bothered to write
out a formal definition, in terms of 'state sequences', for
this semantics). Then, having listed these properties, we can
abandon all direct consideration of the states and semantics
of SL, and shall use only the listed properties of the
E |— P relationship to deduce correctness. However, before
doing so, it is appropriate that we should give formal defini-
tion to the notion of a praa and of the correctness of a praa.

Definition: (a) A praa R is a program Q (of the language
SL) , together with two sets E, E' of propositions-at-places
and -at- functions of Q. The set E is called the set of
assumptions of R and the set E' is called the set of assertions
of R.

(b) The praa R is said to be correct or to be valid

• £ r 1 T^"^ J r I ^fname ^ ~tt t^tt , ^^fname .

if E t~ P and E | — P, , for all P and P, in

the set of assertions of R, where E is the set of assumptions

of R.

-14-

To indicate that a praa R is valid we will often
find it convenient to write ]> R <J. If the text of a praa
is shown explicitly, we shall indicate its assumptions
and assertions by writing each of them (as a fcririula of LF)
either in the place to which it belongs or, {in the case
of propositions-at-f unctions) iirjnediately preceding the
first line of the function to which it belongs. To distinguish
between program text, assumptions, and assertions, we shall
prefix assertions by the sign ' |— ' and assumptions by the sign
' |e' • An example of all this notation, and one that
will be studied and rr.anipulated extensively in section 3,
is the following simple sort-by-counting praa:

p>[=set(s) & f G sing val maps (s , reals)
place = n£ ;
s' = n£.; .

Loop: j — place G one one miaps (s ', integers)

& (Vy G s') #{zGs I f (z) < f (y) } < place (y)

< #(z^s 1 f(z) < f(y) V (f(z)=f(y) & zGs')};
if s = s' then go to Lout; /* note in what follows */
x = 3(s-s'); /* that Q represents 'undefined' */
place(x) = #{z£s|f (z)<f (x) v(f (z)=f (x) &place(z) 7^ ^) } + l;
s' = s' u {x};
go to Loop;
Lout: ] — place G one one maps (s , integers)

& range (place) = {n, 1 £ n < #s}
& (Vx,y G s) f (x) < f(y) =* place (x) < place(y) 4

Having thus explained our intent and illustrated our
notational conventions, we shall now proceed to define the
logical meaning that we attach to the notions 'proposition-
at-a-place' and • proposition-at-a-f unction' , and will
also define the fundamental relationship E [— P .

-15-

Let R be a praa , and let Q be the program on which
it is based.

(i) By a state of Q, we mean (as usual) a mapping
which assigns a value (namely any object of set theory)
to every variable of Q, and which assigns a place of Q
to the special symbol control _lcoation . If a state S
assigns the place tt to the symbol contr'ol_locaticn , then
we say that S is at '^ . By a computation for Q (or R) we mean a
finite sequence of states of Q which evolve in accordance
with the text of Q and the semantic rules of the language SL ,
and which (if we ignore its final state) contains no more
states at places immediately preceding return statements than
states at places immediately preceding function call statements.
If the initial (resp. final) state of a com.putation c is at the
place TT , then we say that c is a computation from (resp. to) '^ •

(ii) If s is a state of Q at a place tt of Q and P is

a proposition at tt , then we say that s satisfies P if the

proposition P (s (v J ,s (v_) , . . . , s (v )) is true, where v, ,...,v

± z n in

are the variables of P""^, and s(v.) is the value which s assigns

to the variable v.. If c is a computation of Q, then we say

that c satisfies P''^ if every state of c which is at tt satisfies

P\

(iii) Let c be a computation of Q, and let f name a func-
tion of Q. Suppose that f has n parameters v, , . . . ,v , and let

f f in

P, - (P^ (val ,a, , . . . ,a )) be a proposition at f. We say that c

satisfies P, if, for every state s of c which is at the place
immediately preceding a call of the function f , and given that
s' is the next following state (if any) of c which is at a place
immediately following the same call statement and for which the
section of c between s and s' contains an equal number of states
before function calls and after such calls then (writing '^ i ' • • • ''^"^i
for all the variables of f and rvf for the value returned by f)

P (rvf, s (v^) , . . . ,s (v^) )
is true. (Note: in what follows we shall sometimes find it con-
venient to refer to s ' as the next matching return state of s.)

-16-

(iv) If E is a set of propositions-at-places and
at-functions of Q, and c is a computation of Q, then we
say that c satisfies E if c satisfies every proposition
at-a-place and every proposition-at-a-f unction of E.

(v) If Q, E, and P are as above and if tt' is
a place of Q then we say that [tt']E |— P^ if every compu-
tation of Q from tt ' which satisfies E also satisfies P^ .

(vi) If Q, E, and P are as above, then we say that

f ^

[Tr']E |— P if every computation of O f rom tt ' which

^ f

satisfies E also satisfies P, •

(vii) The statements [initial_place] E |— P^

f TT

and [initial_flace]E |— P, can be abbreviated as E |— P

f ■'-

and E |— P. respectively.

Now that we have defined the fundamental [tt ] E |— P
relationship, we can begin to list its properties. Note
that some of the properties we list can be deduced from
others listed; to allow this redundancy is convenient even
if somewhat inelegant.
Proof Eu les :

(a) If [7T^]E I- p"" and [tt^] (Eu {p^}) |_ p^^,

1T„ TT„

then [tt ]E |— P^ ; and the same holds if we replace P^ by
a proposition-at-a- function P, .

(For if every computation to tt„ satisfying E also

TT TT

satisfies P , and every computation to tt„ satisfying E and P

TT

also satisfies P ^ ^ then clearly every computation to tt^

-■- TT2 '^

satisfying E also satisfies P, ) .

(b) If g names a function of Q, if also [ti^]E |— P^
and [tt ]E u {p^} |- p^ , then [Tr,]E |- Pw' and the same holds
if we replace P^ by P^.

(By much the same argument given in support of (a) .)

-17-

(c) If E c E' and [tt ]E \- P^ , then [t ]E'\- P^ ,
and similarly if P is replaced by P . (Obvious.)

(d) If P is any universally valid formula of logic,
t±ien [Tr,]E | — P for every E, ir, , and tt , and similarly
if P^ is replaced by P . (Obvious.)

(e) If [^^]E I— p" and [tt^]E [-(?=* Pj)^
(where =* is the sign of predicate implication)

then E I — Pi / ^^^ similarly if tt is replaced by f. (Obvious)

(f) If P^ e E and pf € E , then [tt,]E \— P^ and

f
[tt.IE |— P,. (Obvious.)

In writing the remaining statements of the present
group, we will use the convenient notation g_ , statement ^ g

to indicate that 6_ is the place immediately before
statement and that B, is the place immediately after statement .
Moreover, if we wish to single out one of the variables x of
a praa R, we shall write the list of all its variables as

(Xj othev_yars) . Otherwise we shall write this list of
variables simply as vars .

(g) (Assignment statement proof rule) . If 6_ ,

X = expn(x, other_vars ) , 6 , / (where expn is any expression
depending on the variables vavs of R) , tt^ 7^ B . , and
[tt^JE I — (P(x, other_vars) ) , then „

[Tf^]E I — ( (3x' ) (P (x' ,other_vars) & x = expn(x', other_vars) ) )

(For if we consider any computation from t: to 6
satisfying E and let x' be the value which the variable x
had immediately before the assignment statement was executed,
then clearly P(x', other_vars) & x = expn(x', other_vars)
at the end of the computation) .

(h) (Transfer statement proof rule) If
3_, if C(vars) then go to L, 6^ , where C is any boolean
expression depending on vars) , tt^ 7^ 6_|_ , and
[^ ]E |._ (p(vars)) ", then [tt^^IE [- (P(vars) & "lC(vars))
(Obvious; this is the condition that the transfer not be
taken . )

-18-

^

(i) (Function call proof rule) . If f names a
function of Q having m parameters, if

3 , X = f (expn, (x,other_vars) , . . . ,expn (x,other_vars) ) , 3. ,
where expn, , . . . ,expn are expressions, if

[tt^]E |- (P(x,other_vars) ) ~, [tt^JE |- (P^ (val,a^, . . . ,a^ ) ) ,
and if '^■^ ¥ ^+ > then
[tt^]E !-( (3x') (P(x' ,other_vars) &

P, (x,expn, (x' ,other_vars) , . . . expn (x* ,other_vars) ) )

(Consider a computation c from ir^ to 3^ satisfying E.
then the section of c between the last call to f and the
next matching return receives the values y . = expn . (x,other-vars)
as parameters, and if val denotes the value of the expression
appearing in this return statement the relationship
F- (val,y, , . . . ,y ) holds. Hence, if we let x' designate
the value which this variable x has immediately before the
function call at 3_ , then both P (x' ,other_vars) and
P^ (x,expn, (x* ,other_vars) , . . . ,expn (x' ,other_vars) )
are valid at the place 3^ , immediately after return.)

(j) (Selection operator proof rule) If
3_ , X = Bexp (x,other_vars) , 3^ , (where expn is any
expression depending on the variables of R) , tt^ ?^ 3^ t and

[it ]E 1— (P (x,other_vars) ) ~, then

[TT,]E |- (3x') (P(x',other_vars) & xS expn (x' ,other_vars) ) .

(By much the same justification as that offered for (f ) ,
except that in this case we know only that x g expn (x' ,other_vars)
rather than x = expn (x* ,other_vars) ) .

(k) (return statements) If 3_ / return expn, 3^ , and
TT ?^ 3_i^ , then [tt ]E |- (false) "*". (Since no computation can

reach the place 3^) •

In order to give comfortable form to the proof rules
which apply to the place tt immediately following a label L,
it will be convenient to assume 3_ /L:, 3^f to let

-19-

3_ , . . . , B_ denote all the places in the program Q which

iminediately precede a statement of the form if^ C then go to L

(with the same label L) , and, for each of these places

(J)

(i) ^-'^

3 -^ , to let C (vars) be the boolean expression occurring

(0)

(i) ^_'P+
in the if-statement immediately following &_ (while C

is simply taken to be the constant expression true) . Moreover,

with each such L we introduce m+1 additional boolean constants,

which we shall write as from ... , j = 0,...,m. (In heuristic

terms, from ... denotes the condition that one has just arrived

at the label L from the place B_-' ) . Using these notations,
we can state the proof rules applying to labels as follows:
(5,) (With the above notations) If tt^ 7^ 6^ / then

[7T^]E h (fro^^(o) V ... V from (^))

(m) (with the above notations) If [■n^]E |— (P(vars))

then B^^\&^ 6^

[TT ]E [-(from ... => (C (vars) & P(vars)))

■*■ B_

(Both of these are obvious if we consider computations to
g. which reach B. either by a step from 3_ or by a
conditional transfer from B_ , j >^ 1) .

Function calls bear some resemblance to go to operations,

and thus it is convenient to use auxiliary boolean variables

like those introduced in connection with labels to state the

proof rule which applies to function entrances. Specifically,

if f names a function in the praa R with program Q, then

we let B^''"^/.../3 denote all the places in Q which

immediately precede any call x = f (expn^, . . . jexpn^^) to f.

For each j we let expn,^ ^ ^ , . . . ,expn ^^ ^ denote the argument

■J ^ 1 "^ m (j)

expressions which appear in the call immediately following B

-20-

For each such f, we introduce n boolean constants, which
we shall write as from ... , j = l,...,n. We let tt be
the place iitur.ediately "^fol lowing the header statement
of f, i.e., iirmediately preceding the first executable
statement of f.

(n) (With the above notations) If tt 7^ tt , then

[•n,]E \- (from ,,, v ... v from , .)'"
-L Q ( 1 J gin)

(o) (With the above notations) If P is a predicate
c

and if

whose only free variables are the paramieters yw-../y of f.

[7T^]E I— (P(expnp' ,. . . ,expnp^ )) ^^ then

B.
[TT^]E h (from^ =* P(yir..wy-^)) ^ .

Note that all non-parameter variables of f must be
excluded from P, since when f is called a comipletely new
'incarnation' of it will be built, and in this incarnation
the value of all non-parameter variables will have unknown
values.

This could complete our list of elementary proof rules?
however, it is convenient to give a somewhat more extensive
list, and in particular to give rules which cover the usual
syntactic extensions of our basic language. The principal
syntactic extensions which we propose to allow are as follows:

(p) (while-loops) As usual, we regard the construction

while C;

code
end while;

as an abbrevi-
ation for

Loop: inc then go to Lout;
code ;
go to Loop;
Lout : ...

where Loop, Lout are labels which do not appear elsewhere.

-21-

The program place immediately following the label 'Loop' is called
the head of the while-loop. The proof rule applying in this case
is as follows: if 6_ , while ... end while , 6 , if 3 is the head
of the while loop, if it, 7^ 3 and tt, is not within the while loop,

if the loop cannot be entered except through 3, and if

B B ,3+

[tt ]E |— P and E |— P " , then [tt^]E |— (HC & P) . This is

an obvious consequence of the if-statement proof rule.
(q) (if -then -else) We regard the construction

if C then

oodel
else

aode2
end if;

as an abbrevia-
• tion for

if nc then go to Ll ,
code 1
go to L2 ;

Ll : code2;

L^ I • • •

where Ll, L2 are labels which do not appear elsewhere.
If we introduce notations for places by
3_/ i£ C then, B-^, . . . ,^2' £l^/ B^f-.wB^, end if, 6^ ,
and assume that tt ?^ B , tt 7^ g , and t^.t^B, , then

the following proof rules apply:

3 6,

if [v^]l \- P , then [tt^JE |^- (P & C)

3 e-

(ql)
(q2)
(q3)

if [tt ]E [— P ~ , then [tt^]E [~ (P & He)

3.

if [-rr^lE \- V^

and

[TT_^]E I- V^ ,

p ,
then [TT_^]£ I- (P^ V P2) .

All these are straightforward consequences of proof rules
stated earlier.

(r) (Indexed assignment) We allow the familiar
syntactic form

(3)

var (expn. ) = expn^

to be used, but regard this as an abbreviation for the simple
assignment

-22-

(4) var = {<expn^,expn^>] U {x e var JHpair (x) v(pair (x) &hd (x)7^ej;p?7 ) } ;

Here pair(>:) is the set-theoretic predicate which is true if
and only if x is an ordered pair, and hd_ is the set- theoretic
function which sends each ordered pair into its first coipponent.
The proof rule for (3), which we shall not bother -o vvrite out
explicitly, follows at once if we apply rule (g) to (4).
Note in this sanie connection that var{expn] is allowed as
an abbreviation for {tJ_(x), x e yar|pair(x) & hd(x) = expn] ,
where t_£ is the set-theoretic function which sends each
ordered pair into its second component, and that var {expn)
abbreviates 3 {var {expn}).

(s) (Multiple assignment and superselection operator) As
we will see in the following subsection, the selection
operator aS is of particular significance, since at the
place imiinediately following an assignment x = 3S we know
nothing about x other than the fact that it is a member of s.
Thus if we replace the statement x = 3S by any correct, single
entry, single exit praa R, which changes no variable of F
other than x and for which the assertion (x G s) is
available at the exit place B, of R, , then the praa R containing
the statement x = 3s remains correct. This statem.ent is
an essential key to construction of correct praas by combination;
in exploiting it, we will often want to make use of a code
sequence

temp = 3{<u, ,...,u >| C(u. , — ,u^, other vars)};
1 n i n —

X, = temp(l); ...; x = temp (n) ;

here, temp is assumed to be a 'temporary' variable not
occurring elsewhere in a praa R, and temp(j) denotes the j-th
component of its n-tuple value. It is convenient to allow
this important code sequence to be abbreviated by the syntactic
form

-23-

(6) <x, ,...,x > = <u,,...,u > where C(u, ,...,u ,vars) .
1 n 1 n 1 n

The proof rule for this staterr.ent is an iirmediate consequence

of the selection and assignment rules given above, and can be

stated as follows:

Let B (resp. £ ) be the place which imiriediately

precedes (resp. follows) a ' superselection ' statement of

the form (6). Then if F I — (P(x, ,...,x , other vars) ) ",

i n —

it follows that

E 1^ ((3u, ,...,u ) P(u,,...,u ,other_vars)

K

& C(u,,...,u , other vars))
In —

(t) (Shadow- Variable Principle) 'Shadow' variables
are variables occurring neither in the initial nor in
the final form of a praa, but introduced into intermediate
forms of it (during manipulation) to facilitate praa
proofs that would otherwise be difficult or even impossible.
The rules which govern the introduction and removal of
shadow variables play an essential role in verification;
generally speaking, proof rules like those given in the
present section are incomplete without supplementary
shadow-variable rules , but become complete as soon as a few
simple shadow-variable rules are introduced. For this
reason we have felt it necessary to mention the shadow-variable
issue here, even though detailed statement of the rules
connected with shadow variabels is postponed to the following
subsection ('Code Transformation Pules') into which it fits
more naturally.

A general objection to the preceding rules is that they
do not provide any sufficiently powerful method for eliminating
assumptions from a praa. For this reason, the two following
principles are of fundamental importance.

-24-

Lemma (Induction principle for propositions-at-a-place) .
Let TT be a place in a praa R with variables vers. Let E be
a set of propositions of R, and let P be a Proposition at tt .
Let &_ , L, IT, so that the place it immediately follows
a label L, and let B_ ,...,£_ denote all the places in the
program Q which immediately precede a statement of the form
^f C then go to L (with the same label L) . For each of these
places 3_ / let C '"^ (vars) be the boolean expression
occurring in the conditxonal transfer statement iirmediately

(i ) 6 ^^^ TT

following 3_ (while C ~ ' is the constant expression true) .
Then, if tt^ f^ tt and [tt ] E u {p^} |_ (c^'" '^ ^ P)^'--^
for all j = 0,...,m, it follows that [tt ]E f— P .

Lemma (Induction principle for propositions-at-a-function)

Let f name a function in a praa P having variables vars. Let E

be a set of propositions of R, and let P be a proposition at f.

Let TT bo the place immediately following the function statement

which heads f (so that tt immediately precedes the first

•executable' statement of f ) . Suppose that the places in f which

immediately precede return statements are p^,...,p , and let

expn^ , . . . ,expn denote the expressions which appear in the

corresponding return statements. Let the parameters of f be

X. ,...,x . Then if [tt]E u {p^} |- (P (expn . ,x , . . . ,x ) ) ^
J- n J -c -^ ^^

for j = l,...,m, it follows that [tt^^] E [— P for any place tt^,

Proof of the first induction principle; Suppose the
contrary. Let c be a computation from, tt to tt satisfying
E but not P^, and suppose that c is of mdnimum length among all
computations having this property. Truncate the last step of
c, thus obtaining a computation c' one step shorter, which is
to one of the places B_-' . Because of the minimality o^ c, ^(j)
c' satisfies P^, and thus since [tt^]E u {p^} \- (C^- '^ =* P)
P clearly holds for the final state of c, a contradiction
which proves our assertion. Q.E.d.

-25-

Proof cf the second induction principle: Suppose the
contrary. I-et c be a computation from [tt.] to a place immedi-
ately following a call of f . Suppose that c satisfies E but
not P , and suppose also that c is of minimum length among all
computations having this property. Then a final section c- of c
must go from tt to an invocation of f, and from there through f
to the place immediately following this invocation and have the
property that within c^ tnere occur as many states at places
preceding call statem.ents as at places following call statements.

Let X ',..., X be the values assigned to the variables x,,...,x_
in in

by the initial state of Cp. Truncate the last step of c„, thus
obtaining a computation c' one step shorter, which is to one of

the places p.. Because of the minimality of c, c' satisfies P .

-' f P-i

Since [Tr]E u {p } [- (P (expn . , x^ , . . . , x^) ) -" , it then

follows that Cq satisfies P^. If c_ is the part of c which

precedes c^, then it is clear from the minimality of c that

f f

c satisfies P . Hence altogether c satisfies P , a

contradiction which proves our assertion. Q.E.D.

To use the proof rules described in the preceding pages
to prove the correctness of a root praa R, we will generally
proceed in the following way. Initially, R will be a program
text annotated with assumptions but with no assertions.
Clearly, any praa containing assumptions but no assertions
is correct. The proof rules will then be used to deduce
various assertions; any particularly significant 'output
assertion' playing a significant role in the use of R should
be included among the assertions deduced. Then finally, the first
and second induction lemmas stated just above will be used
to remove superfluous assumptions; in many cases, the only
surviving assumption will be an input assumption characterizing
the data objects on which R will work properly.

In writing out the text of a praa, it will be useful to
distinguish between assumptions which are to remain in the
final fully 'proved' version of the praa and assumptions

-26-

introduced temporarily but to be removed as the praa is
manipulated. In order to make this distinction vivid,
we shall mark assumptions of the latter, purely tem.porary,
class with the prefixed sign \zz rather than [^; and then each
use of one of the two inductive lemmas just stated transforms
some occurrence of the sign f= into an occurrence of | — . Note
that the temiporary assumptions which appear in our formalism
often correspond closely to the 'loop invariants' of the
Floyd and Hoare formalisms .

We can use the 'counting sort' praa shown earlier to
illustrate the general v;orkings of our proof form.alism.
To prove the counting sort praa correct, we begin by striking
out the output assertion which it contains, and by converting
the assertion appearing at the place immiediately following
the label 'Loop' to an assumption. This gives a praa which,
since it contains no assertions, is certainly correct.
From this applying the proof rules stated in the preceding
pages to add assertions, we obtain the following, still
correct, praa. (Note that relatively elem.entary set-
theoretic reasoning has been applied to deduce one assertion
from another at various fixed places in the praa shown below;
in a fully formalized system, justification of this reasoning
to the satisfaction of a logical proof verifier would be the
most onerous part of our total verification procedure.
We do not show the detailed steps of this reasoning, but the
reader who wishes to m.aster our proof technique is strongly
urged to reconstruct it.)

-27-

^ set{s) & f G sing_val_maps (s , reals)
place = n£ ;
s' = n£;
I — place e one one maps (s ', integers)

& (Vyes') #{zes| f (z)<f (y) } < place(y)

< #{zes|f(z)<f(y) V (f(z)=f(y) &zes')};
Loop: |rr place e one_one maps (s ' ^ integers)

& (Vyes') #{zes| f (z)<f (y) } < place(y)

< #{zeslf(z)<f(y) V (f(z)=f(y) & zSs')};
if s = s' then go to Lout;

X = 3(s-s'); j — x€s & x^s' & x^domain (place)
(Vyes') ((f (x)>_f (y) =* #{a£s|f (z)<f (x)v(f (z)=f (x) & ^s')}^place (y))

&(f(x)<f(y) =* #{zes|f (z)<f (x) v(f(z) =f (x) & zes') }<place (y) -1) )

|— place e one one maps (s ', integers) & x^domain (place)
& (#{zGslf (z)<f (x)vf (z)=f (x) & place (z)^il}+l)

^ range (place)
place(x) = #{zes|f(z) < f(x) v f(z)=f(x) & place (z) 7^^}+l;

|— place e one_one_maps (s ' u {x} , integers)

& (Vyes' u {x}) #{zeslf(z) < f(y)} < place(y)

< if{zes|f (z)<f (y) v f(z)=f(y) & ze(s'u {x})};
s' = s u {x};

[— place s one one maps (s ', integers)

& (Vyes') #{zes|f (z)<f (y) } < place(y)

< #{zGs I f(z) < f(y) V f(z) = f(y) & zes ' } ;
go to Loop;

Lout: |~ place G one one maps (s , integers)

& (VyGs) #{zGs I f(z) < f(y)} < place(y) < #{zGs|f(z) ^f(y)}
j— (Vx,y e s) f (x) < f(y) =* place(x) < place(y)
& domain (place) = {n, 1 <n < #s}

-28-

Once this praa is reached, the first inductive leinina
can be used to degrade the assumption at 'Loop' to an assertion;
then by dropping all but this loop assertion and the asser-
tions at 'Lout' we put the praa into its desired form.

Note that much of the logical detail appearing in the
praa written just above is irregular enough in form to evade
the grip of automatic simplification routines working at any
level of power easy to develop at the present time . This
is the central difficulty of current program- verification
technology. The transformational techniques which we shall
now begin to explain aim to make it unnecessary to supply
nearly this much detail except when proving the correctness
of a root praa.

-29-

c. Code Transformation Rules

We shall now begin to state the rules, central to our
proposed approach, which allow the manipulation and combination
of correct praas . We begin with a class of rules which,
since they assume that specific assertions are available
at particular points, can only be stated for praas.
Subsequently, general auxiliary rules which could as well
be stated for programs (rather than praas) will be listed.
Throughout this section, we suppose that R is a valid praa,
that P is one of the assertions-at-a-place in R, that f
names a function appearing in R, and that P, is one of
the assertions-at-a- function in R.

Substitution and Other Fundamental praa Rules

(l.a) (Equality substitution) If P is (e.=e2) , then
e, can be replaced by e„ in any statement at ir .

TT TT

(l.b) (Member siabstitution) If P is (e.^e ) , then
3 e„ can be replaced by e, in any statem.ent at tt .

(The praa in which 9e_ occurs is known to be (partially)
correct no matter what element is chosen from e_ when e2
is evaluated; hence it remains correct if the specific element
e, is selected.)

(l.c) (Siibset substitution) If P is (e, c e-) / then
9 e^ can be replaced by 3 e, in any statement at it. (Justified
in much the same way as (b) .)

(l.d) (Dead code removal/insertion) If (false)^ holds for a
set of places tt at which there are no assumptions (so that no
computation satisfying all assumptions can reach any of these
places) then the statements immediately following these places
can be removed. Conversely, any syntactically admissible code,
with arbitrary assumptions and assertions, can be inserted at

TT

a place at which {false) holds, provided that label duplication
is avoided.

(l.e) (Block substitution rule) Let R^ be a correct praa
whose function names are disjoint from those of R, suppose that
the variables appearing in functions of R, are all distinct from

-30-

the variables appearing in R, and suppose that all the variables

X- ,...,x coininon to R. and R appear either in the 'main block'
1 m 1 ^^

(i.e. 'main program') of R, or that all these variables appear

in a single function f of R. (In the former case, we shall say

that R, is insertabl e into the main block of R; in the latter,

that R, is iyisevtable into the function f of R.) Let tt be the

entry place of R, , and let tt be some other place in R, .

Suppose that the only variables among x,,...,x modified by

R^ are x,,...,x (where of course n < m) , and let x',...,x'
1 In — I'm

be a group of m additional variables of R, which do not appear
either in R or R, . Let C = C(x^,...,x ,x',-../x') be a logical
form.ula whose only free variables are those indicated. Let
E^ be the assumptions of R, . Then if for R^ we have

I I '^1

(7) [iTJE^ u { (x^=x^ &...& ^i^=^iJ,)^^ |— (C(x^, . . . ,x^,x|, . . . ,x^) )

we say that the ^-effect of R, to the place tt, is governed by C.

Next, in addition to the above assumption, suppose that

all the labels in R are distinct from the labels appearing

in R, with the exception of precisely k labels L,,...,L, ,

all of which appear in R either in the main block of R (if R,

is insertable into the main block of R) or in a particular

function f of R (if R, is insertable into f ) . Suppose that

the context in which each of these labels appears in R, is

L.: go to L . ; (i.e., that the statement in R^ following each

of these labels is a 'stop'). Suppose that immediately after

the entry place tt of R, a label L appears. For each j = l,...,k,

let C.(x, , ,x , X ' , ,x') govern the R-effect of R, to the

jl,.>nl 'm^ 1

place ^Y^' immediately following the label L . . Suppose that
in R each of the labels L. , j = l,...,k appears in the
context

(8) B^^^ <x^,...,x^> = <u^,...,u^> where C^ (u^ u^,x^, . . . ,x^) ; L . :

i.e., follows a where statement of the indicated form,
and that if E designates the assiunptions of R we have

-31-

(9) E |- ({Vuw...,u ) (c!(u ,...,u , X ,...,x )
' ± n 3 i n 1 m

(J)

C^(Uir>.>/ U_^ fX^f.../ XjQ J ) )

for j = l,...,k. Suppose finally that ifl<_i7^j<_k
we have

3(i)
(10) E |- (Vuj^, . . . ,u^) (Hc! (u^, . . . ,u^,x^, . . . ,x^) )

Then if we fuse R and R, together by modifying them
in the following way, the praa R' which results is still
correct:

(i) Replace each of the k where statements (8) appear-
ing in R by the statement go to L;

(ii) Add the functions of R, , with all their assumptions
and assertions, to the collection of functions of R;

(iii) If R, is insertable into the main block of R, then
insert the main block of R, at any place in R immediately
following an unconditional go to statement. If R, is insert-
able into the function f of R, then insert the main block of
R- at any place in f immediately following an unconditional
go to or a return statement. In either case, the text of R.
should be inserted into R along with all the assumptions and
assertions present in it, and the labels L. , j = l,...,k
originally present in the text of R, should be suppressed,
leaving only one copy of these labels in R , namely those
copies originally present in R.

To convince ourselves of the correctness of the praa R'
to which this rather complex and general substitution rule
leads us, we can reason as follows. Consider a computation
c' which starts at the entry place of R' and satisfies all the
assumptions of R'. We can decompose c' into a sequence of
subsections CwC ,c ,c , . . . ,c ,c , where each c. is a
computation in R and each c . is a computation in R, ; c. always
starts at the entry place of R, (and if j < n) goes to some

-3 2-

place 6 -' immediately preceding one of the go to L.
statements in R-, . Consider one of the subcomputations c.,
j < n, let V, ... v' be the values assigned to the

variables x, ,...,x by the first state of c . , and let

1 m. -" J '

V, ... V be the values assigned to these variables by the

1 m _ ^

final state of c • . Clearly v' = v, for n < k < m, and
equally clearly all the sta; et of c . assign the same value
to any variable not mentioned in R^ . VJhat we must show is

that if the state of c' imraediately preceding c. is at the

( t ) - (i) ' ^

place B_ , then c . goes to the palce £ ; and that the

values Vt,...,v' are values that could be assigned to
In

X , . . . ,x by the where statement (8) , which is the same as
requiring that C. (v^ , . . . ,v ,v! , . . . ,v' ) . Since vie assume that
the R-effect of R, to the place £_; is governed by

I

C (x, ,...,x ,x, ,...,x ), and taking note of (9), we see that
io-Lnim ^ I c )

we have only to prove that the final state of c_. is at g

Suppose this to be false, so that the final state of c . is

(i) -'

at some £_; for which i 7^ j . Then we would have

c!(v^,...,v ,v',...,v'), so that the proposition
il nl m r-r-

(3v- ... V ) C!(v, ,...,v , x,,...,x ) would hold for the
1 n , J . 1 1 n i m.

state at £_ which immediately precedes the first state
of c . . By (10), this is impossible. Note in connection with
all this that since each c . is a valid computation of P., ,
the computation c satisfies all the assertions and assiamptions
of R , in addition to all the assertions and assumptions of R.

When the block substitution rule (e) is applied, the
next few rules v/ill often be useful.

(l.f) Let x^ , . . . X be variables of R not otherwise
1 n

appearing in P. Let

(11) B_,<x,, ,x > = <u,,...,u^> where P^^^ (u^^ , . . . ,u^, vars)

& P^iu^^^^^, . . . ,u^,vars) ,B_
Then the where statement in (11) can be replaced to give

(12) 3_r<x|/ • • • ^>^i^> = <^i' ' • • '^n,^ where P^ (u^, . . . ,Uj^,vars) ;

x, — X, ; X2 — ^2 ' ' • ' ' ^j, ~ ^n ' ' +

-33-

The new places introduced into R by this substitution should
initially carry no assumptions or assertions.

Conversely, if R contains the code text (12), if the
variables x, ,...,x' appear nowhere else in R, and if no
assumptions or assertions are present in (12) except perhaps
at the places 3_ and 6 , then (12) can be replaced by (11) ,
in which case any assumptions and assertions present at 6_
or B, in (12) should be carried over to the corresponding
places in (11) . (This rule can be obtained by combining rule
(l.b) above with the dead variable and redundant assignment
rules to be stated shortly.)

(l.g) Any occurrence of the expression 3{expn] in a
correct praa R can be replaced by an occurrence of expn , and
conversely.

The following proof rule follows by the argument given
in justification of (l.e) :

(l.h) (Subblock transformation principle) Let R be a
praa, and let B be a block of code in R having only one entry.
Let T\ immediately precede the first statement of B, let tt
be a place in B, and let tt^ be a place not in B. Let R' be
the praa consisting of B and of all the functions which
might be called directly or indirectly from a statement of B.
Let v, ,...,v be the set of all variables of B which are not
dead at r] , let v, , . . . ,v be variables of R which appear
nowhere else in R. Let vars be the variables of R, E be
the assumptions of R, let E' be the subset of these assump-
tions which are at places in R' , and let P = P(v, ,...,v ,vars)
be a predicate having exactly the indicated free variables.
Then if in R' we have

[t]] E' u {(v^=v| &...& v^=Vj^)^} I- (P(v]_,...,VjJ^,vars))^

and if in R we have [Tr^]E |— (P^ (v, , . . . ,v )) for a predicate
P, with the indicated free variables, then in R we have

[71^] E |- ( (3v^, . . . ,Vj^) ^i^v^, . . . ,v^) & P(v^, . . . ,Vj^,vars) )^.

Auxiliary General Travis formation Rules.

Next we shall state a class of rules which are general in
that they can be applied both to praas and to programs. However,
we shall be careful to state the forms of these rules which
apply to praas. We continue to assume that R is a valid praa,
and of course all the transformations we describe will preserve
praa validity.

GAoap J: Labtt-fi(Ltate.d. fiutz^ .

(2. a) A label L not otherwise appearing can be inserted
anywhere in R, thus introducing a new place it imjnediately
following L, with no assumptions or assertions at r, .

(2.b) If there is no i_f ... then go to L statement
in R referencing a given label L, and 3_,L:,3,/ then we can
move all the assertions and assumptions at B. to 3 , and
remove L, thus eliminating the place B , •

(2.c) The statement B_ , if^ false then go to L, 3 , can
be eliminated, provided that we move all assumptions and
assertions at 3, to 3_ and then eliminate 3+ • Similarly, a
statement of this form can be inserted anywhere in a praa, thus
introducing a new place tt immediately following it, with no
assumptions or assertions at tt .

(2.d) In the special context 3_, _if C then go to L; L: ,3^,
we can delete the if -statement , provided that all the
assumptions and assertions at 3_ are moved to the place
following the if-statement and that the place 3_ is eliminated.
Conversely, if L is a label not otherwise occurring, we can
introduce the combination

if C then go to L; L:

at any point in R, thus introducing two new places, initially
with no assumptions or assertions at either of these places.

(2.e) (Will-go-to rule) If tt, if C then go to L, 3^; if
the statement following the label L is if C^ then go to LI , if an
assertion P is available at tt and if P & C =» CI, then the state-
ment if_ C then go to L may be replaced by if^ C then go to Ll, and

conversely.

-35-

(2.f )( Wont-go-to-rule) If it, if C then go to L,B^; if the
context following L is if^ C^ then go to LI; L2 : if the assertion P
is available at tt , and if P & C =^ ~IC1, then the statement
if C then go to L may be replaced by if_ C then go to L2 , and
conversely.

(2.g) (Go-to splitting) Given any boolean expression C, ,
the statem>ent if^ C then go to L can be replaced by the pair
of statements _if C & C^ then go to L; if C & nc, then go to L .
This introduces a new place between the two if-statements ,
and initially there will be no assumptions or assertions at
this place.

(2.h) (Go-to combination) The contiguous pair of
statements

3_, if^ C, then go to L; i_f C„ then go to L,6,

can be replaced by the single statement

if C, V C then go to L;

provided that all assumptions (resp. assertions) at the place
thereby abolished are moved to the place B_ (resp. B, ) .

The go-to rules that we have just stated can be seen
to have a certain interesting completeness property: essentially,
all other rules involving ao-to's only can be obtained from
these rules. Nevertheless, other more 'compound' go- to
rules are worth stating as conveniences. A useful rule of
this type is

(2.i) (Interchange of successive if-statements) If
6_, i_f C, then go to Ll; i_f C then go to L , 8 , then the
two successive if-statements can be replaced by the
combination if C„ '^ ~1C1 then go to L2; if CI then go to Ll;
provided that all assumptions and assertions P at the

place IT between 6 and 6. are converted to assumptions

3
and assertions ("1C,'*P) " at 3_.

To derive rule (2.i) from the preceding rules, we can

proceed as follows: Given

-36-

if C, then go to Ll;
if Cry then go to L2;

use rule (2.d) and then rule (2.g) to get

if C2 '^ ~1C, then go to L;

if C2

A c, then go to L;

L:

if CI then go to Ll;
if C2 then go to L2;

where L is a label not otherwise occurring. The second line
is superfluous by (2.d); (2.e) can be used to replace the
occurrence of L in the first line by Ll; the label L can

IT

then be dropped;

and since the assertion |— (~IC2) i.e,
(C2 = false)" , can be deduced at the place tt iimnediately
preceding the final if^ statement, equality substitution can
be used to replace this statement by i£ false then go to L2,
which (2.c) allows us to remove.

The transformation of i_f C then go to L into
if ~1 C then go to L ' ; go to L ; L ' :

where L' is a label not otherwise occurring, is a special
case of ( 2.i) .

The enthusiastic reader can amuse herself by using the
go to related rules stated above to justify the following well
known while loop transformation, in which Bl and B2 designate
arbitrary praa subblocks; transform

whi

Le C;

if CI then

Bl

else

B2

end if;

end

while;

into

while C;

while C & CI;

Bl
end while;
while C & "ici;

B2
end while;

end while;

-37-

(This transformation introduces new places into a praa;
neither assumptions nor assertions will initially be present
at these new places . )

(2.j) (Isomorphic code rule) Consider two disjoint
subsections s,,s_ of a praa R, each beginning with a label.
Suppose that both are contained within the same function of R
(resp. the 'main' program of R) , and that both consist of
unbroken contiguous sequences of program statements running
up to a final go- to or return statement. Then s. and s- are
said to be isomorphic if the statements, assumptions, and
assertions of s^ can be converted into the corresponding
statements, assumptions, and assertions of s- simply by
replacing each occurrence of any label attached to a statement
of s^ by the label appearing in the corresponding place
in s^.

Rule: If s, and s. are isomorphic, then any statement
of the form if C then go to LI, where LI is a label of s^ ,
can be replaced by i£ C then go to L2, where L2 is the
corresponding label of s_.

Using this rule and the dead code insertion rule (l.d) ,
we can readily derive the following rule, which is often
convenient.

(2.k) (Isolated block duplication) A subsection of a
praa is said to be isolated if it consists of an unbroken
contiguous sequence of program statements running from an
immediately preceding go-to or return statement, up to and
including a final go-to or return statement. A place ir in
a praa is said to be safe if the assertion {false) is
available (so that execution can never reach it) .

Rule: A duplicate of any isolated subsection s of a
praa R may be inserted at any safe place in R, provided that
a subsection belonging to a given function (resp. to the main
block of R) is inserted only in a place belonging to the
same function (resp. the main block) , provided that each

-38-

occurrence of all the labels L attaching to statements in the
duplicated section are changed to occurrences '^^ ^^^ labels L
net otherwise appearing in R, and provided that all the
assumptions and assertions at places within the section
being duplicated are also duplicated = When s is duplicated,
any statement of the form if C then go to L may be changed
to if. C then go to L ' , where L is a label in s and L' is
the label in the duplicate section which corresponds to L.

Note that if we apply rule (2.k) in a manner which
makes all the code in s dead, then it reduces to a rule
isolated code sections to be moved to any safe place in
a praa.

The following rules, which are easy consequences of
(2.j) and (2.k), are sometimes useful.

(2.£) (Go-to-pulling) If 3_, 22. to L, 3^ , and if
the context following the label L is L: statement; L':,
then 6 , go to L can be replaced by 3_, statement; go to L',B^;
provided that every assertion and assumption present at
the places before and after statement in its initial context
is carried over to the appropriate place before or after
the new copy of statement .

(2.m) (Go-to pushing) If 6_/ statement; go to L' , 6.^;
if the context preceding the label L' is L: statement; L ' : ;
if precisely the same assumptions and assertions appear
at the place 6_ as at the place following the label L, and
if precisely the same assumptions and assertions appear
at the place preceding the statement go to L' as at the
place preceding the label L', then B_, statement; go to L ' , B^
can be replaced by 6 _, go to L, B^. When this change is
made, the assvimptions at B_ can be dropped, and the
assertions at B_ kept.

The next few rules state various obvious facts having
to do with the use of labels.

(2.n) (Assertion movement) In the context B_f L^:L2:,B^
any assertion at the place tt between L^ and L^ can be moved
back to B and any assumption at tt can be moved forward to B^-

-39-

(2.o) (Label permutation) If there are no assumptions
or assertions at the place between L^ and L-, then L^:L_ can
be replaced by L_:Lw any statement if^ C then go to L, ;
can be replaced by ijE C then go to L„, and conversely.

Croup 2: Rules relating to assignment statements .

(3. a) An assignment statement of the form x = x can be
inserted anywhere in R, thus introducing a new place tt
immediately following it, with no assumptions or assertions
at IT. Conversely, if 6_, x = x, B, then the statement
X = X can be deleted, provided that we move all the assumptions
and assertions at B_ to B, and eliminate B_.

(3.b) Definition. A variable x of R is said to be
dead at a place tt in a praa if there is no path from it
through the prograiri Q of R which reaches a use of x (either
in a program statement or in an assertion or assumption)
without first passing through some assignment whose target
variable is x.

If IT is a place at which the variable x is dead, then an
assignment statement x = expn or x = Bexpn can be inserted
immediately before tt , thus introducing a new place 7r_ immediately
preceding the assignment statement, with no assumptions or asser-
tions at tt_. Conversely, if 'tt_, x = expn, t\ and x is dead at tt ,
then the statement x = expn can be deleted, provided that we move
all the assumptions and assertions at tt_ to tt and delete tt_.

(3.c) (Shadow variable rule) A family F of variables appear-
ing in a praa R is said to be a shadow variable family if none of
the variables of F appears either in the controlling boolean expres-
sion C of any statement 'if^ C then go to L, in any assumption or
assertion of R, or in any expression assigned to a variable not in F,

Rule: If all assignments to the variables of a shadow
variable family are deleted from R, then R remains correct.

(3.d) (Renaming rule) The labels and the variables
occurring in the statements, assumptions, and assertions of a
praa can be renamed in any fashion, provided that every occurrence

-40-

of every variable and label receives the same new name, and
provided that no two variables or labels having originally
distinct names receive the same name.

(3.e) (Dead variable re-use) Suppose that R is a correct
praa, that x and x, are two variables of R which do not occur
either in two different functions of R or one in a function
and the other in the main block of R, that B is a subregion
of R, that X is dead at every place in B, and that x^ is dead
at every place of exit from B, i.e. every place which is
either followed by

(i) a statement i£ C then go to L, where the place
following L is not in B;

(ii) a statement return e;

(iii) a statement if C then go to L, with C different
from the constant true, and with the place
following this statement not in B;

(iv) a statement or label s of any other form, and with
the place following s not in B.
(We define the notion 'place of entry into B ' similarly,
but do not give the details of this definition, leaving it
to the reader to work them out.) Then if we replace every
occurrence of x in B by an occurrence of x, , and then insert
an assignment x = x, at every place of entry into B, R remains
correct.

Note: This rule can be derived by using rule (3.b) to
insert the assignments x = x^ at every place of entry into B
and assignments x = expn immediately prior to each assignment
X, = expn with target variable x^. If this is done, then
(x = x^)"^ will hold for each place ir of B, so that the equality
substitution rule stated previously allows each occurrence of x^^
in an expression, assumption, or assertion in B to be replaced
by an occurrence of x. After this replacement the assignments
to X occurring in B become dead and rule (a.b) can be used
to delete them.

-41-

Group S. Rules relating to function calls.

(4. a) Any group G of functions which is never called
either from the main block of a praa R or from any other
function not in G can be removed, provided that all the
assertions and assumptions at these functions and at places
within them are removed at the same time.

(4.b) (Moving code on-line) Any function call

6_, X = f(expn^, ,expn )/3^ can be replaced by the

block of code constructed as follows:

(i) Let ^i'""^^ ^^ ^^^ variables, y-^'-'-'^^
be the parameters, and L,,...,Lj^ be the labels occurring
in the statements of f. Let y ' ,y-j^/ . . • ,yj!^ be a set of
variables, and L ,L.,...,L, be c. set of labels, not
otherwise occurring.

(ii) Take the text of f, and using it build up an
'online variant' of f as follows: replace the header line
of f by the set of assignments

y^^ = expn^ ; -- - , Y^ = ^xpn^^ .
Replace the trailer line ('end') of f by
L': ^ Pi^y^yi'-'-'^m)

I- P2(y''^l"*-'^m^

where P, (resp. V ) is the conjunction of all assumptions-at-f

(resp. assertions-at-f ) (each of which is a proposition of

I
the form P (y ,y^, ,y^) .

In the remaining text of f, replace every occurrence
of the variable y. (including occurrences in assumptions and
assertions) by an occurrence of y., j = l,...,n; and replace
every occurrence of the label L . by an occurrence of L . ,
j = l,...,k. Then replace every ' return expn ' statement
by

y ' = expn ; go to L ' ;

-42-

(iii) Having in this way built up the online variant
olvt of f, replace the function call x = f (expn, , . . . ,expn )
by

olvt', X = y' .

(4.c) (Moving code off-line) Let R be a correct praa,
and let B be a siobsection of R all of which belongs either
to a single function of R or to the main block of R. Suppose
that B consists of a contiguous group of statements (with
attached assumptions and assertions) , running up to but not
including a label L . Suppose that no statement
if C then go to L outside B involves a label L present
inside B, and that no statement of this form inside B involves
any label L outside B other than the label L . Let the
variables appearing in the statements of B be ^i' ' ' ' '^m '
and suppose that of these variables the subcollection
y, ,...,y are those not dead at the (necessarily unique) entry
place of B, while the subcollection y, ,...,y^ are
those modified by some statement of B. Let f be a function
name distinct from the names of all functions in R, and intro-
duce a new function with this name, as follows:

(i) Let the labels attached to statements of B be
L, ,...,L . Introduce new variables y ' /y-I / • - • ^y ' / ^\'--''^'^

and labels L' L',...,L' distinct from all the variables and

1 p

labels occurring in R, and substitute yw...,y'^ L',L ',..., L'

for yw...,y , L®,LwL_ , . . . ,L^ respectively in all the
1 m i. z p

stateiiients , assumptions, and assertions of B, thereby
obtaining a new text B ' .

(ii) Choose n'>n, k'<k, £'>il, and surround
B' by the following header and trailer lines:

B'

function f (yV , . . . /y^^i ) ;

i'l =,yi'---'^n = ^n'
return <yj^, , . . . ,7^^^ ,>;

end;

(iii) Add f to the collection of functions of R ,

introduce a new variable t not otherwise occurring, and

replace B by the code fragment

-43-

t = f (yj^,...,yj^,); y,^, = t(l); ..., y^^, = y(k'-£'+l);

Initially, no assertions or assumptions should be present
at any of the places internal to this code fragment.

The following rule, which allows one function call
to be substituted for another, will often be useful in
connection with applications of rule (c) .

(4.d) (Isomorphic function rule) Let R be a correct
praa, and let f and f be two functions of R. Suppose that
there exists a 1-1 mapping which interchanges the variables
and labels of f with the variables and labels of f
in a manner which converts the parameters of f to the
parameters of f, the sequence of statements constituting
the code text of f into the text of f, the assumptions
and assertions present at the various places of f to the
corresponding assumptions and assertions present at the
places of f ' , and vice-versa. Suppose that this same
interchange converts the set of assumptions-at-f and
assertions-at-f into the set of assumptions- and
assertions-at-f ' , and vice-versa. Then any function state-
ment X = f (expn, , . . . ,expn ) appearing in R can be changed
to x = f ' (expn, , . . . ,expn ) , and vice-versa.

(4.e) (Function call insertion) In order to state
this transformation rule, it is convenient to make a preliminary
definition. Let R be a praa with assumptions E. Let f,g
be functions of R, and let tt be a place in g. Let P^ and
P- be predicates at g and at tt respectively.

Definition. We write [f]E |- P^ (resp. [f]E |- P^)
if the assertion P^ (resp. P ) holds in the praa R' obtained
by modifying R in the following way: letting x,x, ,...,x be
variables of R not occurring elsewhere, replace the main
block of R by the statement x = f {x^ , . . . ,x ) (i.e., by a
single, direct call to f ) .

-44-

Rule: Suppose that R, E, and f are as above, and that
for every assertion-at-a-f unction P^ and every assertion-at-a-
place F, for which the place tt is within some function g of R
we have [f]E |- P*^ and [f]E |- P^. (If this is the case,
then we shall say that f allows entry.) Let tt ' be any place
within R, and let x ' be a variable not otherwise occurring
in R. Then if we insert the function call

x' == f (expn, , . . . ,expn );
1 m

at TT ' , R remains correct. (No assertion or assumption should

initially be present at the place following this newly

inserted statement.)

Note that the conditions [f]E ]- P^ and [f]E |- p!^ depend
only on the set of functions of R, not on the main block of R.

Application of transformation (4.e) will often be
facilitated if the following simple proofrule is used
first.

(4.f) Let R be a praa, let f, g be functions in R,
TT a place in g. Suppose that no sequence of function calls
cp.n lead directly or indirectly from f to g . Let E be the
set of assumptions of R. Then we have [f]E |— P-^ and
[f]E |— p!' for any predicates P^ at g and P at tt respec-
tively .

It will often be appropriate to apply rule (e) in the
context

(13) B / <Xw...,x > = <u, , — ,u^> where C(u,, — ,u^,vars),S
— i n i n in t

thus replacing the where statement by one or more function calls.
The following rule, easily derived from (4.e) , facilitates
this kind of application.

(4.g) Let R be a valid praa with assumptions E. Suppose
that f is a function of R having m parameters, and that f allows
entry. Suppose that expn^ , . . ,expn are expressions in the
variables vars of R, and that in R there exist assertions

-45-

f p-

P at f and P, at 3_ such that

(14) E [— ((Vr) P, (vars) & P(r, expn, , . . , , expn )

B_
=* C(r (1) , . . . ,r(n) ,vars) )

Then if x' is a variable not otherwise occurring in K, the
where statement in (13) can be replaced by a function call
and a sequence of assignments, giving

e_,x' = f (expn^ , . . . ,expnj^) ;

x^ = x' (1) ; , x^ = x' (n) ; , 6^

Initially, no assertions or assumptions should be present
at any of the places introduced when this replacement is made.

To justify this transformation, we can reason as
follows: By rule (4.e), a function call x' = f (expn. , . . . ,expn )
can be inserted immediately following B_. This introduces
a new place it immediately following the function call. By
the function call proof rule (i) of Section (2.b) above,
the assertion

|- (P (vars) & P (x' ,expn^, . . . ,expn^) )

holds at IT. Hence, using (14) , it follows that

1- (C(x' (1) ,...,x' (n) ,vars))^

also holds at ti . Rule (l.b) now tells us that the where

statement in (13) can be replaced by the set of assignments

x, = x'(l); ..., X = x'(n); which completes the proof that
1 n

transformation rule (4.g) preserves validity. Q.E.D.

-46-

A general remark on praa transformation rules.

Each of the transformation rules stated in the present
section describes a procedure which manipulates the text of
praas and which has the property that if its input is a
correct praa then its output is also a correct praa. VJe
can think of these procedures as collectively constituting
the internal procedure library of an implemented praa-
verif ication/ modification system VM whose essential
property is that it will never accept a praa unless it is
correct, and never modify a praa in a manner spoiling correct-
ness. Given the initial procedure library of VM, other
procedures which preserve correctness can of course be
de-'/ised by com.pounding the procedures of VM. However, there
exists a more general, and sometimes more efficient and conven-
ient miethod for extending the set of rules for correct- praa
transformation which a systemi like VM. will admit. Namely,
a procedure which recognizes the boolean formula CORR(t)
expressing the statement 't is the text of a correct praa'
can be made part of VM; then, whenever VM has been used to
prove the correctness of a praa R with the sin^if- assuit-ption
^ CORR(t) at its entry place and carrying the assertion
|— CORR(t) at its exit place, the procedure defined by R
can be accepted into VM. We call this 'meta-rule', which
allows us to expand VM ' s internal procedure library,
the metamathematical extensibility rule. Various technical
issues connected with this rule and with related meta-rules
applying to proof-checker programs will be discussed in
a subsequent paper.

-47-

3 . Praa-Manipulation Illustrated,
a . Successive Ref ine:nftent .

In the present section, we shall illustrate the use of
the rules for correct-praa modification and combination
stated in the preceding section, specifically by transforming
the sort-by-counting praa considered in sections 1 and 2 into
a series of more and more efficient forms expressed at steadily
lower language levels, until finally we develop a correct praa
embodying the same algorithm but expressed entirely in an
assembly language. However, before doing so, it is appropriate
both to comment on the intent of the sequence of examples to
be given, and also to give general descriptions of a number
of useful praa manipulation techniques.

The praa manipulations described below are best
regarded as scenarios depicting interactions with a hypotheti-
cal, implementable but of course still unimplemented , inter-
active, 'correctness-preserving editor'. Such a system will
permit its user to make various changes in an initially given
praa. The most elementary of these will be usable without
constraint, but in the case of less elementary manipulations,
justifying assertions will be demanded.
These assertions are groupable into two pragmatically
distinguishable classes: on the one hand, those whose proofs
are simple and stereotyped enough to be generated rapidly
by a program analysis system not much more complex than orogrcim
analyzers/optimizers like those currently under development;
on the other, assertions with proofs complicated enough for
recourse to a full-fledged proof -verification program to be
necessary. Our aim in taking the approach we do is to ensure
that all, or at any rate most, of the proofs that need to be
supplied in support of praa manipulation belong to the first
(superficial) rather than the second (deeper) class. The
illustrations to be given will hopefully create the impression
that this is indeed the case; however, the reader should be
warned that it is all too easy for an author to create this
impression by casting formal arguments into natural language

-48-

forms which mask the irritating complications that arise when
one must really communicate with an implemented system.

Wishing to emphasize the fact that all the praa transfor-
mations that we carry out are fully justified by the rules
stated in the preceding sections, we shall pursue these trans-
formations to quite a low level of detail, indeed to a level
which could be left to a compiler, especially to a very high
level compiler able to accept general directives concerning
transformations to be applied and to refuse service when
acceptable forms of the assertions needed to justify these
transformations are not available. Of course, when we can
do so it is even better to rely on an automated trans-
formation system of this type than to use a praa manipulation
system directly, since a system able to generate a
class of program transformations will be able ipso facto to
assume full responsibility for justifying these transformations.

Certain commonly occurring and quite general transforma-
tion techniques are of particular importance, and it is well
to describe them before proceeding to any more specific discus-
sion. To begin with, note the obvious fact that if we
strengthen the assumptions of a praa R by adding new assumptions
and by adding extra clauses P, which convert particular initial
assumptions ^ P^ to stronger forms ^ (P & P-,)^, correctness
will be preserved. The clauses P^ can involve free variables,
i.e. new set-theoretic objects, which do not appear in the
original form of R. Now it may be that the added clauses P,
imply the clauses P originally present; then P^ =* P & P, ,
so that the hypotheses ^ (P & P-,)^ can be replaced by
^ P^ , and the resulting praa will still remain correct. The
newly added assumptions P, may imply identities and inclusions
not available in the original praa R, and these identities
and inclusions can allow certain of the expressions originally
present in the code text and assertions of R to be replaced by
other expressions which involve the new objects, i.e. those
appearing initially in the clauses P, , rather than the variables

-49-

originally present in R. If these old variables are not
assignment-targets in R then this replacement can be carried
out systematically, and we may even succeed in eliminating
certain of the old variables completely from all the
statements and assertions of R. When this happens, the
only remaining occurrences of these variables x will be in
the assumption clauses P, themselves. If such a point is
reached, and assuming now that the only assumptions in which
X appears are assumptions at the entry place tt of R, we can
hope to apply the following

Lemma (Variable Dropout) . If a variable x of R appears
in the assumptions ^ P of a praa R at only the entry place
IT of R, and never appears either in the program text or the
assertions of R, then R will remain correct if each predicate
P = P(x, other_vars) appearing in such an assumption P is
replaced by ( 3 u^ P (u , other_vars) .

Proof: Let R' be the praa obtained by modifying the
assumptions ^ P in the manner indicated, and let c ' be a
computation satisfying the assumptions of R. Let the
'other_vars' appearing in our hypothesis be Xw . . . ,x , let
o, ,...,o be the values assigned to these variables by the
first state of c', and let o be any set-theoretic object
satisfying P(o,o, ,...o ). Then if we modify each state s'
of c' by constructing a new state s for which s (x . ) = s ' (x . )
for all j = l,...,n and s (x) = o , we obtain an R-computation
c which clearly satisfies all the assumptions of R. Thus c
must satisfy all the assertions of R, which clearly implies
that c' satisfies all the assertions of R'. Q.E.D.

One common way of applying the technique just outlined

will be to select certain variables x, ,...,x which appear

in R but which R does not modify, then to introduce m new

variables r, , . . . ,r and n set-theoretic functions * . (r, , . . . ,r ),

1 m Dim

j = l,...,n, and to supplement the initial assumptions of R

by the clauses x. = d).(r, ,...,r ), j = l,...,n. Then clearly
J 3 ^3 1' ' m -^

-50-

every occurrence of x . in a statement, assumption, or assertion

can be replaced by an occurrence of (j) . (r, , . . . ,r ) ; and after

3 1 m

this is done the only appearance of any of the variables x.

will be in the clauses x. = 4) . (r, , . . . ,r ) themselves. But

3 ^3 1 ' ' m

then the variable dropout lemma stated above allows these
clauses to be replaced by (3 x) (x = 4; . (r, , . . . ,r ) ) . Since
()) . (r, , . . . ,rj^) = 4) . (r, , . . . ,r.^) this existentially quantified
equality is universally true, and can therefore be dropped as
an assumption. The overall effect of this is simply to
substitute 4; . {r^ , . . . ,r^) for x. at each of its occurrences.
This technique, which stands in exact analogy to the technique
of generating new predicate theorems by substituting arbitrary
terms for the free variables of old terms, may be called the
method of substitution in a praa.

Wliat may be called the technique of representatior
goes beyond the substitution method that we have just described.
This technique can be described as follows. Consider some sub-
collection x,,...,x of the variables of a praa R, and consider
all the expressions, occurring either in program statements
and in assumptions/assertions, in which these variables appear.
These expressions will have the form e(x,,...,x ,other_vars) .
Some of these expressions will appear in assignments of
the form

(1) X. = expn(Xw...,x , other_vars) , j = l,...,n;

others will appear in other contexts. We call expressions
which appear in a context (1) active expressions , and call
all other expressions expn (x, , . . . ,x ,other_vars) passive
expressions . Suppose that we can find some collection
r_,r-,...,r of auxiliary variables, together with

(i) n set-theoretic functions
4)^(r ,...,r ,other_vars) , ..., cf) (r , . . . ,r^,other_vars) ;

(ii) for each passive expression e (x, , . . . ,x ,other_vars)

in which x, ,...,x appears, another expression

e'(r, ,...,r , other vars) such that either
1 m —

-51-

(ii.a) e((t)^(r^,... ,r^,other_vars) , . . .

'^n^^l' ■ ' • '^n,'°'ther_vars) ,other_vars) ) =

e' (r^, . . . ,r^,other_vars) holds identically; or
(ii.b) a proposition P{x,,...,x ,other_vars) ,
available in R immediately before the place of appearance
of the expression e, such that the implication

(2) P(({)^(r^, . . . ,rj^,other_vars) , . . . f4>j^(r-|^, . . . ,r ,other_vars) ,other_vars)
=> e((j)^(r^,. . . ,r^,other_vars) , . . . ,4)^ (r^ , , . . ,r^,other_vars) ,other_vars

= e ' (r, , . . . ,r , other vars)
1 m —

holds universally.

(iii) For each active expression appearing in a context

(3) x. = e(x, ,...,x , other vars) ,

J 1 m —

a set of m set-theoretic expressions e.(r,,...,r .other vars),

D 1 ni —
j = l,...,m, and an assertion (P(x , ...,x ,other_vars) ) ^

known to be true at the place tt immediately preceding the

assignment (3) , such that the implications

(4a) P{e^ (r ,. .r .other vars) ,... ,e^(r, ,. . r , other vars) , other vars)
± ± m — mim — —

=> <i>^ (e^ (r^, . .r^,other_vars) , . . . /©^(r^, . .r ,other_vars) ,other_vars)
= <J>£ (r^, . . . ,r ,other_vars) for lf.i£n, i^^j
and

(4b) P (e^ (r^^, . .rj^,other_vars) , . . . ,e^{r^, . .r^,other_vars) ,other_vars)

=> <t>. (ej^(r^, . .r^,other_vars) , . . . ,e^(r^, . . . ,r^,other_vars) ,other_var^.
= e (({)^ (r^, . . . ,r^,other_vars) , . . . ,

<t) (r. , . . . ,r ,other_vars) ,other_var^

hold universally. I

If this is the case, we shall say that the functions

(j) . are representing functions which reduce the expressions

e (x, ,... ,x, other vars) to the expressions e'(r, , ,r .other vars)

in— '^ 1 m —

in the context defined by the assertions P.

-52-

Suppose that variables r. ?.nd representing
functions (p . as described above exist. Suppose that we
modify R, first by using the shadovz-variable rule to
introduce assigninents

(5) r = <e, (r,,...,r ,other_vars ) , . . . ,e {r^,...,r ,other_vars) >;
^1 = ^0^^^' •••' ^m = ^0^"^^

immediately before each assignment (3)- and after this, by
introducing temporary assumptions

(6) t=x. = (t).(r,,...,r , other vars) , 1 < i < n

1 il 'm — — —

everywhere. Because of the inserted assignments (5) and the
identities (4a) and (4b) , none of the assignment sequences
(3, 5) spoil the assumptions (6); hence if we include (6)
among our input assuir.ptions , then at every place other than
the entry place of R, the assumptions (6) can become asser-
tions. Using these assertions we can now replace every
remaining passive expression

(7) e(x, ,...,x ,other_vars)
by

(8) e'(r,,...,r , other vars).

1 m —

After this is done, all assignments to x,,...,x can be
eliminated by the shadow variable rule, and the input
assumptions (6) can be existentially quantified using the
variable dropout lemma stated earlier in the present section
and then dropped since once quantified they become true.

The overall effect of this procedure is to replace each
assignment operation (3 ) by an assignment sequence (5) or
something equivalent to it, and to replace every passive
expression (7) by the substituted expression (8) . As already

-53-

noted, we shall refer to this entire procedure as praa
transformation by representation , specifically by use of the
representing functions (^^,...,(p , plus the various reduced
expressions e', and the various assignment expressions

1 m

In most cases, each representing function 4). will depend

on only a very few of the newly introduced variables r, and
will be independent of all ot}ier joars ', thus the full expression
complexity suggested by form.ulae (1 - 5) will rarely be faced.

The logical propositions (1), (4a), (4b) needed to justify
the transformations described in the last few pages may be
called representation lemmas. The proof of such lemmas may
t>e Considered to be the stuff of a fully formalized variant
of the familiar 'data structures' course. Transformation
by representation can be organized into a process resembling
compilation, roughly as follows. Each member of the collection
of justifying identities (2) , (4a) , (4b) available for repre-
sentational use can be assigned some designating mnemonic
or phrase, e.g.

'represent x, by a list r, '
'represent x_ by a B-tree r_ ' .

An appropriate correctness-preserving com.piler can then check
the consistency of such declarations and coding hints, and
either reject them as hopelessly inconsistent, demand that
supporting assertions P(x^,...,x ,other_vars) be attached to
the praa R to be transformed, or deduce these assertions itself
and proceed immediately to produce an appropriately transformed
praa R' .

To wind up this point, note that identities (4a) , (4b)
which define the representation of indexed assignment operators
x.(expn,) = expn- will obviously find particularly frequent use

-54-

As the code text of a praa R is manipulated to bring it
into more and more efficient forms, there will come a point at
which we pass over from the use of set-theoretic objects having
pure value semantics to the use of representing objects which
can be imbedded easily in a comprehensive memory array having
hardware-like logical characteristics, and also to the use of
code sequences which for the sake of efficiency reflect the con-
ventions of pointer rather than of value semantics. We shall
now say a few words about the typical logical arguments which
justify such a transition.

A pointer-oriented data structure S can be regarded as
an indefinitely expansible set of objects, the pointers ,
together with a mapping pto which sends each pointer into a
vector V whose components are either elementary objects (e.g.
integers) or further pointers and also together with an auxiliary
Set E of pointers, which we shall call the entrances of the
data structure S. Each of the set-theoretic objects which
such a structure represents will be defined by some abstractly
specified function p(p, pto) of pointers p e E and of the
comprehensive mapping pto. The functions p used in

this way will ordinarily have inductive definitions; from
the set-theoretic point of view, it is therefore perhaps best
to introduce auxiliary mappings of (p,pto) onto sequences
f = f(n) defined by inductive and initial conditions

(9) f(n+l) = G(p,pto,f(n)) and f(l) =H(p,pto),

where G and H have elementary definitions. For example, if we
consider a conventional LISP-like structure in which the
vectors v are always pairs having components which are either
elementary objects or pointers, then a particularly important
sequence connected with each entry p will be that defined by

(10) f(l) = P; f(n+l) = if nis_pointer ( (pto(f (n) ) (2) ) then nil

else (pto(f (n))) (2) .

-55-

Here is_pointer (x) is assumed to be an elementary predicate
true for objects which are pointers and false otherwise; and
nil is a special pointer used in the familiar LISP manner.
If we take G and H to be given and designate the sequence f
defined by (9) (or by its special case (10))as F(p,pto), then
the set-theoretic object p(p,pto) represented by p and pto
will often be definable in a straightforward manner using
F(p,pto). For example, if we consider a list-like data
structure for which (10) is appropriate, and if lists are
being used to represent sets, we might very well have

(11) p(p,pto) = { (pto(f (n))) (1) [f = F(p,pto) & f(n) ^ nil) .

If we proceed in this way, then each inductive relationship
between sequences F(p,pto) will yield some useful relationship
between the set-theoretic objects defined using these
sequences. For example, in the case (10) we have

(12a)
and

p(p,pto) = n^ if and only if f(l) = nil

(12b)

p ?« nil => p(p,pto) = p((pto(p)) (2) ,pto) u {(pto(p)) (1)},

which among other things can be used to justify the conversion

Of

Vx G p {p,pto) ;

into the list-loop ■

code
end V ;

P' = P?

while p' fi nil;

x = pto(p') (1) ;

code

p'= pto(p') (2) ;
end while;

In cases involving logical relationships too complex
to be described conveniently by simple sequences f having
definitions like (9) , it may be appropriate to consider

-56-

multi-sequences f = f (<n, , . . . ,n, >) which depend on pto
via more complex inductions, e.g.
(13) f (<n^, . . . ,nj^_^,nj^+l>) = G (p,pto,k,f (<nj^ , . . . ,nj^>) )

f (<nj^, . . . ,nj^_^,l>) = H(p,pto,k)

f(<l>) = H(p,pto,l) .

To manipulate a data structure like S we shall use code
sequences cs' containing assignments pto(p) = expn, and
also assignments of the somewhat more special form
(pto(p))(j) = expn, which is an abbreviation for

a4 ) t = pto(p); t(j) = expn; pto(p) = t;

where t is a variable not otherwise occurring. The code
sequences as used to manipulate S will always be chosen so
as to preserve the validity of certain predicates of the form
P(E,pto). These predicates, which may be called the invariant
predicates of the data structure, will therefore always be
available as hypotheses for use in deducing properties both
of sequences (9) and (13) and of set-theoretic objects
p(p,pto) related to such sequences. Moreover, the code
sequences 3s used to modify a data structure will generally
be chosen so as to leave the values p(p,pto) invariant for
all but a finite subcollection ?]_'•• -/Pn ^^ ^^® members of E,
and for these p. one will generally have proved identities

(1

5) p(p.,pto') = expn. (p (p^, pto) ,... ,p(Pj^, pto) )

which relate each set-theoretic object calculated using a
modified mapping pto' to the set-theoretic objects p calculated
using the unmodified pto from which pto' was obtained.

Once again we note that representation lemmas which
establish properties of sequences f defined by recxarsions (9),
(13), or which assert that particular code sequences preserve
important invariant properties of data structures, or which

-57-

imply identities (15) , only need to be proved once and can
then be used to improve the efficiency of a broad variety
of praas.

Up to this point we have been describing arguments
which can be used to justify the transformation of programs
written using set-theoretic constructs into programs in which
only vector-and-pointer constructs appear. However, we have
assumed that vectors of indefinite length are available;
in pragmatic terms, this implies an environment which is
fully 'garbage collected'. Now we shall sketch the techniques
which can be used to transform praas whose code text has this
character into equivalent praas which only involve 'static'
arrays. To do this, we single out some finite subcollection
P, ,...,p of E, introduce associated 'size integers' k.,...,k
and 'address integers' pa,,..., pa ,as well as a comprehensive
memory vector MEM, and insert the temporary assumptions

(16) pto(p.) = MEM(pa.+l: pa.+k.) , j = l,...,n,

where MEM(a:b) designates the 'slice' of MEM running from
its i-th to its j-th components. The shadow variable rule
is then used to introduce an assignment

(17) MEM(pn. + x) = expn

immediately before each occurrence of (pto(p.))(x) = expn in
the praa R being manipulated. If these indexed assignm.ents
are the only operations in R that can change pto(p.), if the
quantities k . are never changed and we assume that on entry
to R we have k . >_ 1 and pa .+k . f. pa ■ . i for j = 1 , . . . ,n-l ,
and if we can show that every x occurring in an assigmnent
(pto(p.)) (x) = expn satisfies 1 <^ x <^ k . , then each
assignment (17) will change only MEM (pa .+1 :pa .+k . ) and not
MEM(pa2+l:pa.+k. ) for any i 7^ j . This allows the assumptions
(17) to become assertions. Using these assertions, we can
replace every use of pto(p.) by a use of MEM (pa .+l:pa .+k . ) ,

-58-

and if this is done systematically it may be possible to
eliminate all uses of p . , and then to eliminate the
variables p. themselves by the shadow variable rule.

So much for generalities; we turn now to an illustrative
example. In the discussion which now follows, we will refer
repeatedly to the transformation rules stated in the preceding
section, sometimes unspecif ically but sometimes specifically
by number. Our manipulations will make use of the general
techniques sketched in the preceding pages, but in order to
emphasize foundations we will sometimes use first principles
to justify these manipulations instead of simply referring
to a general technique by name. Our example is the sort-by-
counting praa developed in the preceding section, but
before turning to its detailed manipulation it is appropriate
to introduce som.e additional notation and a few simple auxiliary
praas . We take the notation

(18) Vx € s;

code

end V ;

to abbreviate

(19) s = n£;

while s 7^ s ;

X = 3 (s - s ) ;

code ;

s = s u { X } ;
end while;

Proof rules for (is) can easily be deduced by expanding (18)
into (19) . The correct praa

-59-

(20) t> N set(s) & g e sing val maps (s ,booleans)
n = 0;
V y € s ;

if g (y) then

n = n+1;
end if;
end V ;
1- n = #{x e s I g(x)} <^

which of course describes the standard technique of counting
by iteration, uses this notation. The correctness of this
familiar praa is easily proved by introducing the obvious
auxiliary assumption ^ n = #{x e s 1 g(x)} at the head
of the while loop which appears when the V-loop in (20)
is expanded.

By substituting {<y, f (y) <f (x) vf (y) =f (x) &place (y) neQ> ,ygs}
for g in (20) and eliminating redundant assumptions, we
obtain the correct praa
(21) ^ ^ set(s) & f G sing val maps (s , reals) & x 6 s

& place e sing_val_maps
n = 0;
Vy e s;

if f (y) < f (x) V f (y) = f (x) & place (y) ne n then

n = n+1;
end if ;
end V ;
I- n = #{yes | f (y) <f (x) vf (y)=f (x) Splace (y) nef^} <]

Since the praa only modifies variables which do not appear in
the counting sort praa R, shown on page 15, we can insert it
into that praa, and then use the equality substitution rule
to obtain the following correct praa, which we call R- :

-60-

O ^ set(s) & f e sing val maps (s , reals)
place = ni_;
Vx G s;
n = 0;
Vy G s;

if f (y) < f (x) V f (y) = f (x) & place(x) ne n then

n = n+1;
end if;
end V ;

place (x) = n+1;
end V ;
|— place e one one maps (s, integers)

& range (place) = {n, l£_n<_ #s}
& (Vx,y e s)f(x) < f (y) =* place (x) <place (y) <1

If a set s has the form s = {n, p <_ n <_ q} , then any
loop of the form (18), i.e. (19), occurring in a correct praa
can be transformed as follows: Introduce a new variable j, initi-
ally a shadow variable, and introduce the assignment j=p immediate-
ly before the while loop of (19) and j=j+l at the end of this loop;
also introduce the assumption f= s-s ={n,j<_n<_q} at the head of the
loop. With this assuiription , the selection statement x = 3 (s-s )

can be replaced by the single statement code-block x = j .

(Cf. Ri xe (l.e)). Once this is done, the assumption

[= s - s~ = {n, j < n <_ q} can be degraded to an assertion,

and the test while s f^ s~ can be replaced by while j £ q.

If no essential uses of s and s~ remain, the shadow

Variable Rule can be applied to remove all assignments

to s and s~. The s will have the assumed form

if we strengthen our input assumption to read

s = domain(f) & vector(f) & (range(f) c reals) , where vector(f)

means that f is a set of pairs, and that domain (f) = { n , 1 <^n<_# f } .

After this transformation, and resurrecting an assertion
not always shown earlier , the preceding praa takes on the form

-61-

^ ^ vector (f) & range (f) £ reals
place = n^ ;
X = 1;

while X £ #f; j— domain (place) = (n, 1 <_ n < x)
n = 0;

Y = 1;

while y <_ #f ;

if f(y) < f(x) V (f (y) = f(x) & y < x) then

n = n+1;
end if;
y = y + 1;
end while;
place (x) = n+1;
x = X + 1;
end while;
I — vector (place) & #place = #f & range (place) = {n,l<_n<_#f}

& (l<_Vx,y£#f)f (x)<f (y)=»place(x)<place(y) i.-^

We shall call this praa R-,. Suppose that we now introduce
a new variable place', make the initial assumption
^ vector (place* ) & #place' = #f, and then insert the
assignment place' (x) = expn immediately before the
assignment place (x) = expn in the praa R . After these
changes, it is easy to see that the temporary assumption

1= (Vz e dom(place)) (place' (z) = place (z))

can be degraded to an assertion. Since y <_ #f implies

y e domain (place' ) , we have vector (place ' ) & #place' = #f

throughout. This allows place' to replace place

in the final assertion of our praa, which in turn allows the

removal of place by the shadow variable rule. The overall

effect of all this is simply to eliminate the second line

of R_ , to replace place by place' in a few other lines.

-62-

and to drop the assertion |— domain (place) = (n, 1 f_ n < x) ,

which no longer plays any role. We shall use R to denote

4

the praa which results from these changes to R .

Now we start to move to a statically ccr.ipiled form
of our praa. This can be done by introducing a new vector,
called MEM (an assumed overall memory array) , by assuming
initially that k = #f, that f = MEM (f adr+1 : f adr+k) ,
where fadr is some integer, and that padr is another
integer, where padr >_ f adr+k, so that the value of
MEM (f adr+1 : f adr+k) is unchanged by any assignment of the
form MEM(j) = expn with padr+1 f_ j 5_ padr+k. We will also
make the initial assumption that place' = MEM (padr+1: padr+k) ,
which subsumes our earlier assumptions concerning place'.

To deduce 1 £ x <_ #f in the last preceding form R.
of our praa is easy, and thus even if we insert the assign-
ment MEM(padr+x) = n+1 immediately before the statement
place (x) = n+1 in R. , the temporary assumption
1= f = MEM (f adr+1 : f adr+k) is never spoiled, and can become
an assertion. But with this assignment inserted, it is
clear that the assumption f= place' = MEM (padrfl : padr+k) is
not spoiled either. Thus references to MEM can replace all
references to / and place' , allowing these two variables to
be suppressed using the shadow variable rule. This casts
our praa into the following form, which we call R-:

{s vector (MEM) & k€ integers & k>_l & padr^integers & fadr^ integers
& padr >^f adr+k

& range (MEM ( f adr+1 :f adr+k ) ) C reals
X = 1;

while X <_ k;
n = 0;
y = 1;
while y <^ k;

if (MEM(fadr+y) < MEM(fadr+x) v

MEM(fadr+y) = MEM(fadr+x) & y < x) then
n = n+1;

-63-

end if;
y = y + 1;
end whi le ;

MEM(padr + x) = n + 1;
X = X + 1;
end whi le ;

f vector (MEM) & range (MEM (padr+l:padr+k) ) = {n, 1 <_ n <_ k}
& (1 £ Vx,y £ k) MEM(fadr+x) < MEM(fadr+y) =*

MEM(padr+x) < MEM(padr+y)

The praa R- has a semantic level quite close to that of
assembly language. To bring it down to what is recognizably
a form of assembly language, we have only to expand the if_
and while statements in R. into their primitive forms,
introduce additional temporary variables to decompose all
compound expressions into their elementary parts, and replace
all operations not available in assem.bly language by
assembly-language code blocks which have equivalent effect
on the variables of Rj.. We can regard our target assembly
language as a collection of code blocks, of unknown internal
structure, which perform elementary operations on a fixed
collection of variables, let us say to be specific X1,...,X16;
the way in which we write assembly langage operations is
illustrated by the typical case Xi = Xj + Xk. We assume that
every assembly language operation either succeeds or aborts
(perhaps simply by never finishing) , and that if it succeeds
it has precisely the same effect as some corresponding
mathematical operation. By making this simple (although
sweeping, and not entirely realistic) assumption, we rule
out all those complications of proof which ensue if assembly
language operations are explicitly allowed to differ in
certain marginal cases from the mathematical operations which
they normally represent. (For a study of these important but
irritating cases, see [Sites, 1974]).

-64-

We also assume that operations MEM(Xi) = Xj and
Xj = MEM(Xi) are available at the assembly language level.
In order to capture at least some of the typical flavor of
assembly language code, we shall assume that no boolean
operations are available, and that the only available
conditional transfer operations have the usual form

i£ Xk >^ 0 then go to L i£ Xk < 0 then go to L
if Xk <_ 0 then go to L i£ Xk > 0 then go to L
if Xk = 0 then go to L if Xk = 0 then go to L .

Since all the rest is quite ordinary, we will consider only
the treatment of the statements

(20) if MEM(fadr+y) < MEM(fadr+x) v

(MEM(fadr+y) = MEM{fadr+x) & y < x) then n = n+1;
end if;

appearing in R^ . We shall initially assume that fadr+x and
fadr+y have been 'loaded' into two registers which we
designate symbolically as Xfx and Xfy; that is, we make the
temporary assumption \= Xfx = fadr+x and f^ Xfy = fadr+y
immediately prior to the code block (20) . Then treating
others of the special register variables Xj as shadow
variables , we introduce assignments

Xcy = MEM (Xfy); Xcx = MEM (Xfx)

immediately prior to (20) . This establishes equalities which
allow us to rewrite (20) as

(21) if_ Xcy < Xcx v Xcy = Xcx & Xfx < Xfy then n = n+1;

end if;

We now manipulate (21) in various obvious ways using the go to
rules (2.a-2.h) repeatedly, give the variable n the new name Xn,
and also make use of a few other special register variables X j ,
introducing appropriate assignments for those we use, we can
rewrite (21) in the following equivalent form, which is of course

-65-

typical of what a compiler might produce:

Xcxmy = Xcx - Xcy ; .

if Xcxmy 0 then go to Add;

if Xcxmy i- 0 then go to Skip;

Xcxmy = Xfx - Xfy;

if Xcxmy > 0 then go to^ Skip
Add: Xn = Xn + Xone /* where ^ Xone = 1 */

Skip:

By applying the same familiar technique to the remainder
of the praa Rj. , we can easily convert it to an equally^
correct praa, whose assumptions and assertions will retain a
high-level, set theoretic form, but all of whose statements
belong to assembly language. Details of this are left to
the reader.

-66-

b. A Class of Root Praas Derivable by Transformation.

- Up to the present point we have taken the notion of
'root praa ' as fundamental and have described techniques
for combination and manipulation of root praas. In the
present section, we shall describe a class of root praas
which can be derived transformationally from underlying
mathematical facts of a particular form, thereby penetrating
somewhat more deeply into the questions of program genesis
that define the pragmatic issues which a verification tech-
nology must face. We begin by noting that, although set
theory makes available a language of powerful global dictions,
programming rules out direct leaps between global totalities,
so that to devise an algorithm one must rely either on a
technique of systematic extension or on a pattern of
decomposition. To be specific, suppose that some set-theoretic
function (or functions) F depending on a composite set-
theoretic object (or objects) x has been defined mathematically,
leaving us with the problem of developing an acceptable
algorithm for the computation of F(x). First consider
algorithms which are based upon the technique of extension.
Such algorithms typically introduce some class of
auxiliary objects z, together with an auxiliary transformation
z -* T(x,z) which, if applied repeatedly to an initial
z^ = S(x), will eventually produce some z from which F(x) can
be calculated directly. Iteration of T may, for example,
enlarge some set, extend some mapping, or progressively
'tighten' some condition satisfied by z until the condition
defining F(x) comes to be satisfied. For verification of
algorithms of this kind, direct use of the praa proof and
transformation methods described in preceding sections is
normally just about as comfortable a technique as can be devised,
though of course the finding of 'minimal' algorithm forms
which facilitate the task of verification but from which the
conventional versions can be derived by easy transformations
is a task requiring careful thought.

-67-

In the case of algorithms which proceed by decomposi-
tion, a more interesting transformational approach is possible.
To calculate F (x) using such an algorithm, we factor F into
a product of simpler maps F . , some of which may decompose x
(or perhaps objects y calculated from x) into a collection of
simpler 'subparts' F.(x) = <G . '(x),...,G: '(x)>. A given
factorization may only be valid when a particular logical
condition P^ is satisfied; if P, is false but some other
relevant condition is satisfied, a different condition may
apply. In general therefore a decompositional algorithm
for the computation of F will rest upon a relationship
of the general form

(1) F (x) = if Pt (x) then f!^^^ ( . . . F ^"'■^ (x) )

1 In-.

else if P-(x) then f|^M . . . F ^^^ (x) )

2 1 n^

• • •

else if P, (x) then F,^^' (... F^^^ (x))
K J n,

k

Note that if the set-theoretic fvinction F will only appear in
the context 3F(x), then it is sufficient to have inclusion
(of right by left) in (1) rather than identity.

As everybody knows, a relationship of the form (1) can
be used to compute F even if F appears in several places on
the right-hand side of (1) , provided only that the argument
values to which F is supplied are in some sense simpler than
the initial argxament x. When this is the case, the relation-
ship (1) is recursive and can be converted directly into a
recursive program for the calculation of F. Now, any recursive
program can be converted into an iteration by introduction of
an explicit stack of appropriate form. Moreover, at each
recursive level we only need to stack information which
cannot be recovered conveniently from the information passed down

-68-

to the next recursive level. In general, any recursion for
which it is possible to keep track of stack contents in a
simple way can be converted to an iteration; and as a matter
of fact numerous useful recursive schemata having this property
have been catalogued and exploited by [Walker and Strong 1972] ,
[Burstall and Darlington 1975] . We list various significant
items from their catalog, assuming at first that the function
F is single-valued.

(i) Assume that

(2) F(x) = if P^(x) then F (M (F (M ... F(N^(x) ...))))

else if P2(x) then F (M (F (M .. .F (N (x) ...))) )

else if Pj^(x) then F (M (F (M. . .F (N (x) ...))) )

with the map M occurring m. times if P . is satisfied. Then
(as observed by Walker and Strong) y = F (x) converts (if x
is dead) to

(3) k = 1;

go to Lstart;
while k > 0;
x = M (x) ;

Lstart: while P. (x) v ... v P, (x) ;

k = k+ _if P, (x) then m else if. . .else if Pj, (x)

then m, ;

X = if^ P (x) then N (x) else if else if Pj^ (x)

then N, (x) ;

end wh

ile; |-"l(Pj^(x) V ... V Pj^(x))

x = F(x) ;
k = k-1;
end while;
y = x;
If all the integers m. are zero, the outer loop is superfluous,
and (3) simplifies to

-69-

(4) while P (x) v ... v P {x) ;

X = i£ P^ (x) then N^ (x) else if

else if P, (x) then N, (x) ;

end while;

y = F (x) ; \— ^{P^ix) w ... w P^ (x) )

(ii) Assume that

(5) F(x) = if P^(x) then M^(H^{x) ,F(N^(x) ) ) else if ...

else if Pj^(x) then Mj^(Hj^(x), F(Nj^(x))) ,

that all the mappings N. have inverses N. , that the predicates
P . (N . (x) ) are mutually exclusive, and that, for each x,
there exists at m.ost one y in the set generated from x by
repeated application of the maps N. which satisfies
n(P (y) & . . . & P (y) ) . We call this value V(x). Then
y = F(x) converts (if x is dead) to

(6) xsave = x;

X = V (x) ; y = F (x) ; |— H (P^ (x) v ... v P^^ (x) )
while X f^xsave;

X = if P^(N~-'-(x)) then N~-'-(x) else if_ . . .
else if P (N~-'-(x) ) then n""'" (x) ;

y = if P^(x) then M^(H (x) ,y) else if . . .

else if P (x) then M(H (x) ,y) ;

end while;

This transformation will commonly be applied to cases in which
the functions M. are independent of their first parameters.
Application of it will often convert a recursive relationship
of the form (5) into an algorithm that works by extension.

-70-

Even if the N. have no inverse, this transformation can
D
still be used if we are willing to search nondeteriTiinistically

over the sets N. (x) .

(iii) Assiome that

(7) F(x) = if P^(x) then M(H^(x), G^ (F (N^ (x) ) ) ) else if...

else if Pj^(x) then M(Hj^(x), G^^ (F (N^^ (x) ) ) ) ,

and that the two-parameter mapping M is associative. We say
that a one-parameter mapping G left-commutes (resp. commutes,
resp. right-commiutes) with M if G(M(x,y)) = M(Gx,y)
(resp. = M(Gx,Gy), resp. M(x,Gy)). Suppose that the range
j = l,...,k. is divided into three subsets £c, c, re such
that G. left-commutes (resp. commutes, resp. right-commutes)

with M for j e £c (resp. j e c, resp. j e re) . Put
crc(j) = if_ j G {c, re} then 1 else 0. Suppose also that
all the G. for which j 6 {c, re} commute with each other.
. Then y = F(x) converts (if x is dead) to

(8) if n(P^(x) V ... V Pj^(x)) then

y = F(x) ; ^ n(P^(x) V ... V Pj^(x))
else

n - = 0 ; . . . ; n, = 0 ;

j = i£ P (x) then 1 else if. . .else if P (x) then k;

y = H (x) ;

while P (x) V ... V Pj^(x);

new

j = if P (x) then 1 else. . .else if Pj^(x) then k;

z = H . (x) ;
new 3

if j e (AcUc) then

z = G. (z) ;
3
end if;

-71-

for m = 1 to k;

if m 6 c then

for i = 1 to n ;

— m

z = G^(z);
end for;

end if

end for ;

y = M(y,z); n . =n .+crc ( j ) ; j=newj; x=N . (x) ;
end while;

z = G.(F(x)); f- n(P^(x) V ... V Pj^(x))
for m = 1 to k;

for i = 1 to n ;

— m

z = G^(z) ;
m

end for;
end for;

y = M(y,z) ;

Frequently encountered special cases of this general schema are
G . (x) = X, j = l,...,k, in which case G. left-commutes with M
and the quantities n. are identically zero, and M(x,y) = y, in
which case all G. right-commute with M; also the more special
case in which M(x,y) = y and G . (x) = G (x) for all j.

(iv) Suppose that (7) holds, that the two-parameter

mapping M in (iii) is both associative and commutative, and

that all the G. = G are the same and left-commute with M.

J
Suppose also that for each x all the u in the set V(x) defined

by the condition "1(P (u) v ... v P (u) ) and by the requirement
that u be generable from x by repeated application of the trans-
formations N. have the same value F(u). Then a code sequence

3
somewhat different from (8) can be used to calculate F (x) .

-72-

As a matter of fact, as observed by Darlington and Burstall,
this alternative code sequence can be used even if M only
satisfies the condition M(x,M(y,z)) = M(y,M(x,z)), which
is somewhat weaker than associativity and commutativity
together. In this case, y = F(x) converts (if x is dead) to

(9) y = G(FO V(x) )) ;
j = 0;
while P, (x) V ... V P (x) ;

z = _if P (x) then H^ (x) else if . . .

else if Pi^(x) then H, (x) ;
if j 5^ 0 then

z = G (z) ;
end if;
j = if_ P, (x) then 1 else if . . .

else if P^ (x) then k;

y = M(z,y) ; x = N . (x) ;
end while;

(v) Assume that

(10) F(x) = if Pj^(x) then M(F(N^(x)) , F(n|(x))) else if ...

else if Pj^(x) then M (F (N^^ (x) ) ,F (Nj^(x) ) ) ,

and that the two-parameter mapping M is associative. Suppose

that Nt,n' ...,N, ,n' all have inverses, and that the ranges
1 1 k k

of these mappings are all disjoint, so that given an x of the
form N.(z) or N*. (z) the z = N~ (x) from which it was obtained
is uniquely defined. (I.e., we can define N as the 'combined'
inverse of all the mappings N^,N^, . . . ,Nj^,Nj^.) Suppose moreover
there exists a boolean function R(x) which is true for all elements
of the form n'. (z) and false for all elements of the form Nj(z).
Then y = F(x) can be converted into

-73-

(11) x- = x;

while P(x') V V P,{x');
x' = if P, (x') then N^(x') else if; . . .

else if P (x') then N (x' ) ;
end while;

y = F(x'); f-n(P^(x') V ... V Pj^(x'))
while x' i- x;

if_nR(x') then
X' = N~-'-(x') ;
x' = if P, (x') then n|(x') else if . . .

else if Pj^(x') then N^', (x') ;

while P(x') V V P (x');

x' = if P, (x* ) then N (x' ) else if , . .
else if P,(x') then N (x' ) ;
end while;

y = M(y, F(x')) ; |— n(P^(x) ... Pj^(x))
else

x' = n"-'-(x')
end if ;
end while;

If there exists a left-identity element for the two parameter

mapping M the code sequence (11) can be simplified. We leave

it to the reader to work out the details of this simplification.

A few additional, but less generally useful cases of
recursions which can be converted into iterations are
found in the cited works of Walker, Strong, Burstall, and
Darlington.

We have already noted that if the set-theoretic function
F appearing in the general recursive relationship (1) will be
used only in the context 3F(x), then (1) leads to a recursive
algorithm that can be used to calculate F, even if only inclusion
and not equality has been proved in (1) . This remark carries
through to the various iterative constructions into which (1)

-74-

can be expanded; all these expansions remain correct if we
replace certain of the set-theoretic functions appearing in
them by functions having smaller set values ("'^mailer' in
the sense of set-theoretic inclusion) , provided that other
of the set-theoretic functions map smaller sets into smaller
sets. In cases of this sort, simple function composition
F^ (F (x) ) will often be replaced by the element-by-element
composition function F [F^[x]] = {z|( u, ,u„) u^ s x &
<u, ,u_> e F, & <u_,z> G F-}. Moreover, in dealing with
cases of this sort, associativity of a two parameter map M
can be replaced by the inclusion M[x,M[y,z]] £ M [M [x,y ] ,z] ,
while commutativity of M and G can be replaced by
G[M[x,y]] 2M[G[x], G[y]], etc.

Whenever it is possible to derive a praa R using one
of the recursion-removal schemata described in the preceding
pages, the derivation is likely to be more advantageous than
any other, since in such a case all that needs to be proved
is the mathematical fact embodied in the recursive relationship
(2). Once this is done, rather complex program structures
such as (3), (6), (8), (9), etc., together with all the induc-
tive assumptions needed to prove their correctness, follow
immediately. Moreover, we avoid the labor of supplying all
the intermediate proof details, instantiations, etc. that
would be needed to prove such a program structure correct even
after it had been supplied with inductive assumptions.

To convince the reader that the recursion-removal rules
displayed above do generate a number of interesting root praas ,
we will give a few examples.

(a) Greatest comivon divisor. Let x and y be nonnegative
integers not both zero, gcd(x,y) their greatest common divisor.
Then

gcd(x,y) = if x=0 then y else if x>y then gcd(y,x-y) else gcd(y-x,x)

converts into a familiar iteration, and

-75-

gcd(x,y) = if odd(x) & oddCy) then

if x>y then gcd(x-y,y) else gcd(x,y-x)
else if x=0 then y else if y = 0 then x
else if even(x+y) then 2*gcd (y/2 /X/2)
else if even(x) then gcd(x/2,y)
else if even(y) then gcd(x,y/2)

leads to a more efficient iteration.

(b) Merging of sorted arrays. Let x and y be two sorted
arrays, and let merge (x,y) be a sorted array with

rangecount (merge (x,y) ) = rangecount (x) + rangeccunt( y) .
Then the relationship

merge (x,y) = if x= r^ then y else if y = n£^ then x

else if x(l)fy(l) then x(l) Bmerge (x(2: ) ,y)
else y(l)B merge (x,y (2 : ) )

leads, since the concatenation operator I is associative, to
a variant of the familiar merging loop. Note that x(2:) is
the vector of all components of x, omitting the first.

(c) Binary search. Let a be a sorted array of reals,
and let S. £ u be integers. Define place (a,£ ,u,x) as the
least index i in the range ^ 1 i 1 " such that a(i) = x,
if there is any such i; otherwise zero. Then

place(a,£,u,x) = if 2.=u then if a(£)=x then £ else 0

else if a(L£+u/2J) >_ x then place (a , £ ,L£+u/2J ,x
else place(a,L£+u/2J+l,u,x)

converts to the standard binary search.

On the other hand, certain algorithms which work with
stacks and which consequently are often expressed recursively
are best regarded as having iterative root forms. For
example, consider the well known algorithm of Tarjan which takes

-76-

an undirected graph G and a node x in it from which every
other node can be reached, and which develops a 'depth first
spanning tree' T in G. Perhaps the most convenient root form
for this algorithm is

(12) nodestack = <x>; nodes = {x}; T = nil;
while nodestack ^ n£ ;

^ range (T) u dom(T) u range (nodestack) £ nodes
& nodestack (l)=x
& (Vj,k, l<_j<k<#nodestack) Q pGpaths (T, nodestack (j) ,

nodestack (k) )
& (Vz G nodes I (G{z} -nodes) j^ nl) z^range (nodestack)
& (Vz G nodes) 3!p ^ paths (T,x,z)

/* 3!p means that there exists a unique p */
if X GG{nodestack(#nodestack) } | x f nodes then

nodestack = nodestack | | <x>; nodes = nodes u {x};
T = T with {< nodes tack (#nodes tack) iX> } ;
else

nodestack = nodestack (1 : #nodestack-l) ;
end if;
end while;

Since successive elements of nodestack are T-descendants of
each other, and since all the elements of nodes which have
descendants not in nodes belong to the range of nodestack,
it is not hard to show, by supplementing the loop assumption,
that whenever y,z g nodes and <y,z> e G it follows that z
is either a T-descendant or ancestor of y, or that in T z lies
to the left of the path leading to y, which is of course a
property fundamental to the use of depth-first spanning trees.

Note that, in spite of its typically recursive use
of a stack, (12) cannot be regarded as a true recursive
algorithm, since it accesses the global variables nodestack,
nodes, and r in a manner forbidden to straightforwardly recursive
functions.

-7 7-

4 . Additional Comments on praa Manipulation.

a. The block sv±>stitution rule revisited; Pramas

The fundamental block substitution Rule (l.e) of Section 2(c)
allows us to combine praas by replacing either single where
statemients or groups of several such statements in a correct
praa R by an auxiliary praa R. which contains appropriate
output assertions. While rather general, this replacement
principle is not quite as general as we would like it to be,
since as nomnally written a praa may contain fewer where
statements than would be ideal for broad application of Rule
(l.e). In the next few pages we will (again follov/ing
Gerhart) address this point, specifically by modifying the
proof formalism described in Sections 2(a,b) above in such a
way as to facilitate insertion and deletion of where
statements. For this, the following definition is appropriate.

Definition. (a) A prama ('program with assumptions and
maximal assertions') R is a program Q (of the language SL) ,
together with three sets E, E', M. As in a praa, E and E' are
are both sets of propositions-at-places and -at-f unctions of Q;
the set E (resp. E") is called the set of assumptions of R
(resp. the set of assertions) of R. The elements of M are pairs
(A,?*^) , where P^' is a proposition-at-a-place or -at-a-function
of R, and where A is a list of variables of R. We impose the
restriction that if a is a place in a function f, then
only variables which do not appear in any function other than
f and which are not arguments of f can appear in the list A.
(If a is a place in the main code block of P, then only
variables not appearing in any function can appear in A) . The
propositions P appearing in pairs (A, p ) belonging to M are

called maximal assertions of R, and A is called the modifiable

a
variable list associated with the maximal assertion P .

We impose the restriction that no prama can contain more than

one maximal assertion at any place or function, and that if it

contains a maximal assertion P at a given place or function,

-78-

then all other assertions Q at the same place or function
which involve any of the variables of P are implied by P.

In heuristic terms, each maximal assertion P states both
that the assertion P is true whenever control reaches the
place a (or whenever the function a is exectued) , and that no
predicate stronger than P is known at a. More specifically:

(b) A prama R is aorrect or valid if conversion of all
its maximal assertions to ordinary assertions turns R into a
correct praa, and if the following additional conditions are
also satisfied:

(b.l) Let (A/P") G M and let a be a place in R. Then R
must remain correct if we insert the where statement

(1) <x,,...,x> = <u, ,... ,u> where P (u,, ... ,u ,other_vars)

immediately following the place a. Here x-,...,x is

the list A of variables, and the predicate P is assumed

to have the form P (x. , . . . ,x ,other_vars) .

(b.2) Let (AfP^) G M/ and let a be a function f in R. Then
the list A must consist of the single variable x and R must remain

correct if we replace any function call

(2) X = f{expn-,..., expn )

in R by the where statement

(3) X = u where P (u,expn, , . . . ,expn ) .

(Note that the form of the proposition-at-a-function f is

necessarily P(u,y, ,...,y ), where m is the number of parameters

of f.)

If A = (x. ,...,x ), and E is the set of assumptions of the

prama R, we will sometimes indicate the presence of the maximal

assertion (AjP*^) by writing E(x,,...,x ) \-\— P . Similarly,

in writing out the text of a prama, we shall distinguish maximal

assertions by prefixing them with the sign (x,,...,x ) H — i °^ r

in case x^ , . . . ,k is the collection of all variables which
1 n

can be changed at a given place or function, simply by prefixing
the sign \-\ — .

-79-

Now we begin to state a set of proof and transformation
rules for pramas, culminating in a discussion of block
substitution in the prama case.

Proof Rules:

(a) The proof rules (a), (b) , (c) , (d) , (e) , (f) stated
in Section 2 (b) above and also the two Induction Principles
(for propositions-at-a-place and for propositions-at-a-function)
stated there carry over from praas to pramas. In applying
these rules, we can use any maximal assertion (A) j-j — P or

(A) H— P as a simple assertion (e.g. we can use (A) |-}— P^ as
|— P , etc. )

(b) Proof rules (g) , (h) , (i) . (j), (k) , (£) , (m) , (n)
and (o) stated in Section 2(b) above carry over from praas

to pramas, provided that in applying any of these rules to deduce

proposition F at the place tt in the prama R we insist that R

contain no maximal assertion (A,Q) at t\ whose list A of

variables involves any of the variables of P. In applying

these rules we can use any maximal assertion as a simple

assertion (in the manner explained in the preceding paragraph) .

We assume throughout the next few pages that P is a

correct prama, that 3, B_, P, , ii", t\ _ , tt , etc. are places

in R, that f, g etc. are functions in R, that the variables

appearing in R are x-,...,x , and that A is the list

X, ,...,x of variables. We will som.etimes call the variables
1 n

of the list A active variables of a maximal assertion
(A) H— P^ or (A) H— P^ , and call all other variables of P
passive variables of such an assertion.

(c) A prama remains correct if the list A of variables
attached to any of its maximal assertions-at-a-place or
-at-a-f unction is replaced by a smaller list of variables.
In particular, a prama remains correct if any of its
maximal assertions is replaced by a corresponding simple
assertion.

-80-

(d) (Maximal Assertion Strengthening) Let R contain
the maximal assertion (A) H— P^ at the place tt , and suppose
that if the maximal assertion were reduced to an ordinary
assertion the additional assertion ] — P at tt could be
deduced, where we assume that the implication (Vx . . . ,x )(P,=* P)
holds identically. Then (A) f-^ — P can be replaced by

(A) [^ P^.

(e) (Union Rule for Maximal Assertions) Suppose that
maximal assertions separated only by a label appear in R, as
follows: „ „

(A) K- P " , L: (A^) H- P^""

Suppose that every assertion of R at the place P_ immediately
preceding the label L which is net independent of the variables
of A^ is implied by the predicate P.. . Let the variables appear-
ing in the list A (resp. A,) be x^,...,x (resp. x, ....,Xj),
and let the list of all varic±)les of R be x ,...,x . Then if
the predicate P is independent of the variables x -,..., x^^,
the maximal assertion (A) \-\ — P can be replaced by

(x^,. .. ,Xj^) ^^ (P & P^)

Proof: It is clear that the assertion -| — (P & P^)
holds at B_. Since P (x^,...,x^) implies every assertion of R
which is at 3_ and which is not independent of x^^. . . ,x^ , and
since each assertion at 3_ which is not independent of x^,...,x^
is implied by P(x.,...,x ), it is clear that every assertion
of R which is at 3_ and which is not independent of x^, . . . ,x^
is implied by P & P, . Hence insertion of the where
statement

(4) <x^,...,x^> = <u^,...,u^> where

P(u^, . . . ,u^,x^^^, . . . ,x^) & P^iu^, . . . ,u^,x^_^^, . .X,

at B_ does not invalidate any of the R-assertions at B_.
Suppose that the statement is inserted at 6_ , and also
that the where statement

-81-

m

(5) <x, ....,x.> = <u, ....,Uj,> where

■•^vX, f... ,X,_i ,U,,. .. fUp f^Qii f» •• I X I

is inserted immediately before the place f in R.

Let R be the prama that results from these insertions,

and let c ' be a computation for the code text R'. Then

since P (u, ,..., u^ ,x„ ,,,..., x ) is independent of the variables
1 X, >^ + l m

u ,,,..., u„, it is clear that any values assigned to the
n+1 £ -^

variables x, , . . . ,x by (4) could also have been assigned
by the v/here statem.ent

(6) <x,,...,x^> = <u,,...,u^> where P(u,, ,u^ ,x^ ,,,... ,x) ,

i n i n i n n+i m

and hence that any values assigned to x, ,...,Xp by (4) could
also have been assigned by the two successive statements (5) ,
(6). Thus, in the presence of (5), the only components of
the computation c' which can differ from the corresponding
components of a computation c for R must be components which
are either at 6_ or at 6 . Thus c' must satisfy all the
assertions of R at places other than 3_ and 3, . But since
any values assigned to x, , . . . , x. by (4) could also have been
assigned by (5), (6) in combination, c must satisfy all the
assertions of R at 6 , and since we have already seen the
same to be true at B , our proof rule follows. Q.E.D.

(f) (Splitting Rule for Maximal Assertions) Suppose that
B , L: , B, / that a maximal assertion of the form

3_
(7) (x^,...,x^) H— (P & P^)

appears at the place B , and that no maximal assertion appears
at B, . Suppose that n <_ £ , that the predicate P is independent
of the variables x _|^,,...,x^, and that the assertion \— Pj_
can be deduced at 6. . Then the maximal assertion
(x,,...,x ) H — P, can be added to R, with preservation
of correctness. _„

Proof : As seen in the proof of (e) above, any values
assigned to x^,...,x^ by the where statement (6) can be
assigned to these variables by (7) . Thus insertion of (6)
into the text of R at 3 will not cause any assertion of R
to become false.

(g) (Reduction Rule) Suppose that (A) H— (P & ^i ^
is a maximal assertion of R and that P.. is independent of
the variables appearing in the list A. Then (A) f-j — (P & P, )
can be replaced by (A) |-| — P , with preservation of
correctness.

Proof : Consider two pramas R^,R derived from R, the
first obtained by inserting the statement (6) with i = n
immediately after the place 6, the second by inserting (4)
instead. We shall simply shov; that both admit the same sets
of computations. Obviously the set of computations which R,
admits is no smaller than the set of computations which R,
adniits . Nov; let c be a computation of minimal length
admitted by R„ but not by R, . Clearly the semi-final
component of c m.ust be at the place 6. If we truncate
the final component of c, we obtain a c' which is a valid
computation both for R, and R-. Kence it must satisfy all
the assertions of R, , and in particular the final component
of c' must satisfy P, . But then since P, is independent of
all the variables of A any final values which can be
assigned to the variables x,,...,x by (6) can also be
assigned by (4) , so that c must be a computation which R,
admits, a contradiction which proves our rule. Q.E.D.

-83-

Transformation Rules

The next rules to be stated justify motion of
maximal assertions backward through the code text of a praraa .
In addition to the standing assumptions described above, we
assume throughout the next few pages that no maximal assvmption
of E is initially at the place 6 .

(h) (Assignment to an active variable) If „
3_, x^ = expn(x^, . . . ,x^) , ^^ , if (A) 'rl— (P (x^ , . . . ,x^) ) ,
and if P (expn (x, , . . . , x ),Xp,...,x ) implies every assertion
of R which is at the place B_ and which is not independent of
the variables of A, then the maximal assertion
(A) |-| — (P (expn (x, , . . . ,x ),x„,...,x )) can be added to R
with preservation of correctness.

We shall give a detailed proof of this rule since it
is the first of its type that we state; detailed proofs will
not be given for subsequent rules of this general kind, since
rather similar arguments can be used in all cases.

Proof: Since — P , it is clear that

, ■ ^-

— (P (expn (x, , . . • ,x ), x-,...,x )) . Moreover, since

' 1 m 2 m

P (expnCx, , . . . ,x ),x^,...,x ) implies every assertion of R
1 m / m

which is at 3 and which is not independent of x, , . . . ,x ,
it is clear that insertion of the where statement

(8) <x ,...,x > = <M^,...,\x > where

P {expn(u, , . . . ,u , other vars) ,u_ , . . . ,u , other vars)
In— /. n —

immediately before the place B_ does not invalidate any
of the R-assertions at 3 • It is also clear that insertion
of (8) at 3 does not invalidate the assertion j — P . Suppose
that the where statement

(9) <x, , . . . ,x > = <Uw...,u > where P(u, ,...,u , other vars)

i n 1 n 1 n —

is inserted immediately before the place 3, in R. It is clear
that in the presence of (9) at 3. the members of the set of
computations for the code text R' containing (8) differ from

-84-

the the computations legal in the absence of (8) only for
computation components v/hich are at either 3_ or 3, • Thus
these computations satisfy the assertions of R' at all places
other than 6_ or 3 , and, since we have seen that all
assertions at 3_ and 3, are satisfied also, it follows that
R' is correct, which proves the transformation rule that
has been stated.

(i) (Assignment to a passive variable) If p
3_, X ^^ - expn(x^, . . . ,x^) , 3+ , if (A) hf— (P (x^, . . . ,x^) )
if P(x , .,.,x , expn(x^, . , . ,x^) , ^n+2'''*'^m^ implies
every assertion of R which is at the place 3_ and which
is not independent of the variables of A, and if expn (x^, . . . ,x^)
is independent of the variables of A, then the maximal assertion

B_
(10) (A) 4— (P(Xj_, . . . ,x^, expn(x^, .. . ,x^) , ^^+2 ' ' * " '^m^ ^

can be added to R, with preservation of correctness.

(The proof is like that of (h ) ; we must assume that
expn (x, , . . . ,x ) is independent of the variables of A since
otherwise insertion of the where statement (8) at 3_ might
influence the course of computation past the place 3^ •
Note that if we are prepared to drop all variables on which
expn (x- , . . . ,x ) depends from A, the condition ' expn (x, , . . .x )
is independent of the variables of A ' can always be made to
hold.)

(j) (Selection assignment to an active variable) If

3+
3_, x^ = 3expn(x^, . . . ,x^) ,6_^ , if (A) H— (P (x^^, . . . ,x^) ) ,

and if (Vu e expn (x , . . . ,x^) ) P (u,X2 , . . • ,x^) implies every
assertion of R which is at the place 3_ and which is not inde-
pendent of the variables of A, then the maximal assertion
(A) |-|— ((Vu e expn(x^, .. . ,x^) ) P (u,X2 , • • . ,Xj^) ) ~ can be added
to R, with preservation of correctness. (Proof like that of (h).)

(k) (Selection assignment to a passive variable) If
B_, Xj^^^ = 3expn(x^,... ,Xj^) ,3+, if (A) H" (P (x^, . . . ,x^)
if (Vu e expn(x^,.. . ,x^) ) P(x^,...,x^, ^'^n+2' * * ' '^m^ implies
every assertion of R which is at the place 3_ and which is
not independent of the variables of A, and

-85-

if expn (x, , . . . ,x ) is independent of the variables of A, then
the maximal assertion

B.

(11) (A) \-\— ((Vue expn(x^, '^m^) ^ ^^1 ' • • • '^n '^' ^n+2 ' ' * ""^m^ ^

can be added to R, with preservation of correctness.

(£) (Conditional Transfer Rule) Let
B_, i_f C then go to L, 3, , and suppose that the place tt follows
the label L. Suppose that (A) \-\— P , and that (A) |-[— P^ •
Suppose that the proposition (C =* P ) & (He =* P) implies
every assertion of R which is at the place B_ and which is
not independent of the variables of A. Then the maximal
assertion (A) \-\— ( (C =* P ) & (He =* P) ) ~ can be added to R,
with preservation of correctness.

(The proof can be adapted from that of (h) ; details

are left to the reader.)

Note that if the condition C in if_ C then go to L is

identically true, then we can alv;ays take the predicate P to

be false, in which case the maximal assertion

B-
(A) H — ( (C =* P, ) & (nc => P)) reduces immediately to

B- 1
(A) f+ Pj^ .

(m) (Label Rule) Suppose that B , L, B,, that
(A) f-j — P , and that the proposition P implies every assertion
of R which is at the place B_ and which is not independent of
the variables of A. Then (A) |-| — P can be added to R, with
preservation of correctness. (This is rather obvious.)

(n) (Function call rule) Let f be a function of R
which allows entry in the sense of Rule (4.e) of Section (2.c);
let B_, X = f (expn^ . . . f expn, ) , B, , and let (A) \-\ — P
Suppose that the maximal assertion (z) f-j — (C ( z ,y, , - . . ,y, ) )
is available at f, and that the proposition

(12) (Vz)(C(z, expn, , . . . ,expn, ) =>P(vars))

implies every assertion of R which is at the place B_ and which
is not independent of the variables of A. Then

-86-

6

(13) (A) H— ((Vz)(C(z, expn^^, .. . ,expnj^) =>-P(vars)))

can be added to R, with preservation of correctness.

Proof : Since R remains correct if the function call is
replaced by

(14) X, = u where C (u, expn. , . . . ,expn, ) ,

rule (j) above implies that the assertion

I — ((Vu)(C(u, expn. , . . . ,expn ) =* P(vars)) must hold at 6_.
Next suppose that we assume that this replacement has been
made and that we further modify R by inserting the statement

(15) <x, , . . . ,x > = <u, ,...,u > where

1' ' n In

(Vz) (C(z,expn^(u^, . . -^'^n+l' * ' '^n^ ' ' * -^^P^^^i' • "^'^n+l* * '^n^^^

at B . Using rule (j) again, we see that these modifications
preserve the correctness of R. Since the function f allows
entry in the sense of Rule (4.e) of Section (2.c), all
assertions encountered during any computation c which begins
at the entry place of f and continues until return from f will
be satisfied no matter v/hat the initial state of c is. Thus,
even if the where statement (14) is replaced by the function

call x = f(expn,, ,expn,) after the insertion of (15),

R remains correct. Q.E.D.

(o) (Function call rule for a passive result variable)
Let f be a function of R, let B_/ ^^+1^ f (expn^ , . . .expn^^) , B^ ,
and let (A) \-\~ P "*". Suppose that the maximal assertion
(z) H— (P, (z,y^, .. .,yj^))^ is available at f, and that the
proposition (12) implies every assertion of R which is at the
place B_ and which is not independent of the variables of A.
Suppose that all the argument expressions expn^ , . . . ,expnj^
are independent of the variables of A. Suppose also that
neither f nor any function g that can be called directly
or indirectly from f contains an assertion that references

-87-

any variable in A. Then the maximal assertion (13) can be
added to R, with preservation of correctness.

The proof is readily adapted from that of (n) ; details
are left to the reader.

Observe that the condition that all expn . are independent
of the variables of A is required for the reason noted follow-
ing (i) above. Moreover, this same condition, supplemented by
the condition that neither f nor any function g that can be
called directly or indirectly from f contains ar assertion
that references any variable in A, can be used in (n) to replace
the condition that f allows entry.

(p) (Proposition-at-a-function Rule) Suppose that the
calls to a function f of R are 3_ , x^ =f (expn|-' , . . .expnj^^ M , B^-"
j = l,...,p. Let the parametersof f be-^y, , . . . ,y, , and let
P be a predicate having exactly k+l free variables. Suppose
that for each j, 1 <_ j <_ p, an assertion \ — Q.- is available at

(A) ^

3 -' , and also that a maximal assertion having the form

(16) (x. ) H— ( (Vu) (Q (x ,. .. ,x. _^,u,x^ _^^,...,x^) &

j -^ j j

P(x^ ,expn|^ Mxj^, . . .x^ 1 '"^i +i' — x^^),...

... expnj^-' (x^,...,x^ _3^'^'^i _^^ , . . .x^^) ) ) )

is available at 3_;-' . Suppose also that the assertion |— P
is available at f, and that this assertion implies all other
assertions available at f. Then the maximal assertion

(17) (z) H-(P(Z/yi'--"yj^))^

at f can be added to R, with preservation of correctness.

Proof: Arguing as in (h) above, we can show that R
remains correct if any call x = f (expn^ , . . . ,expnj^) is replaced
by X = V where P (v,expn. , . . . ,expn, ) . Since \— P^ is available
at f, the present rule follows immediately from the definition

-88-

of maximality for a proposition-at-a-function.

(q) (Return statement rule) Let f be a function of

R, let its parameters be Y-, , . . . ,Y-., and let the remaining

I f

variables of f be Y^+i' • • • 'Y^* ^^^ ^^^ ^~' (P (ZfYo^/ • • • ^Yj^) )

be a maximal assertion at f. Let the place it in f immediately
precede the statement return expn. If the proposition
P (expn,y, , . . . ,y, ) implies every assertion at tt which is not
independent of the variables of f, then the maximal assertion
^^k+l""'^m^ H— (P(expn(y^,...,yjjj) , yj^,...,yj^))^ can be
added to R, with preservation of correctness.

We will normally use the above-stated prama proof and
transformation rules in the following manner. Any proof of
praa correctness will ordinarily begin with the statement of
a group of temporary assumptions; these assumptions will generally
be attached to function entries and to the heads of loops ,
in a manner which (necessarily) breaks every closed path
through the praa R being proved. Often no other statements
than the temporary assumption itself ever needs to be generated
at the place it at which such an assumption is made. If this
is the case, then a maximal assertion built from the assumption
and involving some or all of the variables appearing in it
can be put at it without spoiling the validity proof of R
(since the presence of a maximal assertion at tt restricts
deduction of other assertions at tt, but does not restrict
deduction at any other place). If this can be done, then
the proof of R's correctness will ipso facto prove the correct-
ness of a prama R' , largely identical with R, but containing
maximal assertions not present in R. To know that R' is
correct is of course to know more than the correctness of R;
in particular, the transformation rules stated in this section
allow maximal assertions to be moved about in R'. Once a
maximal assertion (x^,...,x^) f4— P^ has been moved to the
place TT, the following technique can be used to justify
substantial modifications of the code immediately preceding
TT, if such modification is desired:

-89-

(i) Introduce the where statement

<x,,...,x^> = <u, , — ,u > where P(u,,...,u ,x ,,,...x )
i n 1 n ± n n+± m

immediately before the place tt, retaining the maximal
assertion at tt; this introduces a new place tt ' .

(ii) The presence of the where statement at tt ' makes
all the variables x, ,...,x dead at tt ' . Therefore the
dead variable rule (3.b) of Section 2 allows deletion and
insertion of other statements or groups of statements
preceding u ' , provided that these other statements modify
only the variables x,,...,x and perhaps also other variables
used only to calculate values to be assigned to x^,...,x .
Make deletions and insertions, as appropriate.

(iii) Now use the block substitution rule (l.e) of
Section ( 2. c) to replace the inserted where statement by
any appropriate prama.

b. Proofs of Termination

A praa or prama R is said to be terminate for a given
initial condition of its input variables if the set of all
computations which begin with these initial input values
and then proceed from the start of R to any place in R is
finite. (To reduce the standard notion of program termination
to this notion, take a program Q, add the tacit input assump-
tions of Q to Q explicitly, and also add the assumption
^ (false) to the exit place tt of Q, thus obtaining a praa R.
Then Q terminates in the conventional sense if and only if R
terminates in the sense just explained. Note that execution
of a praa is taken to terminate immediately if control reaches
a point at which an assumption is violated.) The question of

-90-

termination has been deliberately systeir^atically neglected
in the preceding pages. Vie shall now discuss this question
briefly, approaching it in a spirit suggested by the
transformational formalisms that have been introduced.

VCliich of the transformations of Section 2.c preserve
termination? This obvious but significant question is
easily answered. Praa termination is preserved vhen the
following transformation rules are applied: (la-d), (If-g),
(2a-o) , (3a-e), (4a-d). Concerning the more complex substi-
tuion rules (l.e), (4.e), and (4.g) we make the following
comments :

Ad (l.e): Let R, R, , L_- , j = l,...,k be as in transfor-
mation rule (l.e), and let gj^i be the place in R^ imm,ediately
following the label L.. Let. the praa RJ result if we insert
the assumption ^ {false) + at each of the places 6_^-' ,

j = l,...,k. Suppose that r' term.inates (so that any suffi-

( i )
ciently long com.putation in R, must reach one of the places 6^ )

Then the praa v/hich results if we fuse R^ into R in the

manner described by Rule (l.e) term.inates.

This assertion can be proved by an easy adaption of
the argument used to prove Rule l.e; details are left to
the reader.

Ad (4.e)' Let R, E, f and R' be as in Rule (4.e),
Section (2.c). We shall say that f allows terminating entry
if f allows entry in the sense of Rule (4.e), and if

-91-

in addition the praa R' terminates. Let it' be any place
within R, and let x' be any variable not otherwise occurring
in R. Assume that f allows terminating entry. Then if we
insert the function call

(18) x' = f (expn, , . . . ,expn )

1 m

at TT ' , termination is preserved.

Ad (4.g) . Rule (4.g) is derived from (4.e) . If in
applying Rule (4.e) we assume that the function f appearing
in the inserted call (18) allows terminating entry, then
termination is preserved.

Ab initio proofs of termination generally combine
references to a program's statement order and block structure
with a f^w supplementary mathematical facts. The following
straightforward definitions and 'termination proof rules'
formalize the techniques most commonly used.

Definition . Let R be a praa. A subsection s of P. is
a set of places in the main block of R, together with the
statements (or labels, v;hich we treat here as 'no-ops')
immediately following these places. A decomposition of a
subsection s of R is a collection of disjoint subsections s.
of R whose union is s. One place it in R is a predecessor place
of another place n' if the statement at it' can be the next
statement executed after execution of the statement at tt.
The entry places of a subsection s are all places in s having
predecessor places not in s; the exit places of a subsection s
are all places in s which are predecessors of places not in s.
A subsection s of R is said to terminate if for each of its
entry places it, the praa R obtained by modifying R in the
following manner terminates:

(i) Drop all statements in the main block of R which
do not belong to s; add a label L. at the place tf if necessary
and also add one statement, which will be the entry statement
of R^ , having the form 22 to L- . Also,

(ii) Add a stop statement with label L, to the end of R

1 TT

change every statement if_ C then 30 to L in s which references

-92-

a label L outside s to i£ C then g£ to L , and insert
the statement 2°. to L^ immediately after every statement
in s whose immediate successor statement is not in s.
We now give some termination proof rules:

(a) (Simple forward branch rule) Any praa subsection contain-
ing only forward branches and no selections 3 s from infinite sets
terminates .

(b) (Generalized forward branch rule) Let s be a subsec-
tion of the praa R, and let s-,...,s be a decomposition of s.

in

Suppose that s. terminates for each j = l,...,n, and that

whenever tt and t; ' are both places of s and tt is a predecessor

place of TT ' , then if tt belongs to s. and tt ' beloncs to s,

D ' k

with j 7^ k we have j < k. Then s terminates.

(c) (Backward branch rule) Let s be a terminating siib-
section of the praa R, let tt ,...tt, be all the entry places
of s, and let tt ',..., tt' be places which have predecessors in
s but which are not themselves in s. Suppose that for j =
l,...,n, the statement following the place tt . has the form
if C. then go to L . , where the label L. is at som.e place

of s that is physically prior to the place tt ! (so that the
if-statement represents a possible backward branch) .
Suppose that there exists a partially ordered set A in v/hich
indefinitely long ascending sequences of elements are impos-
sible, and an expression expn(vars) in the variables x^ , . . .x

of R, such that we have

I

[tt^jE uj (x =x|&. . .&x =x^) '^> \- (expn(x^, . . .x^) >expn(x^, x^^) )

for all entry places tt . of s and all exit places tt . ; where E is

the set of assumptions of R, '>' is the order relationship in the

partially ordered set A, and the x! are variables not otherwise

appearing. Let s' be the union of s and the statements

if C. then go to L . at the places tt ! . Then s' is a terminating

subsection of the praa R.

Rule (c) reflects the familiar observation, which goes

back as far as [Floyd, 67] , that termination proofs for a root

praa R will often proceed by mapping the data objects of R into some

appropriately devised partially ordered set. Note however that for

praa subsections s only involving loops of the 'do' type and their

-93-

set-theoretic equivalents, rules (a) , (b) , (c) normally yield easy
termination proofs, since in these cases A can simply be either
a finite range of integers in its natural order or the lattice of
subsets of a finite set, ordered by inclusion. The reader may be
interested in applying this remark to prove termination of the
counting-sort praa considered earlier.

Programs in our set-theoretic language proceed nondetermin-
istically, since the selection opreator x = aexpn makes a
nondeterministic choice. Thus 'termination' has two possible
senses, nair>ely finiteness of all possible computations (which is
the sense adopted in the last few pages) , and the existence of
at least one computation which reaches a given program point.

While a deterministic program, can only terminate by either
reaching its exit place or aborting, a program deliberately written
to exploit nondeterminism can terminate in two equally legitimate
senses, either by reaching some exit point and thereby succeeding,
or by failing along all paths and thereby certifying that the ccmbina-
torial problem which the program explores is unsolvable. Kence
reachability becomes a significant issue in the nondetermistic case,
i.e., to justify use of a program written in a manner deliberately
exploiting nondeterminism, termination in both senses must be proved.
To formalize this, suppose that we say that a place tt in a valid praa
P. is reachable if there exists at least one R-computation from the
entry place of R to tt . Equivalently we can say that tt is reachable
if R is valid but becomes invalid if the assertion I— {false) is
added to the assertion set of R.

To frove reachability, one can often proceed in the follow-
ing manner:

(i) First prove that R must terminate if tt is not reached
(i.e., that the praa R' obtained by adding M (false)'' to R terminates)

(ii) Next consider a computation c of maximal length in R',
and suppose the final state of c is at the place tt ' . We shall call
tt' a stopping place of R; clearly it' ^ tt .

(iii) Our aim now is to show that R can have no stopping
place tt'. To do this, we apply the following observations.

Civ" tt' can be a stopping place if some unsatisf iable
assumption ^ p"^ ' is present at tt ' . To avoid this possibility,
v.e shall suppose throughout the next few paragraphs that no

-94-

assumptions are present at any place other than the entry
place of R, (In effect, this means that all other assumptions
must have been reduced to assertions.)

(v) If tt", X = expn, then tt ' can only be a stopping
place if an operation error can arise in the evaluation of
expn (e.g. expn might contain the subexpression x/y , where
the value of y m.ight be zero) . Direct inspection of expn will
always reveal the types of operation errors possible in its
execution. If assertions ruling out these operation errors
are available at it ' , then tt ' cannot be a stopping place.

(vi) Similarly, if it', x =3 expn, and if assertions both
ruling out operation errors in the evaluation of expn and
ensuring that expn has a non-null value are available at tt',
then TT ' is not a stopping place. If tt', if^ C then go to L ,
and if assertions ruling out operation errors in the evaluation
of C are available at tt ' , then tt ' is not a stopping place. If
TT ' , X = f (expn, , . . . ,expn, ) , where f is a function of R, and
if assertions ruling out operation errors in the evaluation of
each of the argument expressions expn. are available at tt ' ,
then TT ' is not a stopping place.

(vii) Suppose that tt ' , return expn, and that assertions
ruling out operation errors in the evaluation of expn are
available at tt ' . Then tt ' can only be a stopping place if
there exists an assumption ^ P at the function f containing
the place tt ' which comes to be violated at the moment that
the return statement is executed. This possibility is ruled
out if we assume that R contains no assumptions-at-functions
(which is to say that all such assumptions have been converted
to assertions) .

Programs which deliberately exploit nondeterminism will
generally contain fail statements; the semantic effect of such
a statement is simply to terminate any computation which
reaches it. (In our restricted formalism, such a statement
could be represented as a deliberate error, e.g. x = 1/0.)
TO prove reachability using the termination-based technique

-95-

just outlined, it is necessary to prove that such fail
statements (or the erroneous statements used to represent them)
are avoided (or more precisely, can be avoided) . Arguments
useful for this purpose can be based on the folloving notions.
Suppose that R, is a correct praa. Then R is a generalizaticn
of R- if R is obtained from. R^ by replacing certain of the
assignments x = 3 expn (resp. x = expn) in R by arguments x=9expn'
(resp. x=expn) and by dropping some of the assertions of P., ,
provided that an assertion | — (expn £ expn') (resp.
I — (expn G expn') ') is available in R, at each point tt^
where such a replacement is made. It is clear that if R is
a generalization of R, and it is reachable in R, , then tt is
reachable in R. (Note however that the correctness of R
does not follow from that of R^ , but must be proved separately.)

As an illustration of this we consider the following
nondeterministic praa which solves the well-known 'eight queens'
problem (placing 8 queens on a chessboard so that no queen
attacks any other) . We develop the solution as a vector posns
whose j-th component shows the position of the j-th queen.
The praa is :

(19) rows = { n I l<_n<_8 } ; posns = n£^; n = 1;

while n<_8; (= vector (posns) & range (posns) C rows

& (l<_Vi,j<n| ij^j) (posns (i) -posns (j) ) ^{ 0 , i- j , j-i} )
posns (n) = 3 (rows-{posns (k) +tilt* (n-k) , l<_k<n,

tilt e {0,+l,-l}}) ;
n = n+1;
end while;
I — vector (posns) & range (posns) c rows

S domain (posns) = (n, l<_n<_8}
& (1<_ Vi,j _< 8| ij^j) ( (posns (i) -posns (j) ) ^{0 ,i- j , j-i} )

That this praa is correct is easily verified using the
temporary assumption shown, and the termination-proof techniques
described earlier make it obvious that the praa terminates .

-96-

What we wish to show is that, if we assume that the eight-
queens problem has a solution, then the end of the praa (19)
is reachable. To do this, we make use of the following
modified praa, of which (19) is (essentially) a generalization.

(20) soln = u where range (u) c {n, 1 <_ n <_ 8}

& domain (u) = {n, 1 <^ n <_ 8}
& (1 < Vi,j <_ Sjij^j) ((u(i)-u(j)) ^ {0,i-j,j-i})
rows = {n I l<_n<_8}; posns = n^; n = 1;
while n <_ 8; \= posns = soln(l:n-l)

[— soln(n)£(rows-{posns (k) + tilt * (n-k) ,

l<^k<n, tilt e {0,1,-1}})
posns (n) = soln(n);
n = n+1;
end while;

Now since we assume that the eight-queens problem, has a solution,
the first statement of (2 0) is not a stopping place, and thus
(20) possesses no stopping place. It is equally clear that
(20) terminates; thus the end of (20) is reachable. But by
virtue of the assertions following the while statement in (20) ,

(20) clearly has the following generalization:

(21) soln = u where range (u) c {n, l£n;^8} & domain (u) ={n,l<_r.<_8}

& (l<Vi,j<8|i?^j) ((u(i)-u(j) ) ^ {0,i-j,j-i});
rows = {n|l<_n£8}; posns = ni_; n = 1;
while n £ 8;

posns (n) = 9(rows-{posns (k)+tilt* (n-k) ,l£k<n,

tilt e {0,1,-1}});
n = n+1;

• end while;

-97-

Hence the end of (21) is reachable. But in (21) the variable
scln is dead. Since deletion of an assignment to a dead
variable clearly does not spoil reachability, it follows
immediately that the end of (19) is reachable.

We conclude the present section with a discussion of
the question of the reachability properties of the praa trans-
formations listed in Section (2.c). We have already noted that
IT is reachable in R if R is valid but becomes invalid if the
assertion | — {false) is added to R. This makes it plain
that all of the reversible transformation rules listed in Section (2.c)
preserve reachability. This includes Rules (l.a), (l.d), (l.f),

(l.g), (2.a-f), (2.k-i) provided that the place tt to be reached
is not one of those directly involved in the transformation
applied, and with the same restriction also (2.m.), {2.n), (2.o),

(3. a), (3.c-e), (4.a-c). The remaining rules require additional
comment:

Ad (l.b) and (l.c): If e, c e_ is known at a place 7t_
in the praa R, then 7t_ , x = 3e_ , tt can be replaced by
IT , X = 3e, , IT preserving reachability of tt , provided that

~ 1 + TT4_

addition of the assumption ^ (x G e„- e, ) makes it possible
to deduce the assertion | — {false) . Similarly, if e, e e^
is known at tt_ , then to replace x = 3e_ by x = e, we must

TT TT

be able to show that ^ (x e e - {e }) "*" leads to | — {false) .

Ad (l.e) : To give adequate form to this rule, we need to

introduce an extended notion of reachability. Let R, be a valid

praa with variables x-,...,x„, let n < m < £, let P be a

predicate with free variables x ,...,x , and let C be a

predicate with free variables u,,..,,u ,Xt,...,x . Let tt be
^ ]. n 1 m

a place in R, . Then we say that the triple (TT,C,n) is P-reach-

able if, for all Uw.-./U , x',.../xV satisfying

P(x|,...,x') & C(u,,...,u ,x|,...,x'), there exists an R -computation

c terminating at tt in whose initial state the variables x, , . . . ,x

have the values x,',...,x and in whose final state the

1 m

variables x, , . . . ,x have the values u, , . . . ,u .

-98-

Now let R, R , B_-'' , L . , j = 1, . . . ,k be as in

transformation rule (l.e), let B'-^ be the place in R^

immediately following the label L. , and let C. be as in

D 3

formula (8) of Rule (l.e). Suppose that the assum.ptions

made in connection with Rule (l.e) are all satisfied, and

suppose also that at each of the places B_ , j = l,...,k

in R a proposition P. v/ith free variables x^ , . . . ,y.

3 (i) 1' ' IT.

IS available, such that the triple (3 ' ,C . ,n) is

P .-reachable. Then rule (l.e) can be applied, with preser-
vation of reachability.

To prove that a triple (TT,C,n) is P-reachable, we can
generally proceed as follows. Let R be the praa containing tt .

Introduce variables Xt,...,x', u,',...,u not otherwise

1 m. 1 n

occurring, and add the assumption

^ (P(x|, . . . ,x^) & C(u|, . . . ,Uj!^, x|,...,Xjj^) &

(x,'= X, & . . . & x' = X ))

1 i mm

to the entry place tTq of R, thus obtaining a new praa R'.

Find a correct praa R" of which R' is a generalization, and

which is such that the assertion I — (x, =u, &...&X =u)

'11 n n

can be proved in R" .

A less elaborate discussion suffices to dispose of the
remaining transformation rules.

Ad (2.g): Let C, be as in Rule (2.g). Then Rule (2.g)
can be applied, with preservation of reachability, provided
that at the place it immediately preceding the go-to statement
to be split there are available assertions implying the
impossibility of operation errors in the evaluation of the
boolean expression C-^ .

Ad (2.j): As in Rule (2.j), let s^ and s be isomorphic
sections of a praa R. Then Rule (2.j) can be applied, with
preservation of reachability, provided that the place tt to
be reached does not belong to the code section s,.

-99-

Ad {2.k): As in rule (2.k), let s be an isolated
section of a praa R. Then rule {2.k) can be applied, with
preservation of reachability, provided that if any statement
if C then go to L of s is modified, the place it to be reached
does not belong to the code section s.

Ad {2.£): Let the label L be as in rule {2.i). Then
rule {2.Z) can be applied, with preservation of reachability,
provided that the place tt to be reached is not the place
immediately following the label L.

Ad (3.b): Reachability is preserved by insertion of
assignment statement x = expn whose target variable is dead,
provided that at the point of insertion assertions implying the
impossibility of operation errors in the evaluation of expn are
available. Similarly, reachability preserved by insertion of a
selection statement x = 3sxpn whose target variable is dead, pro-
vided that at the point of insertion assertions implying the
impossibility of operation errors in the evaluation of expn,
and also implying that expn cannot be null, are available.

Ad (4.d): As in rule (4.d), let f and f be two
isomorphic functions. Then provided that the place tt to be
reached is not a call to f, rule (4.d) can be applied, with
preservation of reachability.

Ad (4.e): As in rule (4.e), let f be an n-parameter
function of the praa R, let tt ' be a place in R, and suppose
that f allows entry. Let R, be obtained from R as follows:

The functions of R, are the functions of R, but the main
block of R, is the body of the function f, with all label and
variable names changed to new names, and with each return
statement replaced by a statement go to L, where L is a label
not otherwise occurring. Let tt be the place following L.

Suppose that P is a predicate whose free variables are
the variables of R, which correspond to the parameters of f,
and suppose also that the triple (TT,P,n) is P-reachable in the
sense of the discussion concerning (l.e) found a few paragraphs
above. Let expn. be the argument expressions of a function

-100-

call which is to be inserted at tt ' . Suppose that at the place
ir ' there are available assertions implying the impossibility
of operation errors in the evaluation of any of these expres-
sions, and also assertions implying the proposition
P (expn, , . . . ,expn ). Then reachability is preserved even if
we insert a function call x = f (expn^ . . . ,expn ) at tt ' , provided
that the target variable x of the call has no other occurrences
in R.

-101-

Appendix . Proof rules for other semantic features.

A variety of useful syntactic and semantic features,
including label and function variables, procedures able to
modify their parameters, procedure variables, and nondetermin-
ism, are available in languages like the one which we have
been considering, and it is therefore appropriate to state proof
rules which cover these features.

a. Label Variables. If we enumerate the labels

Lw • • . ,L occurring in a praa R, we can treat label variables

simply as integers. If the labels recurring in a particular

function f of R (or in the main block M of R) are L.,...,L. ,

1 j

then each statement 22. ^ ^ occurring in f (or M) can be
treated as if it read

if X = i then go to L. else if x=i+l then go to L.^, else if
... else if x=j then 2°. to L. else error;

where the error statement terminates execution.

b. Function Variables. We can treat function variables
in a very similar way. If we enumerate the functions f^.-./f-^
occurring in a praa R, and let the number of parameters of f .
t>e p(j>,then function variables can be treated simply as
integers. A call x = y (expn, , . . . ,expn ) to a function variable
y can simply be regarded as an abbreviation for the conditional
code sequence

if p(y) = m then go to L2;
Ll: go to Ll /* a 'stop* statement */

L2: if_ Y = 1 then

X = f , (expn, , . . . ,expn ) ;
else if n = 2 then

X = f (expn, , . . . ,expn^)
else if . . .

-102-

else if y = n then

X = f^(expn^, . . . ,expnj^)
end if;

Of course, all functions f, for which p(j) ^ m can and should
be omitted from the compound if-statement following label L2.

c. Modifiable Arguments, Procedures, and Procedure Variables
Provided that parameters are passed by value with return
of values at the moment of procedure return, the procedure call

p(x^, . . . ,x^) ;

can be represented by the equivalent code sequence

t = f (x^, ,x^)

x,= t (1) ; . . . , x^ = t (n) ;

where the function f is obtained from the procedure p as follows:
i. For j = l,...,n, replace every occurrence of the

(modifiable) parameter y. of p by an occurrence of a new

variable y! not otherwise occurring;

ii. Insert the group of assignments y^ = y^, . . . ,Y^ - y^

at the entry place of p;

iii. Replace every simple return statement in p by the

statement return <y-. / • . • /Y ' > •

If this transformation is used, then procedure variables
can be handled by the function-variable technique sketched in
paragraph b.

Other common styles of parameter-passing, e.g., parameters
passed by reference, are less readily dealt with. In the worst
case, treatment of a feature of this kind may force much of the
mechanism of its intended implementation to be made explicit by
introduction of a comprehensive mapping of pointers into values.

-103-

If this is necessary, application of the proof formalism
developed in the preceding pages will become much cltimsier.
However, it will still be possible to use auxiliary proof
rules which establish the semantic equivalence of value and
pointer semantics in particular cases to prove the correctness
of many algorithms written in a language which makes use
either of call-by-reference or other, still more general,
pointer mechanisms.

d. Nondeterminism . As already noted, the set-theoretic
selection operator bs acts nondeterministically . This operator
can be used to represent other semantic mechanisms used to
introduce nondeterminism into programming languages . For
example, a binary primitive function ok which is nondeterminis-
tically either true or false can be written simply as

3 {true , false] . Hence, if we ignore the issue of termination,
the proof and transformation rules set forth above cover
deterministic and nondeterministic programs indifferently.
However, as indicated in Section 4, the question of termination
must be approached in a rather different way for nondeterministic
than for deterministic programs.

e. Existential Operator. A powerful and broadly useful
programming construct is the existential operator

(1) t = 3xt, ,x^ I C(x, , ,x^) ,

1 n ' 1 n

which both checks for the existence of values x, ,...,x

satisfying the condition C and which assigns x,',...,x'

to the variables x, ,...,x if x-,...,x' can be found.

1 n 1 n

This operator has two useful properties:

(a) It can be expanded, in an obvious way, into a
'search* loop; and

(b) Immediately after (1) , the assertion

-104-

(2) f- (t =* C(Xj^,...,x^)) & nt => (Vx^,...,x^) nc(x^,...,x ))

is available.

The corresponding numerical iterator

(3) t = m < 3k < n I C{k)

can be expanded into a loop which searches in increasing order;
iTioreover, immediately after (3) , the assertion

(4) 1— (t => C(k) & (m < Vj < k) nc(j)) & (Ht => (m <_ Vj <_ n)nc(j))

is available.

A third useful property of the existential (3) is that it
can be replaced by t = m, £ 3 k <_ n, |C(k), provided that

(5) |— m <_ m, <_ n & m<_n,<_n & ( (m£Vk<m^) nc(k)) &

( (n^ < Vk < n) "lC(k) )

is available at the place preceding (3) . (Of course, (1) can
also be transformed in similar fashion.)

The simple 'bubble sort' illustrates the use of this
broadly useful rule. If we write the bubble sort praa as

(6) ^^ vector (v) & range (v) c reals & v = v'
while 1 £3k < #vlv(k) > v(k+l);

[— 1 £ Vj < k I n(v(j) > v(j+l))
swap(v(k) ,v(k+l) ) ; |— rangecount (v) = rangecout(v')
j— 1 < Vj < k-l|n(v(j) > v(j+l))
end while;
|— l<Vk<#v|v(j) < v(j+l) & rangecount (v) = rangecount (v' )

its correctness is obvious. But then the transformation rule
for existentials that has been stated allows us to rewrite the
body of (6) as

-105-

(7) kk = 1;

while kk < 3k < #v I v(k) > v(k+l) ;

swap(v(k), v(k+l));

kk = max(k-l,l); [— 1 < kk < #v
end while;

Then, if the existential operator is rewritten as a search
loop we get

(8) kk = 1;

Loop: k = kk;
Sloop: if v{k) > v(k+l) then go to Lswap;
k = k+1;

if k >^ #v then go to Lout;
go to Sloop;
Lswap: swap(v(k), v(k+l));

kk = i£ k = 1 then 1 else k-1;
go to Loop;
Lout:

Since the variables k and kk are never alive at the same time,
they can be identified, which makes it easy to transform (8)
into

(9) k = 1;

Loop: _if v(k) > v(k+l) then
swap(v(k) , v(k+l));
k = if k = 1 then 1 else k-1; t" 1 1 ^ < #v

else

k = k+1;

if k >_ #v then go to Lout;
end if;

go to Loop;

Lout;

-106-

which can in turn be converted into the standard form of the
bubble sort.

It should be noted that other set-theoretic constructs
which expand into stereotyped code sequences and which make
available assertions of predictable form can be exploited in
similar fashion. This remark applies to 'generator' routines
which generate all the elements of some large set one after
another, and also to codes which develop solutions to equations
of various useful standard forms.

-107-

Bibliography

Burstall, R. and Darlington, J. [1975] Some Transformations
for Developing Reaursive programs . Proc. of 1975
International Conference on Reliable Software,
pp. 465-472.

Cohen, P. [1966] Set Theory and the Continuum Hypothesis .
Mathematics Lecture Note Series, W. A. Benjamin Publ.
Co. , New York.

Floyd, R. [1967] Assigning Meanings to Programs . Proc.
Symp. Appl. Math., American Math. Society, v. 19.

Gerhart, S. [1975a] Correctness-Preserving Program Trans-
formations. Symposium on Principles of Programming
Languages, pp. 54-66. Also available as Tech. Rep.
CS-1975-4, Computer Sci. Dept., Duke Univ., Durham,
N.C.

[1975b] Knowledge abouy Programs : A Model and Case
Study. Tech. Rep. CS-1975-1, Comp. Sci. Dept.,
Duke Univ. , Durham, N.C.

[1976] Proof Theory of Partial Correctness Verifi-
cation Systems. Tech. Rep. CS-1976-5, Comp. Sci.
Dept., Duke Univ., Durham, N.C.

Hoare, A. [1969] An Axiomatic Basis for Computer Program-
ming. Comm. ACM, v. 12, pp. 576-580.
[1971] Procedures and Parameters : An Axiomatic
Approach. Symposiiim on the Semantics of Algorithmic
Languages (ed. Engeler, E.). Springer Lecture Notes
on Mathematics No. 188, pp. 102-116, Springer-Verlag,
Germany.

[1972] Proof of Correctness of Data Representations .
Acta Informatica, v. 1, pp. 271-280.

London, R. [1 70] Bibliography on Proving the Correctness
of Computer Programs. Machine Intelligence 5 (eds.
Meltzer, B. & Michie, D. ) pp. 569-580. American
Elsevier Publ. Co., N.Y.

-108-

[1972] The Current State of Proving Programs Correct .

Proc. ACM Annual Conf. 1972, pp. 39-46.
Misra, J. [1975] Relations Uniformly Conserved by a Loop.

IRIA Conference on Proving and Improving Programs,

pp. 71-80. Arc et Senans, France.
Morris, J. H., and Wegbreit, B. [1976] Subgoal Induction.

Tech. Rept. , Xerox Palo Alto Research Cr . , Palo Alto,Cal,
Sites, R. [1974] Proving that Computer Programs Terminate

Cleanly. Ph.D. Thesis, Stanford Univ.; also Comp.

Sci. Rept. STAN-CS-74-418.
Walker, S. and Strong, H. R. Jr. [1972] Characterization

of Flohiahartable Recursions. IBM Res. Rep. RC-3844.

T. J. Watson Res. Lab., Yorktown Heights, New York.
Wegbreit, B. [1974] The Synthesis of Loop Predicates .

Comm. ACM v. 17, pp. 102-112.

[1976] Verification of Program Performance .

Tech. Rept., Xerox Palo Alto Research Center, Palo

Alto, Calif.

-109-

Appendix . Derivation of a related group of searching praas .

(by Edith Deak)

The follov/ing example illustrates the derivation of
several functionally related algorithms from a common root praa
usint, echniques discussed in Sections 1 and 2. All of the
praas presented search for an element R in a sorted array A,
and realize the output assertion:

|— found = (1 < 3k ^ h) i=k & A(k) = R

We first present a general, high level root praa and then show
how three more specific algorithms can be derived from it by
applying correctness-preserving transformations. The success
of this method depends on the nonprocedural nature of the where
diction and the block substitution rule.

A. Root praa for searching a sorted array.

^ A e vector (reals) & #A = n & Real (R) & sorted (A) & n>0

Ti^ found = false ;

TT2 £ = 1;

1T_ u = n;

ir LI: 1— (1 < Vj < ?.) A(j)<R & (u < Vj j^ n) A(j) > R

IT- if^ u < £ 2^ t^ ^3'

7r_ i = j where 2. < j < u;

o — —

TT_ if A(i) = R go to L2;

TTg if A(i) > R then

■"■g u = i - 1;

TT else

TT 2. = i + 1;

IT end if;

TT^ - go to LI ;

IT L2: I— (1 < 3k < n) i = k & A(k) = R

TT found = true',

TT L3: [— found ^ (1 < 3k £ n) i = k & A(k) = R

-110-

Several search algorithms can be obtained by specifying
how i at IT is to be selected.

B. Sequential search praa .

To derive a sequential search, we make an obvious choice,

setting i = i, and perform the following transformations of

the root praa. (Justification is given for each transformation,

all of which are either rules mentioned in Section 2 or standard

optimization techniques.)

(i) Replace tt^ by i = £; (block substitution rule)

6

(ii) Move •"■_ to the end of all predecessor blocks
5

(all predecessors are

single exit)
(iii) Replace uses of u and i by n and £ respectively

(equality substitution)

The resulting praa is:

-111-

^ A G vector (reals) & #A = n & Real (R) & sorted (A) & n > 0

TT found = false;

^ ^ - 1;

TT^ u = n;

TT if n < i go jto L3;

TT^ LI;

TT i = £;

D

TT if A(g-) = R go to L2;

IT if A(e) > R then
o

TT u = £-1;

TT if £-1 < I go to L3;

TT else

TT J^ u < £ go jto L3;

TT . end if ;

TT ^o jto LI ;

TT found = true ;
^18

L3: I- found e (1 < 3k < n) i = k & A(k) = R

TT- then becomes a go to statement, which makes u at tt
dead. Then u at tt is equal to n, and so tt becomes dead.
We have now :

-112-

^ A 6 vector (reals) & #A = n & Real (R) & sorted (A) & n > 0

ir. found = false;

7T2 £ = 1;

TT- if n < g- go to 13;

■n . Ll:
4

TTg i = £;

TTg if A(g-) = R go to L3 ;

IT- if A(£) > R go to L3 ;

ir. I = il+l;

tTq if n < g. go to L3 ;

IT, - 30 to Ll ;

^1 ^2:

IT „ found = true;

IT L3: [- found = (1 < 3k < n) i = k A A(k) = R

Then, to eliminate i, note that

+

""13
K [ (1 1 3k < n) i = k & A(k) = R =» i = £]

+

^13
\— [found = (1 < 3k < n) £ = k & A(k) = R]

C. Binary search praa

A binary search procedure is obtained immediately by
using the block substitution rule to replace tt by the
statement:

i = la + u)/2j ;

D. Fibonaccian search praa

We now derive the Fibonaccian search procedure described
in Knuth, Vol.3, p. 415, from our original root praa.
We refer the reader to the Fibonacci tree shown by Knuth on p. 415
as an aid to understanding what follows. The algorithm computes
the next value of i without any multiplication or subsequent divisor,

-113-

Values of i are nodes in the Fibonacci tree, obtained by
adding or subtracting successively smaller Fibonacci numbers.
The algorithm uses two auxiliary variables q and p, which are
always consecutive Fibonacci numbers satisfying q < p.
As in Knuth ' s first version of the algorithm, we make the
additional assumption that n+1 is a Fibonacci number. If we
assume i as the root of the current subtree in the Fibonacci tree
being searched, l-l indexes the left most leaf of that subtree,
and u indexes the rightmost leaf of the subtree. It is interesting
to note that while the final algorithm uses p and q and not 9, and u,
our root praa is a natural path to derivation of the Fibonaccian
search praa. The proof of the Fibonaccian algorithm is
facilitated by putting it in this framework.

We are going to assume that our verification system has
been supplied with information concerning some basic mathematical
properties of Fibonacci numbers. Let the function fib(k) specify
the k-th Fibonacci number, so that fib(O) = 0, fib(l) = 1,
fib(2) = 1, etc. Variables i, p, and q are initialized
as follows:

i = fib(k) where n+1 = fib(k+l);

p = fib(k-l) where i = fib(k) ;

q = fib(k-2) where i = fib(k);

If A(i) < R, the algorithm moves i down the left branch of the
tree, which is done by executing the code:

i = i - q;
q = p - q;
p = p - q;

If A(i) > q, i moves down the right branch, by executing the code

i = i + q;
P = P - q;
q = q - p;

-114-

We embed these two code fragments in two fragmentary Fibonacci
praas , both of which can be seen to preserve the following
proposition P under appropriate conditions on p and q:

(3k) p = fib(k) & q = fib(k-l) & i+p = u+1 & 2,+q+p = i+1

Fib praa 1:

^ P & q > 0
u = i-1;

i = i-q;

q = p-q;

p = p-q;

1- p

Fib praa 2:

^ P & p > 1
£ = i+1;
i = i+q;

p = p-q;
q = q-p;
hP

The invariance of P can easily be verified by calculating strongest
postconditions and then performing appropriate algebraic manipulations

These two Fibonacci praas embody most of the information
concerning the fih function that we require.

Returning now to the root praa, the first step of our
derivation is to move statements tt^ and it backwards to all
predecessor blocks, as was done in section A. This gives

-115-

^ A e vector (reals) & #A = n & Real(R) & Sorted (A) & n > 0

\

found = false;

^2

V

I = 1;

"3

u = n;

\

if u < S, go to L3;

^

i = j where Ji < j < u;

\

LI:

^

if A(i) = R go to L2;

"8

if A(i) < R then

\

u = i-1;

\o

if u < J. go to L3;

\l

i = j where Jl < j < u;

\2

else

\3

£ = i+1;

\4

if u < £ go to L3;

\5

i = j where £ < i < u;

\e

end if;

\7

go to LI;

\b

L2:

\9

found = true ;

^20

L3:

— found = (l<^3k<n) i =

We then observe that proposition P => £ < i <^ u.
The Fibonacci search praas given above can therefore be
substituted for the where statements in our search praa,
using the block substitution rule.

The next version of the search praa is obtained by the
following sequence of transformations:

(i) strengthen initial assumption, adding (3k > 2) n+1 = fib(k)

(ii) replace initialization of i at tt (block substitution)

(iii) initialize p and q (shadow variable)

(iv) replace use of u at tt by i-1 (equality substitution)

(v) replace it,, by fib praa 1 (code block substitution)

(vi) delete "n^ (dead code elimination)

(vii) replace use of £ at tt . by i+1 (equality substitution)
(viii) replace tt^ ^Y fib praa 2 (code block substitution)

(ix) delete tt,^ (dead code elimination)

-116-

The result is:
^ A e vector (reals) & #A=n & real(R) & sorted (A) & (3k>2) k+1 = fib(k)

IT found = false ;

IT u = n ;

7T if u < £ go to L3;

7T^ i = fib(k) where k+1 = fib (k+1);

TT^ p = fib(k-l) where i = fib(k);

TT q = fib(k-2) where i = fib(k);

TTg LI:

TT_ if A(i) = R go to_ L2 ;

■"10 if_ A(i) < R then

7T _if i-1 < 2. ^ to L3;

}= P S q > 0

^2 ^ = ^-^'

^13 i = i-q;

TT^4 q = p-q;

TT-L5 p = p-q;

TT^ ^ else

IT if u < i+1 go to S-3;

j= P & p > 1

TT^g ii = i+1;

^^g i = i+q;

^20 P = P"^'

1^21 q = q-p;

iT_„ end if ;
IT go to LI;

^24 ^2:

TT- found = true;

^26

L3: I— found = (1 < 3k < n) i = k & A(k) = R

-117-

P is loop invariant, and therefore the assumptions
1^ P at IT and tt can be degraded to assertions.

Next, we want to eliminate I and u from the program.
First observe that

i-1 < £ H i £ £ E q+p-1 <_ 0 since ?.+q+p = i + 1.

Since q and p are consecutive Fibonacci numbers, this can only
occur when q = 0. Therefore i-1 < I = q £ 0. Similarly,
u < i+1 Eu^i Ep£l since i+p = u+1 . This justifies
the following sequence of transformations:

(i) replace it by if q ^ 0 go to L3; (equivalence substitution)

+

^11
(ii) degrade f= (q >0) to an assertion

(iii) replace tt^ _ by if_ p £ 1 go to £3; (equivalence substitution)

+

■^17
(iv) degrade t^ (p > j) to an assertion

(v) replace it. by dJE n < 1 go to £3; (equality substitution)

(vi) delete it. since n < 1 is false

(vii) delete tt„, tt, , tt,„, tt _ (shadow variable rule)

The resulting program, shown just below, is a correct Fibonacci
search praa:

.118-

^ A e vector (reals) & #A=n & real (R) & sorted (A) & (3k>2) n+l=fib(k)

found = false ;

i = fib(k) where n+1 = fib(k+l);
p = fib(k-l) where i = fib(k);
q = fib(k-2) where i = fib(k);

Ll: if A(i) = R go to L2;
if A(i) < R then

if q < 0 go to L3 ;

i = i-q;

q = p-q;
p = p-q;

else

if p < 1 go to L3;
i = i+q;

p = p-q;
q = q-p;

end if ;

L2

L3

go to Ll ;
found = true;
|— found E (1 < 3k < n) i = k & A(k) = R

-119-

METAMATHEMATICAL EXTENSIBILITY FOR THEOREM VERIFIERS

AND PROOF-CHECKERS

Martin Davis and Jack Schwartz

A full-blown program verification technology must rest on
more than the informal or semiformal type of reasoning customary
in ordinary published m.athematics , since reasoning of this type
does not prevent numerous small errors from intruding into proofs,
For this reason, any fully satisfactory program verification
technology will have to make use of proofs which are expressed
in computer readable form and which are then certified formally
by a programmed proof-checker or theorem prover. The proof -
checker system used will then play the role of a fundamental
verification yardstick, and must therefore meet very stringent
(albeit only manual) standards of verification. On the other
hand, a central aim of verification technology is to reduce
the cost of program verification drastically, and thus use of
a single inextensible verification formalism will be self-
defeating. It is therefore interesting to note that in ordinary
mathematical practice, expressions of proofs are greatly facili-
tated by the availability of metamathematical extension mechan-
isms. A familiar example of this kind of metamathematical exten-
sion justifies the ordinary habit of using a predicate-calculus
statement of the associative and distributive laws to set up
an algebraic formalism and then of accepting algebraic calcu-
lations in lieu of detailed predicate calculus proofs.

These considerations show that in establishing a verifica-
tion mechanism suitable for long-term reliable use, we will
need to define a system having the following three properties:

(A) SOUNDNESS. The system must be capable of verifying
the correctness of mathematical proofs, and of maintaining a
library of theorems for which correct proofs have already been
supplied. We must be entirely convinced that any proof of a
theorem which the system certifies as correct should indeed

be so,

(B) EXTENSIBILITY. It should be possible to augment the
system by adding new symbols, schemes of notation, and extended
rules of inference of various kinds (e.g. rules allowing proof

120

by algebraic or other formal cornputation to be incorporated into
what is originally a system containing predicate calculus state-
ments of the commutative, associative, and distributive laws.)

(C) STABILITY. The changes to the system envisioned in (B)
must not alter the soundness demanded in (A) .

It is clear that stability is crucial to the long-term
success of verification systems. Uncontrolled insertion of
unverified, even if plausible, new proof methods can be entirely
fatal to the usability of such a. system. A verification system
guards against the possibility of an incorrect statement entering
into its library of verified statements by refusing to admit a
statement into this library unless a proof of it has been
accepted by the system. In order to use a similar technique to
guard against the introduction of unsound proof methods, it is
necessary to fully formalize our metamathematics . Then, for each
proposed new method of proof, we can form a 'justifying sentence'
which asserts that anything which can be proved using the new
method was already provable before its introduction. The system
will then accept a new proof method only if it succe ds in check-
ing a proof (supplied to the system) of this justifying sentence.

In this paper, we will present a logical prototype of such
a system; will then describe the way in which it could accept
general notational extensions of its initial proof formalism;
will touch upon some of the logical issues v;hich arise in connec-
tion with the 'computerization' of such systems; and will
analyze some of the metamathematical questions raised by the
method used to achieve extensibility.

In our initial analysis, we shall deliberately impose very
drastic restrictions on the programming environment which supports
the extensible proof checker systems we consider, so as to post-
pone certain technical considerations which would otherwise have
to be faced immediately. However, in a final section, we will
extend our initial analysis by considering the issues which
need to be faced in order to extend our initial rudimentary pro-
gramming environment to one in which more adequate computing
mechanisms, programs, and programming languages can be used.

-121-

2. A Formal System (FS)

We work with a formal system (or theory) FS which is suitable
for the formalization of substantial portions of ordinary mathe-
matics. -(To simplify our exposition, a powerful but rather
minimal formal system will be used.) Without attempting to
specify FS completely, we assume:

(a) FS contains the usual predicate logic (i.e., the first
order predicate calculus) . The expressions (terms and formulas )
of FS are character strings on a finite alphabet consisting of
alpha-numeric characters ordinarily available in computer systems,
and have a convenient syntax of the kind ordinarily used in
programming languages. (Of course this implies that the variables
of FS are represented by character-string names rather than
separate symbols.)

(b) There is a term of FS , which we write 0, whose intended
interpretation is the empty set; for each pair of terms a,B of
FS , there are formulae a e B , a = B, and terms {a,B}, a-B,

a u B, and P(a) (this last designating the 'power set' or set
of all subsets of a) . Within FS there exist axioms implying
that these formulas and terms have all their ordinary set-theoretic
properties. We write {a} ={a,a}. Following von Neumann, we
recursively identify each nonnegative integer with the set of
all nonnegative integers preceding it, i.e. 0=0, n+1 = n u {n}.
Thus each nonnegative integer is identified with a term of FS .
(This identification plays no essential role in which follows, but
does simplify our exposition.) Also there is a term w of FS
whose intended interpretation is the set of nonnegative iricegers,
such that for each nonnegative integer the formula n £ w is
provable in FS.

(c) We write <a,B> = {{a},{a,B}}, thus using the Wiener-

Kuratowski definition of ordered pair. Proceeding recursively,

we set <a> = a, <a,,...,a > = <a,,<a_,...,a >>. We also write

1 n 12 n

[a,,...,a ] = <n,a,,...,a > = <n,<aT,...,a >>. This latter
1 n 1 n 1 n

"n-tuple" has the virtue that its length is unambiguously
determined. We assume that for each term a of FS , there is a
term Len(a) such that the equation Len(a) = n is provable in FS

* Formulas are sometimes called w.f.f.'s.

-122-

for some nonnegative integer n, and such that whenever the equation
a = [a ,.,.,a ] is provable in FS , so is the equation Len(a) = n.

(d) For each pair a , B of terms there is a term a| JB. When
the equations a = [a ,...,a ], B = [B-,,...,!3 ] are provable

in FS , so is the equation a||B = [a,,..,a ,^ , . . . ,Q ].

(e) For each pair of terms a,B there is a term a(B) .

Whe ever the equations a = [a^ ,...,a ] and B = ni with 1 < m < n

in — —

are provable in FS, so is the equation a(B) = a .

(f) For each pair of terms a,B, there is a term ajB such
that whenever the equation B = m > 1 is provable in FS, so is
the equation

a|B = [a (1) ,a (2) , . . . ,a (m) ] .

By (e) , this implies that if the equation a = [a,,..., a 1 is

provable in FS with m <^ n , then so is the equation

a|B = [a,,a^,...,a ].
'12m

(g) For each pair of terms a,B there is a term a + B. When
the equations a = m, B = n are provable in FS , so is the equation
a + B = k where k is the ordinary integer sum of m and n,

(h) For each term a of FS, there are terms R(a), Lev(a).
The sentences R(0) = 0, (Vn)(n e to ^ R(n+1) = P(R(n))) and
( Vx) (Vy) (Lev(x) £ y -^ x e R(y)) will all be provable in FS .
Intuitively the elements of R(n), for n a nonnegative integer,
are those which can be built up in at most n stages beginning
with 0, where at each stage one is permitted to form any
(necessarily finite) set using the elements produced at
an earlier stage.

(i) If the formulas (}) (1) , <}) (2) , . . . ,4) (n-1) are all provable
in FS, then so is the formula

Now we specify a subsystem LFS of FS within which all
sentences (i.e. formulae without free variables) will be routinely
decidable by a finite procedure. The terms of LFS are the
smallest class T of terms of FS containing the term 0 and the
variables of FS which is, such that whenever a,B are in T, so
are {a,B}, (a u B) , P(a), Len(a), (a||B), a(B), (a|B), (a+B) ,
R(a), and Lev(a) . The formulae of LFS are the smallest class F of

-123-

of formulae of FS containing all formulae (a = B) and (a e 6)
where a and B are terms of LPS, and which is such that:

(i) whenever (p and 6 are in F so are '^"f , {'t> & 6), (^ V 6),
((j) -> 6) , and (cf) *> 6) .

(ii) whenever (J) is in F , X is a variable of FS and a is a
term of LFS not containing X, then (3X) (X ^ a ->■ $) and
(3X) (X G a & 4)) are in F.

We speak of terms containing no variables as constant terms.
It is clear that the constant terms of LFS (often simply called
constants ) denote finite data objects. Using this fact we can
describe a systematic algorithm which applied to any sentence
0 of LFS returns one of the truth values true or false . This
algorithm can be described recursively in terms of the total
number of occurrences of the symbols "x^ & V -»■ -^ V
in $ . If this number is 0 , * must have the form (a ^ 6) or (a = B)
v/here a,B are constants; and hence $ can be tested in a finite
number of steps. If this number is greater than 0 and '? has one
of the forms '^^4),4)&6,c})V6,(t)->-6 or (i> ** & , the truth value
of "f can be computed as a Boolean combination of the truth values
of <p and 6. Finally if '^ has one of the forms

(VX) (X e a -^ c{)(X) ) or (3X) (X e a & <}) (X) )

the truth value of $ can be computed from a finite number of
truth values of sentences cf) (a, ) , . . , (j) (a ).

VJe assume that FS is sufficiently powerful to permit formali-
zation of the finite computations needed to obtain the truth
values of sentences of LFS, i.e. that for every such sentence $
for which the computed value is true, $ is provable in FS .
Or, as we may say, we assume that FS is complete with respect
to sentences of LFS. It is a routine exercise to verify that
any of the usual ways of specifying FS satisfy this complete-
ness condition.

It follows from this completeness condition that for every
constant a, the sentence a e R(n) is provable in FS for some
nonnegative integer n (indeed for all sufficiently large n) .

-124-

It is a familiar fact (first used by Gfldel in his famous
work on undecidability) that the expressions of FS can be coded
by nonnegative integers. It will be more convenient for our
purposes to use the class of constants (which of course includes
terms denoting the nonnegative integers) as codes. Thus, first
letting each character of the alphabet FS be coded by a unique
integer, any expression consisting of a finite sequence of such
symbols (and hence any term or formula of FS) can simply be
coded by an n-tuple of integers in the obvious way. We assume
that such a code has been set up in some definite way, and write
X for the constant which codes the term or formula X of FS.
Once such an encoding has been chosen, it is a straightforward
task to describe the syntax of FS within LFS . Thus, e.g., we
can find rather short formulae TERM (X) , FORM (X) , SENT (X) of LFS
containing one free variable, such that if a is any constant then
TERI4(a), FORM (a) , and SENT (a) respectively have the truth value
true when a = X, for X a term, formula, or sentence (i.e. formula
with no free variables) of FS , respectively. Note that in
developing the first two of these formulae, it will be necessary
to convert the recursions which would appear in their most direct
expression into references to underlying sequences of objects.
The needed set-theoretic bounds on these sequences can be
expressed using constants of the form R(6).

It is useful for later purposes to extend the preceding
considerations by noting that there exist a pair of formulas
TRU(X) and FAL(X) of FS (but not of LFS) which express the condi-
tions that X is the encoding of a true (resp. false) sentence
of LFS. To construct these formulas, we first construct a
formula IS_VALUE (X,Y) of LFS such that IS_VALUE (y , 6) is true for
given constants y,3 just in case y has the form a and the equa-
tion a = 6 is true. Our technique for doing this is simply to
reexpress the obvious recursive definition of the value
designated by a term a of LFS, replacing the recursion that this
definition involves by the statement that an appropriate sequence
of recursive steps exists. Here we recall that this standard

-125-

technique always allows recursions to be replaced by references
to sequences. However, in order to be sure that there is a
formula of LFS obtained by applying the technique to a given
recursion, we must be sure that an a priori bound for the length
of the recursion and of Lev(ot) for each component a of the
corresponding sequence can be given by applying R, lev, +, etc.,
to the free variables of the recursively defined predicate
we are trying to express. We leave it to the reader to check
that in the case of the predicate IS_VALUE (X,Y) such a bound
can be given.

Next, using IS_VALUE, we create two additional formulae of
LFS, called TERM_IS_MEMB (X,Y) and TERM_IS_EQ (X ,Y) respectively.
The first (resp. the second) of these is to be true for given
constants YwY-j if and only if these have the form a, 6/ where
a and Bare terms of LFS and a e B (resp. a = B) are true.
These formulae can of course be written as

{*) TERM_IS_MEMB(X,Y)

•H- (3U G BOUND(X), VeBOUND(Y) ) (IS_VALUE(X,U)

& IS_VALUE(Y,V) & U G V) ,

etc. where the BOUND needed so that (*) shall be a legitimate
formula of LFS can readily be given in terms of R, Lev / etc.
Next, using these two formulae, we construct formulae
TR_HT(X,Z) and FA_HT(X,Z) of LFS such that for a given nonnegative
integer n and constant a, TR_HT(a,n) (resp. FA_HT(a,n)) is true
just in case a = (}) , where 4) is a true (resp. false) sentence
of LFS containing no more than n occurrences of the symbols
'^r &/ Vf -^r **t V, and 3. These formulas can be written out by
making explicit the recursive algorithm used in computing the
truth value of sentences of LFS, as described above (and of course
by replacing a recursion by reference to an appropriate
sequence) . Note that in describing the truth value of a formula
of the form (VX) (X G a ^ cj) (X) ) or (3x) (X G a -^ 4) (X) ) , we must again
make use of the fact that an a priori BOUND (X) can be written
(in terms of R, Lev, etc.) such that

-126-

is_value(b,y) -^ y e bound (B)

is true for all constants a and B.
Finally we define

TRU(X) « (3Z) (Z e CO & TR_HT(X,Z))

FAL(X) ^ (3Z) (Z G CO & FA_HT(X,Z) ) .

TRU, FAL are of course formulas of FS but not of LFS . (Indeed,
it is a consequence of Tarski's famous theorem on the impossi-
bility of self -definition of truth that no formula of LFS could
be provably equivalent to TRU in FS . )

We have noted above that there exists a systematic procedure
for calculating the truth-value of any sentence <t> of LFS.
Accordingly, in what follows we will sometimes wish to regard LFS
as a rudimentary 'programming language'. The 'programs' of
this language are simply formulae H'(x ,...,X ), and the only
operations available in the 'programming environment' PE which
it defines are

(a) An 'input' operation, which 'reads in' an appropriate

number n of constants a, , . . . ,a and forms the sentence

1 n

$ = H'(a, ,...,a ) by substitution.

(b) 'Execution', which simply calculates the truth value of
$ in some totally reliable way, and announces this value.

Purely for expository reasons, we shall sometimes wish to
pretend in what follows that our programming system can issue
various 'confirmation messages' and 'diagnostics'. This is merely
a matter of coupling the core logical mechanism PE to an
auxiliary system, which can use the elementary true-false indica-
tions provided by PE to trigger the issuance of such messages.

In the next three sections, every reference to a 'program-
ming environment' should be understood as meaning PE . In a final
section, we shall indicate the way in which the formal verification
techniques that we discuss can be used to justify the use of more
highly developed programming systems.

-127-

3. The System VT.

We now sketch a system VT which can check proofs in FS .
VT is to be maintained in a programming environment (e.g., that
described at the end of the preceding section) which can
accept character strings and sequences of character strings
as inputs. Thus formulas of FS can be input to VT in a natural
format. VT will maintain two libraries VA (verified assertions)
and RI (rules of inference) each capable of being updated by
VT itself in a manner described below. VA is a set of sentences
of FS , hence of character strings. RI is a collection of
'procedures' each of which is in fact a formula 0 (X) of LFS
containing just one free variable. The sentence 't'(a) for a
given constant a is to be true only when a = [A ,...,X ,^] for
suitable formulae A ^ , . . . , A ,<}) of FS . When $ ( [ A , . . . , A , ^] )
has the value true , we say that (f) is a consequence of the
premises A ,...,A according to the 'rule of inference' -I^ (X) .
It will be convenient to assume that all rules of inference in
RI satisfy the stipulation that a consequence of a given
sequence of premises remains a consequence if the order of
premises is altered or if additional premises are supplied.
Thus in particular if 'I> ( [ A, , . . . , A ,^]) is true so will

$ ( [A^, . , . , A^, A^^2.' • • • '^m'^-' ^ ^^ true.

Initially, RI will contain various procedures which corres-
pond to the axioms and rules of inference of an appropriate
version of FS . For example, we might expect to find the
following items in RI :

(a) A procedure

AXIOM (X)

where the sentence AXI0M(6) is true precisely when 6 = [A-,...,A ,^]
where 4> is an axiom of FS .

(b) A procedure

MODUSPONENS (X) ,
where the sentence MODUSPONENS (6) is true precisely when
6 = [ A, , . . . , A , ^] where there are i,j, l£i,j f_n and a
formula ^ of FS such that A . = i|j and A. = 0) -*■ (p) .

-128-

For each fixed value of VA and RI , we define a corresponding
notion of proof. (Note that we will shortly describe ways in
which VA and RI can be modified; such modifications will of course
modify our notion of proof in corresponding fashion.) Namely,
TT is a proof if

TT = [^-j^/ . . . ,^ ]

where for each i, 0 < i < n, either 4) . , ^ € vA or (J) . , , is a

— 1+1 1+1

consequence of premises (};■,..., (J) . according to som.e rule of

inference in RI . In this case it is said to be a proof of (t> .

'■ n

We can easily construct a formula PROVE (X,Y) of LFS, con-
taining two free variables, such that PROVE (a, it) is true for
given constants a,7T just in case a = ^ where tt is a proof of <p .
To exhibit the formula PROVE (X,Y), one first compiles the
two formulae

and

SOME_VA(X) = (X = 4)^) V (X = 4>2) V . . . V (X = 4)^)

SOME RI(X) = $- (X) V $_ (X) V . . . V $ (X) ,
— 1 2 n

where *,,...,* are a complete list of the formulas which belong
1 n

to VA and <!>,...,$ is a complete list of the procedures in RI .
The formula PROVE (X,Y) can now be written as follows:

(*) Y(Len(Y)) = X & Len(Y) ^ 0 &

(Vi)-^^^^^^^^Y) fS°^E-VA(Y(i) ) V SOiME-RI(Y|i)]

It is clear that if tt is a proof of 4* and a = ^ , then
PROVE (a, tt) is true. Conversely, if PROVE (a, tt) is true, it
follows that the constant [tt (1) ,Tr (2) , . . . ,tt (Len (tt) ) ] is a proof
of (f) where a = Tr(Len(TT)) = 4).

Note that PROVE (X,Y) is a formula of LFS (the quantifiers and
integers of (*) are permitted in LFS because under von Neumann's
definition of the natural numbers, j < i and j e i are equivalent
conditions). Thus PROVE(X,Y) may be regarded as defining a
strictly finite procedure for testing an alleged proof for really
being one .

-129-

Writing PR-LEV(X,Z) for the formula (3Y)(YeR(z) & PROVE(X,Y)),
we see that this is also a formula of LFS . Finally, we write
THM(X) for the formula

(3Z)(Z S CO & PR-LEV(X,Z)) .

We observe that THM(X) is not a formula of LFS (because of the
occurrence of the term lo) . Note that if PR0VE(a,7T) is true for
given constants a , tt , we will be able to prove tt ^ H(n) in FS
for some fixed integer n and hence, using predicate logic, we
will be able to prove PR-LEV (a, n) in FS . Using predicate logic
again, we see that THM(a) will be provable in FS .

For most versions of FS it will be possible to prove the
sentence

(VX) (THM(X) ** (3Y)PR0VE(X,Y) )
in FS, but we will not make use of this fact.

-130-

4. Modes of Use of VT.

We shall now describe six modes in which VT can be
used. Of these, the first two correspond to the normal use
of VT as a theorem library and proof checker, while others
correspond to the various ways in which we allow VT to modify
itself .

Mode I (Lookup): This is a simple library lookup function.
In this mode, a sentence il* can be presented to VT for verifi-
cation. If 4^ e VA, VT will return a message such as

(1) cf) IS IN LIBRARY

Otherv;ise, VT will return a negative message.

Mode II (Verification) : When this mode is engaged, a
sentence <^ and its alleged proof tt can be presented to VT as
inputs. VT will then translate (fi into its encoding <\> (which
simply amounts to coding a character string as a constant) and
will then execute the procedure PROV(^,it), If the value true
is obtained, UT returns an appropriate message, e.g.

a IS VERIFIED .

If the value false is obtained VT should return a suitable
diagnostic, e.g.

STEP 5 OF PURPORTED PROOF IS ILL-FORMED

or in other cases something like

STEP 11 OF PURPORTED PROOF DOES NOT FOLLOW FROM PREVIOUS STEPS

Mode III (Assertion Insertion) : This mode is similar to
Mode II; however, it is intended that a sentence is both to be
verified and to be stored in VA. Hence, after issuing the
success message (1), VT must update itself. It does so by
inserting a in the library VA. Of course, this makes revision
of the procedures SOME VA(X) and PROVE (X,Y) necessary.* The

Of course, the overall structure of the PROVE procedure will
remain invariant. It is just that SOME_VA(X) will now repre-
sent a different formula of LFS.

-131-

stability of the system is assured by verification of the proof
which was input with a .

Mode IV (Rule Insertion) : When the rule is engaged, a new
proof -rule $, a 'justifying' proposition a, and a proof P can
be presented to $ as inputs. Then VT will first check that a
has the form

(2) (VX)([$(X) - (f (^:i)i<j<Len(X) ™M(X(j))] ^ THM (X (Len (X) ) ) ] ) ,

If this check fails, a suitable diagnostic, i.e.

RULE IS NOT CORRECTLY JUSTIFIED

will be emitted. If the check succeeds, VT will proceed to
translate a into its encoding a and will execute the procedure
PROVE(a,P). If the value false is obtained, VT will issue an
appropriate diagnostic, as in Mode II usage. Otherwise, if the
value true is obtained, VT will issue the message

RULE ACCEPTED ,

and will then adjoin '!> to its collection RI of proof rules.
Of course, this makes reconstruction of the procedures
SOME_RI(X) and PROVE (X,Y) necessary.

A discussion of the stability of the system VT under Mode IV
use will be found in Section 5 below.

We shall now explain how rule IV can be used to extend VT
so as to permit algebraic notations, calculations, and modes of
reasoning to be used directly. Let us first describe the struc-
ture of an extension capable of verifying certain propositions
by automatic testing of certain (necessarily limited) classes of
algebraic calculations. To develop such an extension, we can
write out a formula $ (X) of LFS such that $ (a) is true for a
given constant a if and only if a = [X ,...,X ,^], where one of
the X . encodes a sentence of the form x = t , where t is in turn
the encoding of some algebraic identity a routinely verifiable
by an algorithmic technique (e.g. some special case of the
binomial theorem) and where cf is a translation of o into FS.
The proof of the justifying sentence for such a $ (X) would simply

-132-

be a formalization of some standard proof of the correctness
of whatever algorithm was used to test such alleged identities.
Once VT accepted this new rule, any identity belonging to the
class handled by <P could be introduced as a single step of any
proof that required it.

Of course, in practice one would wish to improve the
efficiency with which formulae of this class were handled,
specifically by replacing the slow general procedure needed to
evaluate the truth value of $(a) by an invocation of some
equivalent but more efficient algebra 'package' directly execut-
able on a computing mechanism M of known structure. Once we have
proved that Mode IV use of VT raises no stability problems, it
will be straightforward to justify the use of such compiled
'packages'. But since to do so involves consideration of the
somewhat technical issue of program correctness, we put off
additional discussion of this issue until Section 6 below.

Now let us consider the way in which VT can be extended
to allow algebraic reasoning in an algebraic notation, thus making
algebraic techniques of a more 'creative' character available.
For this, we need first of all to write out a formula H'(X) of FS
which expresses the statement "X encodes a true formula of
algebra". Technically, this can be put as "X encodes a formula
which follows from the axioms of algebra by the rules of
algebraic deduction". In addition to this, we need various
deduction rules corresponding to the rules of algebraic deduc-
tion. These would be expressed by formulae A ,A2,...,A of
LPS, which might respectively correspond to the rules of
algebraic substitution, multiplication of equals by equals,
solution of algebraic equations, etc. Thus, for example, the
first of these might be such that A (a,B,Y) for a given constant
if and only if a and 3 respectively encode algebraic identities
of the form a = a', and b = b', whereas y encodes a proposition
of the form c = c' which follows by algebraic substitution of b
for one of the variables of a and of b' for the corresponding
variable of a ' .

-133-

To use these formulae, we will have to prove statements of
the form ( VA, B ,C) [ (^' (A) & 4' (B) & A.(A,B,C)) ^ ^(C)], etc.

We also require a formula <!> (x) of LFS , such that ^ {a) is
true for a given constant a if and only if a = [A ,...,A ,^],
where either one of the A. encodes a sentence of the form ^ (t) ,
and where ^ is the translation of t into FS , or vice versa.
Then we can make '$ available as a rule of inference by extending
VT . The proof of its justifying sentence would simply be a
formalization of a standard proof of the fact that the transla-
tion into FS of a valid algebraic formula is a theorem of FS,
and of the appropriate converse of this statement. <i' can then
be used to translate in either direction between sentences of
FS and algebraic identities.

Mode V (Define New Function) . In this mode it is possible
to extend the notation of FS by adding a symbol <p for a new
function using as "definition" a sentence of FS :

(VXw...,X^,Y) [Y = g(X^ ...,X ) - r(X,,...,X ,y) ]
in 1 r n in

where r (X, , . . . ,X ,Y) is a formula of FS .
1 n

VT will check that g is indeed a new function symbol and then
demand proofs of the justifying sentences:

(VX^ , ...,X ) (3Y)r(X. , . . . ,X ,Y)
In In

(VXw...,x ,Y,z) [ (r (X, , . . . ,x ,Y) & r(x,,...,x ,z) ^ (y = z)] .

in In in

If such proofs are provided and are verified by VT, then the
defining sentence of g is adjoined to VA and SOME_VA(X) recom-
piled as in Mode III usage.

Mode VI (Define New Relation) : When this mode is engaged,
a new symbol S, which does not appear in any of the formulae of
VA or RI , is presented to VT, and with it the sentence

(3) (VXt,...,X )(S(X.,...,X ) *> A(X,,...,X )) ,
i n i n in

where A(X^,...,X ) is a formula of FS containing only symbols

which appear in VA or RI , and having no free variables other than

X^ , . . . ,X . VT proceeds immediately to add (3) to VA, and S

becomes available for use as an n-parameter predicate symsol of

FS as extended. No justifying sentence is needed in this mode.

-134-

We end this section with some informal remarks intended to
indicate the significance we attach to the extensibility mechan-
isms that have just been defined. Given any proof verification
system V, one can define the difficulty of a sentence S to be
the length of the shortest input which will cause VT to accept
S , or to be °° if no such input exists. Even though it will
follow by arguments to be offered in the next section that the
extension principles we have described can never reduce the
difficulty of S from » to a finite quantity (i.e., can never
enlarge the set of verifiable sentences) , we conjecture that
the availability of these extension principles will reduce the
difficulty of large classes of sentences by very large amounts
relative to what the difficulty of these sentences would have
been in any fixed extension of V not containing an extensibility
principle or something equivalent to it.

It is known that certain extensions of formal systems (e.g. by
large cardinal axioms or so-called reflection principles) which in-
crease the class of decidable arithmetic sentences, also decrease the

difficulty of some such sentence by arbitrarily large (recursive)
amounts. However, the sentences obtained in this way seem always
to have an artificial post-hoc flavor (even though they can
always be taken to simply assert the nonsolvability in integers
of some Diophantine equation) . And in fact, there seem at present
to be no general principles, not already available in Zermelo-
Fraenkel set theory as formalized within predicate calculus, which
promise to enlarge the class of propositions interesting to the
working mathematician that can be proved. (Recent work in
descriptive set theory, where new axioms have led to real advances,
may give something of a counterexample to this assertion.
But this work is still quite remote from "everyday" mathematics.)

We can thus state the remarkable and fundamental fact that
the very simple formal mechanisms embodied in predicate calculus
and the Zermelo-Fraenkel axioms can track mathematical discourse
in a quite comprehensive manner. But this tracking has been very
much a matter of principle rather than of practice. It is obviously

-135-

quite unfeasible, in practical terras, to represent ordinary
mathematical discourse in raw forTiialized Zermelo-Fraenkel
set theory. Our extensibility mechanisms are intended to
enable one to incorporate the various dictions and methods
of ordinary mathematical discourse more comfortably into a
fully formal system. On the basis of ordinary mathematical
experience we have every reason to expect that the difficulty
(in the precise sense we have defined) of various important
theorems will be greatly decreased in this way. Although we
have been unable to formulate and prove any metatheorems that
would serve as a formal demonstration of this conjecture, we
can point to some suggestive evidence. It is well known in
proof theoretic research that the addition of new rules of
inference to so-called cut-free systems can drastically
decrease the lengths of proofs. In fact an exponential
improvement is obtained (for a suitable class of theorems) for
each use of cut rules that is permitted. Analogously, in
connection with the system VT sketched above we have seen that
the introduction of an appropriate "algebra" rule of inference
shortens to 1 the difficulty of a sentence which asserts an
algebraic identity.

We note that attempts over the past few years to develop
practical program verification systems have increased the
pragmatic urgency of supplying verifiers which keep the diffi-
culty of significant classes of sentences low. Unfortunately,
this has tended to lead to the proliferation of numerous
incommensurable systems, since different authors have proposed
systems designed to lower the difficulty of one or another
somewhat special class of sentence. This has in part tended
to blunt the thrust of the verification literature. It is
rather clear that the extensibility mechanisms described above
allow one to start with any convenient one of these formalisms
and (after considerable but only finite difficulty) extend it
to include any or all of the others. Thus we provide a single
mechanism which, if we leave a necessary initial investment out
of account, can be made as comprehensive as any of the previ-
ously proposed verifiers, each on its own chosen ground.

-136-

5 . Metamathematical Considerations Concerning the Stability of VT .

After our hypothetical system VT has been in operation for
a while, assuming that it has been used in Modes III, IV, V
and/or VI, the "proofs" being supplied the system may be
syntactically quite different (and hopefully less tedious)
from those acceptable to the original system. We shall write
] — a to indicate that the sentence a of FS was verifiable
by VT in its original version .

We have been using the notation PROVE(X,Y), PR-LEV(X,Z) and
THM(X) ambiguously, since these formulas change as VT modifies
itself. To remove this ambiguity we have only to introduce
a counter t, writing PROVE^(X,Y), PR-LEV^(X,Z) and THM^(X).
We let t be initialized at 0 and assume that whenever VT is
used in a Mode which results in modification of PROVE , t is
incremented by 1. It is obvious that PROVE (a, tt) implies
PROVE (a,Tr). That is, if VT accepts a sentence (upon presentation
of a proof tt) , it will continue to accept (f^ as it modifies
itself (by virtue of the same proof tt) . The stability result
we wish to prove is simply that if for any value of t,
PROVE (4>,tt) is true, then |- (J) . Note that, using the formal
techniques introduced earlier, this assertion (for any particular
t, representing some particular sequence of extensions of VT) ,
can itself be represented by the sentence of FS:

(*) (VX) [THM (X) ^THMq(X)] .

Hence it might be expected that the stability proof we give
could itself be formalized in FS . However, this is not quite
the case, and to formalize the proof of (*) in a system like FS we
need to use a system which, though it may be considerably
weaker than FS in many regards, goes beyond FS in a certain
direction. Specif icatly, we need to assume the following con-
dition which we call weak o^-aonsistency (because it is implied
by Gfldel's notion of w-consistency) :

-137-

If ^(X) is a formula of LFS, and if \~ (3X) (X e co & a (X) ) ,
then there is a natural number n such that ^(n) is true.

The assertion that FS is weakly cu-consistent can be expressed
in FG by the infinite collection of sentences:

(4) THMq( (3X)(X e CO & A(X))) ^ {3X)(X e co &A(X))

(or more satisfactorily by a single sentence, which implies
all of the sentences of (4)) . However there are obviously
particular formulas A (X) for v/hich if (4) were a theorem of FS,
we should have:

(5) }— % THM ( (3X) (X G CO & A{X) ) )

(E.g., take for A (X) the formula X = 0 & X = 1) . But it follov/s
from well known results of Gftdel that (5) cannot be proved in
FS if FS is a consistent system. (This is because (5) amounts to
asserting that the consistency of FS is provable in FS . ) This
shows clearly that we cannot expect our stability proof to be
formalizable in FS . However, the proof we are about to give
can be formalized in any system which contains:

(a) a certain relatively weak subsystem of FS, and

(b) additional axioms sufficient to prove all of the
sentences of (4).

Having made these preliminary explanations, we shall now
proceed to present our formalizable arguments quite informally.
We have :

Lemma 1. If PROVE (a, tt) is true, then |— THM (a) .

Proof. We have | — fr e R(n) for some nonnegative integer n.
Therefore by predicate calculus

[— TT G R(n) & PROVE (a, tt)
and hence

|— (3y) (Y G R(n) & PROVE (a, Y)) ,

i.e,

\— PR-LEV (a, n)

-138-

since | — n ^ ^ , we can use predicate calculus again to obtain:
|— (3Z) (Z e CO & PR-LEV (a, Z)) ,

|— THM (a) .

Next we shall need a converse to Lemma 1, and in order to
obtain it we will have to use our assumption that FS is weakly
00- consistent.

Lemma

2. If f— THM (a) then there is a constant tt such

that PROVE^(a,TT) .

Proof. We are given

|— (3Z) (Z G u) & PR-LEV (a, Z)) .

By weak oj-consistency , for some nonnegative integer n,
PR-LEV (a, n) is true. I.e., the sentence of LFS

(3y) (Y G R(n) & PROVE^(a,Y) )

is true. Hence for some constant it , PROVE (a, it) is true. Q.E.D,

We are now in a position to prove our main result, which
gives the stability of VT :

Theorem, If (|) is a sentence of FS and PROVE^(i,TT) is true
then j — ({) .

Proof. Our proof is by induction on the counter t. The
result is obvious for t = 0. We therefore need only verify
that the fact asserted is preserved under use of VT in
Modes III, IV, V and VI. It is a well known property of
predicate calculus that use of the extensions obtained under
Modes III, V, and VI do not increase the class of provable
sentences. Hence we need only show that the property is
preserved under use of VT in Mode IV.

To obtain this result, let us suppose that the transition
from t to t+1 was the result of a use of VT in Mode IV.
and let 0 be a sentence of FS such that PROVE ^_^^ (^ ,^) is true
for a given constant tt . We shall show that [- ^ - We write

-139-

SOME-VA^(X), SOME-RI (X) for the formulas of LFS introduced

earlier, showing the counter t explicitly.

We are given the sequence "t = [$,,...,$ ], where <^ = (f)
_ inn

and PROV (^,7t) has the value true. We shall show that
I — (fi. for i = l,2,...,n. The proof is itself by induction,
so in proving the result for i we may assume that it is known
for all j < i. (Thus the whole of the present proof has the
form of a double induction -- an inner induction on j and an
outer induction on t.)

Case 2. SOME-VA^ , ^ (^.) is true. Then, since we are

t+1 1

assuming that the change to VT involved in the counter

increasing to t+1 was not of MODE III, SOME-VA (i^.) is

likewise true. Hence PROVE^ (4 . , [ A . ] ) is true. By induction

til -^

hypothesis, ] — (p..

Case 2 . SOME-RI , {['^-, ,'^-y , ' . . t"^ ■]) is true . By induction
hypothesis | — (\> . for all j < i. So PROVE (^i ., tt . ) is true
for suitable constants tt . and therefore PROVE, (*.,7t.) is
likewise true for all j < i.

We consider two subcases:

set

Case 2a. SOME-RI ([ cf), , (^ ,...,<}).) ] is true. Then, if we

we have that PROVE (({) . ,7t) is true. By induction hypothesis
(on t) , |— (}) . .

Case 2b. SOME-RI ( [^ , ^ ,..., ^ .] ) is false. Then, the
transition from t to t+1 involved adjoining a new rule of
inference ^(X) to RI , and moreover 0 ([$,, ^-^ ,...,$.] ) is true.
Since $(X) was accepted by VT , it follows that VT (with
index t) must have verified the correctness of the justifying
sentence (2). That is, for some constant tt ,

PROVE^ (TWr[TTxFRTTV3TT7~~ ,^> THM^ (X (y) ) ] ^THM. (X (Len (X) ) ) ] , tt)
t L "^ "^ "^ i-iGXl \ A. ) t u

has the value true. By induction hypothesis (on t) ,

-140-

h (VX)[^(X) - (f (^J)i<j<Len(X)^™t^^^^^^^ - THM^ (X (Len (X) ) ) ]
By the completeness of FS with respect to sentences of LFS

\— ^( [^3_,^2' • • • /^^ ] ) •

Since PROVE ($j , it j ) is true for all j < i, using Lemma 1 we
have "I — THM ("^^ . ) , for j < i. Therefore, v/e have also

Using predicate calculus we conclude that

|— THM (i. )

By Lemma 2, there is a constant it such that PROVE (^. ,7t) is
true. Finally, using the induction hypothesis on t,
|— ({) . . Q.E.D.

-141-

6 . Program Verification and Extension of the Programming
Environment .

In the present section, we shall supplement the preceding
analysis by considering additional issues which need to be faced
when we wish to extend the rudimentary programming environment
used till now, in order to allow use of other computing mechanisms,
programs, and programming languages.

It is convenient for us to view a computing mechanism M simply
as a system which can accept texts of a particular kind, and which,
once having accepted such a text, will use it to establish some
kind of initial internal state, following which this internal state
will be transformed, cycle by cycle. Such transformation
may eventually lead the mechanism to termination. If termina-
tion occurs, M will exhibit some part of its internal state,
and this exhibited part constitutes its 'output'. Suppose that,
as is customary, we always regard the input to such a mechanism
as being divided into two distinguishable parts, called 'program'
and 'input-data' respectively (though in particular cases either
of these may be null) . Then we can write
YIELDS (program , input_data, output) for the sentence
"if the finite objects (and to make contact with the preceding
sections , let us agree that these objects will be encoded as
constants, i.e. constant terms of LFS) 'program', 'input_data'
are presented to M, and if termination occurs, then 'output'
will be exhibited" .

For us to be willing to use M as part of a formal verifica-
tion system, we must of course feel that we understand the way
in which it operates, and for this to be the case we must be
in possession of some formula 'GOESBY' of LFS which describes
the internal operation of M , i.e. a formula for which we
believe the equivalence

(1) YIELDS (program, input_data, output) **

(3c) (3n) (n Goj & c e R(n)) & GOESBY (program, input_data , output ,c) )

to be correct. We can regard (1) either as a mathematical
definition of an (idealized) mechanism M, or equivalently

-142-

(at least for our purposes) as an axiom about the behavior of
a certain physical object (namely an actual computer of some
particular type) .

To use the computing mechanism M as part of a verification
system like our VT , we will generally need to make use of a
program P^ for it which can cause M to calculate the truth
value of some class of sentences of LFS. In order that P„
can be used reliably, we must know that P_ is 'correct', i.e.
that if P processes a sentence S of LFS and terminates with the
output 'true' (resp. 'false') then the truth value of E is indeed
'true' (resp. 'false'). (Note however that P^ need not be
capable of processing every sentence S of LFS, i.e. for some
input S, P may yield the result 'can't handle this input',
or may simply fail to terminate) . We can express the condition
that P be correct as a pair of statements of FS. In writing
these statements, we shall suppose that we have already con-
structed a formula SENT(X) of LFS such that SENT (a) is true
for a constant a just in case a = ^, where cf) is a sentence
of LFS. We will also make use of the sentences TRU(X) and
FAL(X) constructed in section 2 above. (Note again that these
are sentences of FS but not of LFS.) Then the correctness
assertion needed to justify use of the program P^ is expressed
by
(2a) (VX)(SENT(X) & YIELDS ( B ,X , true) -^ TRU(X))

(2b) (VX)(SENT(X) & YIELDS (B,X, false) -> FAL(X)) ,

where 6 is a constant which doees the program Pq.

In practice one will want to lighten the considerable labor
of proving the correctness of programs like P by making use
of auxiliary program verification systems. This implies a
less direct approach to proof of the correctness of Pq than
that which we have just outlined. The following considerations
show how such systems can be used, ultimately to establish
assertions like (2a) and (2b) . We can regard any such program
verification system (PVF) as being described by a formula

-143-

IS_VERIF (X,Y,Z) of LFS containing exactly three free variables,
The sentence IS_VERIF (a , B , Y) is to be true for given constants
a,B,Y just in case a is the code for an object 0 which PVF
will 'accept' or 'verify', B codes the 'program part' of 0,
and Y encodes the 'input-output assertion part' of 0.
(The objects a will often belong to some formal system of
extended or annotated programs which PVF is able to handle,
i.e., they can be program texts 'decorated' with Floyd
assertions. E.g., in the verification formalism of [Schw 1] ,
such objects would be 'praas'. Generally, the 'program part'
of such an object will simply be the program text which it
contains, stripped of the decorating annotations attached to
this text within 0. Note that this program part is assumed
to encode a program P, possibly in a high level language
of which some subset is directly acceptable to the computing
mechanism M.) The part y of 0 is assumed to be the encoding

(^(X,Y) of a formula of LFS which expresses some relationship

between P's output Y and its input X which PVT verifies as

part of the verification of 0. Since we allow the program

part of 0 to be the encoding of a high level language, only a

subset of which gives valid M-programs, we will also need a formula

IS_MPROG{X) , such that IS_MPROG(B) is true for

a given constant B if and only if B codes a program of the

restricted form acceptable to M. Finally we will need a

formula SUBST (X,U ,V,W) expressing the relationship the sentence

W arises by substitution of the particular constants U,V into

the (two-parameter) formula X". That is, SUBST (a , y ^ 6 ^ B) is

to be true for given constants a,Y/<5,B just in case a = (})(X,Y)

for some formula (p(X,Y) of FS and B = <t>{y,&) . Then, in order
to justify use of PVF, we will need to prove the following
theorem (for clarity, we shall give multicharacter mnemonic
names to the variables occuring in it) :

-144-

(3) (VX, PROG, PROP, INP, OUP , ASRT) [( IS_VERIF (X , PROG , PROP ) &
IS_MPROG (PROG) & YIELDS (PROG, INP, OUP)
& SUBST(PROP, INP, OUP, ASRT) -> TRU(ASRT)]

Once (3) has been proved, any P. coded by a constant B satisfy-
ing IS MPROG(B) for which PVF has been used to establish

IS_VERIF (a, 6 , Y ) / where y = (J)(X,Y), and where we also have

(4a) (VX) [ (SENT(X) & (t)(X,true) ^ TRU(X)]

and

(4b) (VX) [ (SENT(X) & 4)(X, false)) ->FAL(X)]

can be executed on M with ^ as input to evaluate the truth value
of <I>. We note again that a given P. used in this way need not
be capable of handling all $; for some inputs 0 if the program
P may fail to terminate or may exhibit outputs other than 'true'
or 'false*. In practice, it may be advantageous to begin by
developing rather simple programs P„ which are capable of
computing the truth values of certain particular crucial classes
of formulas <l> , and then to use these P^ to verify (2a-2b), (3),
and (4a-4b) for more powerful P and for additional auxiliary
verification systems. All of this is merely the kind of
'bootstrapping' process typically involved in getting any
complex system under way. Of course, in actually building a
verification system, one might proceed manually and with a rela-
tive minimum of formal checking to implement some level of
system function that ought more properly be reached by boot-
strapping. If this is done, it is desirable, and may be
possible, to use the initial system to verify itself.

Finally, we note that it may be possible, in a particular
auxiliary formalism PVF, to find an object y satisfying
IS_MPROG(y), for which we are also able to establish the
universal validity of the formula

(5) IS_VERIF(y, PROG, PROP) & YIELDS (y , [X , PROG , PROP] , [Y, PROG ', PROP ' ]
^ IS_MPROG(PROG') & IS_VERIF (Y, PROG ', PROP')

-145-

In this case, the program C can be used as a compiler. I.e. ,
it can be executed with inputs which are verified programs
in the extended sense of PVF , to construct verified programs
(having related, and perhaps identical, effect) which are
directly executable. Note that more and more powerful compilers
of this kind will be constructible by a suitable bootstrapping
process .

Reference

J. T. Schwartz: On Correat-Program Technology , Preceding
Paper, this collection.

-146-

R E S !1Wf-fre^^f

K -^^^it-is*

.. -..i t.

.,

■> >

;v-5g^fg^3yE w^ s\

1 ■2(^'

^i.i:>u

It.

V

J

— ^

CAVLORD

1 —\

5 'Civ

NYU NSO-12 C.2

Davis

Correct programming technology/
Extensibility of verifiers.
2 papers on program verlflcatlor

N.Y.U. Courant Institute of
Mathematical Sciences

251 Mercer St.
New York, N. Y. 10012