A LOOIC FOR COffi-P?CT PROGRA?? D?7EbCPY?ENT
Josep? Lojis Rates
Ph.D. Tbesis
TR 79-3S8
Department of Computer Science
Cornell University
Ithaca, New York 14S53
Auqust 1979
A lOGlC FOR ceRKr.cT PROcfQ&N t?ffiVEL(?P'ffi??T
A Thesis
Presented to the Faculty of the Graduate School
of Cornell Uni?ersity
in Partial Fulfillinent for the Degree of
Doctor of Philosophy
by
Joseph Louis Bates
August 1979
BIOGRAPHICAL SXETCH
Jcsepb Louis Bates was born on October 20, 1953 in Baltimore.
Nar?lsnd. He began study at The Johns Hopkins University in September
1969 as the first early entrant of the later formalized Study of
Itathenatically Precocious Youth. In January 1972 he was admitted to the
Johns Hopkins Craduste School for concurrent study in Computer Science.
He received the degree of Bachelor of Arta in Quantitative Studies in
Nay 1973. and the degree of Master of Science and Engineering in
Computer Science in August 1973, both from Johna Hopkins. He received
Honorable Mention for tbe Clark Teaching Award (given for excellence in
teaching) fros Cornell University in May 1973.
--H`i--H
To Paul. Louis. and Julian
for making it posaibla.
ACXNoWLEflO(ENTS
Professor Alan Demers encouraged my research efforts from the
beginning. His ready car and persistent interest in this work, though
it was not squarely "in his area5. were vital to its completion. In
addition. his technical assistance has significantly improved numerous
aspects of this thesis. I as pleased to have worked with him the last
few years.
Professor lobert Constable provided critical insight and crucial
smpnort during tbs later stages of mv studies. His arguments for
constructive reasoning drove me to understand more deeply the
application of logic to programming. Had he spoken less persuasively, I
would still be struggling with "obviously valid5 classical reasoning.
Xany individuals. in addition to the two above. took time to read
and co-ent upon drafts of this document. William Appelbaum. Milton
Hates. Professor Robert Cartwright. Merrick Furst. and Professor David
Cries supplied suggestions on the style and presentation of the thesis.
My special thanks go to Peter Vanderbilt for many fruitful discussions.
for his careful technical readint of rough drafts. and for constantly
encouraging is to ciplain o+yssl clearly and correctly.
-jy-
Dr. llerlan Kills planted the seed of this ?ork ions ago by a?guing
that people can and should construct correct programs. A glance at
aociety?e uses of computers convinced me of the lattert William
Appelbeum and Fran Corredo concretely demonsttated the former.
Finally. I would like to thank fly friends for aaking time here
tolerable. especially during my self-imposed isolation this last year.
I cannot adequately acknowledge the support of iy family when things
were intolerable.
TAilt OF CONTENTS
1, Introduction1
1.1			The software problemI
1.2			Toward a solutionA
1.3			Organization of the thesis6
2. Correct program development by formsl refinement8
2.1			Some existing approaches to correctness8
2.2			The formal refinement approach to correctness21
2.?			The specification of imperative program segments31
2.4			gefinement rules and the semantic content of proofs38
3.			PEL: A logic for correct program development48
3.1 Types and expressions49
3.2 Generators and iterators55
3.3 Transition specifications63
3.4 Propositions. environments, and justifications65
3.5 Refinement: logical rules70
3.6 Refinement: integers and sets--H81
3.7 Refinement: transition specifications87
3.8 Abstraction 97
3.9 Static analysis and type checking112
vi-
?. The extraction of prosrasa fros proofs126
4.1			Itefinement logic netatbeory126
4.2			The extraction procesa and extracted prograMs131
4.3			Extraction: logical rulea143
4.4			Extraction: integera and aeta139
4.3			Extraction: tranaition apecifications161
4.6			Extraction: definitions and leunna170
4.7			Example extractiona and optimization173
3.			Conclusion18?
5.1			Summary187
3.2			Ideas for future research192
Bibliography200
Collected concepts. definitions. and syntax210
Index of refinement rules216
CIIAPTVM I
INTRODUCTION
1.1 ?ialinu??
With the advent of the silicon integrated circuit in the early
1960's. the fundasental electrooics tecbnology that underlies modern
coiputers began doubling in effectiveness every year (Siewiorek Ct. 51.
1978. Bhandarkar and Juliussen 19783. Prior to this technological
achievement. sachines were limited, society's expectations modest. and
potential applications of computers were adequately realized. liowever,
as exponentially inproving hardware encouraged increasingly cornplex
applications. the burden of producing correct. efficient. ever larger
systeas case to rest on the programmer. Too often the programmer failed
miserably.
As hardware advances continued into the 1970's. the growing gap
between the expectation and reality of software development prompted
computer scientists to examine the programming task in depth. Dijkstra
wrote the frequently mimicked 1COTO Statement Considered ilaruiful5 letter
Dijkstra 1968a) advancing tha idea that the anro statement led to
programs with 5intellectually unmanageable5 control flow. The term
5software engineering5 was coined to convey the notion that programs are
structured objacts to be constructed according to sound anginesring
--H1--H
-2-
principles [Randell and Naur 1968]. progra?ming language seeantics took
on a new aignif:cance as Noare's axiomatic method provided an effective
tool for analyzing both the complexity of languages and the properties
of individual programs (Hoare 1969]. These ideas grew into several
broad areas of research aimed at solving the software problem.
Languages: Progra,ming language designers realized that languages
must aid. not burden, the programmer (Hoare 1973. Wirth 1974).
Languages were developed to support the major intellectual
techniques for handling complexity -- abstraction, case
analysis. induction. etc. -- without themselves becoming too
complex to understand. Study of such areas as data abstraction,
control abstraction, scoping. and modularity led to proposals
for various supporting language constructs.
Nethodology: After considerable debate. the 5code then debug5
philosophy gave way to the idea that programs could and should
be constructed to function properly the cat time execute,:
(Nilla 1973]. Top down design from well specified requirements
became an accepted development technique. Progra?era
recognized that testing alone could only mildly increase their
confidence that a program was properly constructed; assured
correctness had to be built in, it couldn't be tested in.
Verification: The notion of program correctoess was formalized in
various ways and techniques were developed to prove programs
correct. (Correctoess means performing according to
specifications. Assuring the aptnesa of specifications is an
important, but distinct, problem.) These ideas affected
programssing languages and methodology? they led to tha
-3-
suggestion that programs and their proofs be developed
simultaneously. Systems `gere built to support program
verification with varying degrees of automated aid.
As of the late 1970'.. many of these advances in progran-ing
languages and methodology have had an impact on the construction of real
world software. Top down development and structured programming have
been adopted by a wide variety of software producers. Articles
proposing or analyzing other techniques appear constantly in the data
processing industry's trade journals. Myriad introductory programming
texts describe top down development in PVI subsets or PASCAL.
5Structured progra?ing5 preprocessors for FORTRAN, COBOL. and other old
languages seem as common as the compilers themselves.
In contrast, thougb the idea has been in the technical literature
for over a decade. formal verification of programs has not had a direct
impact on real world software production. That is, people almost never
carry out complete formal verificatione of their programs. For
interesting algorithes. existing formal proof techniques and their
informal counterparts are adequate. These short programs. often
published, are subject to the detailed scrutiny of many iod?viduale.
Real programs, however. are often so dull that only the original
programmer ever reads them. Existing techniques. though theoretically
adequate, are exceedingly tedious in this domain, even if mechanical aid
is supplied. Thus. one finds that enforced formal verification with
current technology is unacceptable in practice; yet. because real world
programs are too large to be fully tested and are produced by
pr?gra?s?rs ?ith a ,,r,jst?nt t?n.;?n?y to err. f?'rma;?nR of ,uma
-4-
kind (checked by sachine) is exactly what is needed to guarantee the
correctneaa of large programa.
1.2 Za??1??i?
The work presented herein is based on the belief that current
verification technology is inadequate largely because it fails to
directly support effective methods of progras development. ?(oat
verification techniques are analytic tools. applicable to arbitrary code
segments divorced fron their development; simila?ly. soat verification
systems analyze arbitrary programs and yield a set of lemmas
(verification conditiona) that must he proven. In ny experience.
however. careful. accurate prograusaera having low error rates develnp
correct programa with informal reaaoniug -- they seldom verify completed
programs with formal reasoning. Though formal techniques for analyzing
code can help guide informal development .e.g. flijkstra?s uae of
predicate tranaforuera (Dijkstra 1976). verification systems based on
these techniques are code readers -- they can only insure correctoesa by
anslyais performed after code is written. In contrast. this thesis
claims the need for a habitable formal logic and associated support
system for correct program cnn.tructinn
A logic for program construction should formalize a particular
development methodology. not just the semantics of a conventional
programming language. The text produced by a programmer should contain
the complete record of an idealized (l.e.. no backup) development of his
program. including all reneoning needed to dt.monatrate i?a correctness.
Prugr rs are y,e1?.'raI ly a?.? ?f a r..as?nje? Jur'?g devel??ment of
-5
forrect code. Providing a fors?l notation for recording it peruits
program and proof synthesis to be integrated into one unifled process5
with correctoess of the evolving program insured at all stages. This
approach forsalizes the methodology advocated by many authore of
structured proarsamaing texts (Wirth 1973. Conway and Cries 1975,
Dljkstra 1976).
?stsbliahing program correctness is viewed differently from this
vantage. Verification as a distinct activity no longer exists since
incorrect progranLa cannot be produced. Executable code is obtained only
by means of correct formal development. This change in viewpoint is of
great psychological importance becauae it captures the idea of
prograsnaing as a methodical process of discrete. manageable deci.ions in
which the concepts of bugs, quick and dirty prograna, etc., never arise.
When constructing programs to meet given specifications. I believe
limiting one's thought in this way is not ?ust appropriate. but
assentisl.
A program development logic requires prograu?ners to manipulate
substantially ,sore text than is usual. Also, formal reasoning has an
advantage over rigorous reasoning only when it is mechanically checked
for validity. Thus, an interactive system that assists and watches the
prograsiser is sn indispensable part of this approach. The minimal
version of such a system must provide clerical help in manipulating
program developments sod should check the validity of reasoning used
therein. Im addition, the system should take over the work of proving
the less of trivial propositions found in developments. The constantly
increasing ratio of software to hardware Costa bee ude any such
-6-
assistance ecoomically attractive. even at the expense of substantial
dedicated computing power.
The view of program development advocated here clearly contradicts
the well known argument that 5programs should not be written at
terminals5. The reasoning behind that claim applies to conventional
(edit-run-dehug) systems. because they effectively support only the
5modify until.sll the test cases work5 methodology. Ny proposal is for
a system supporting a more tenable methodology requiring and helping
the programmer to reason about all possible executions. I envision
construction proceeding via a man-machine dialogue. perhaps a variation
of that suggested by Floyd (Floyd 1971]. The dialogue would emphasize
correct reasoning in a style suited to expressing complete idealixed
developments.
1.3 Oreanization ? the thesis
The body of this thesis is the presentation and analysis of PRL. a
logic for the top down development of programs. PRL an acronym for
Proeram Refrinemeur ??. is a tormalism that provides for the
specification and correct refinement of programs operating on integers,
hooleans, and well typed. homogeneous finite sets. The logic is the
result of my attempt at the 5habitable formal logic ... for program
constructions called for in the previous section.
Chapters 3 and 4 contain the major technical results of my work.
Chapter 3 describes PRL in depth; it includes examples dispersed
throughout the text. Chapter 4 presents a detailed account of a method
--H7--H
for aitractias (1.s.. compiling) programs from proofs. Inherent in this
account is a desonstration of the logic's consistency.
Though I have tried to limit the bulk of the thesis. chspters 3 and
4 have steadfastly resisted my efforts. In chapter 2. the 5casual5
reader will find the general ideas of refinement logics. motivated and
developed from previous work on program correctnesa. Chapter 5 first
sunnarizes the three fundamental ideas that underlie PaL. then
enunerates a variety of areas subject to future study. Thus. chapters 2
and 5 provide an overview of refinenent logica in the context of past
and suggested research.
CWTKt 2
CORRECT PRoCRA?q DEVELOPMENT DV FODEL W1!wD(?ENT
2.1 Some existing annroacbea ? correermeas
I shall now discuss a variety of methods aimed at belping people
produce correct imperative programs. These methods range from the early
work on formally defining correctness to automatic systems for
synthesizing correct code from specifications. They roughly fall into
three catagories: development methodologies, formal logic.. and computer
based programming support systems.
The fundamental idea in establishing correctnesa is that uecutable
programs may be interpreted as defining classes of computations. One
can analyze a given program to determine its leaning. that is. the claas
of computations it performs. A program is said to be correct exactly
when its determined meaning is consistent with a separate specification
of its intended meaning.
Early workers on program verification (Naur 1966. Floyd 19671
developt'd a method of assigning predicate.. called Inductive assertions.
to various points In the control flow of a program so that every time
execution reaches any particular point the corresponding sasertion is
true. By choosing ss?ertions appiopriately and examining all ex??ution
paths bi?twcnn an p?i r. l?prov?d norr.rt n that the
-9
otitnut assertion will hold at termination whenever the innut assertion
holds initially. The pair of input/output assertions forms a
specification of the progreas. 7or exaxple consider the followin8
saerted prograi segIent to Cuss the first ? positive integers.
(Mxl)
s			i;
K			It
A S-sui of I up to KI
MhLL' KxM ?
jlxtt<N A Sam- of I up to r)
I			1.1;
5 ? 5+1;
A Sauss of 1 up to I)
(S=sus of 1 up to NJ
The assertions are boolean expressions of the variables of the program.
They are written in curly braces and serve to describe the stete of the
variables when control passes by the assertion. The specification for
the program segment is that if Mxl initially then 5 will be the sum of I
up to II when the segment completes.
Soars extended tbe idea of adding assertions to programs into a
logical systea that provides both a formal definition of the semantica
of several language constructs and a method of reasoning about
individual prograssa (soars 1969). This wiomat,c technique defines each
language construct by describing the relationship that must bold betvsen
e
assortiona placed before atd aft?r any Instance of the construct. thus.
the meaning of an asaigneent statement x+e is defined by ???e? ????
where ??e is the assertion P with all free occurrences of x replaced by
a. (Roughly. an occurrence of x is free in P if it represents the value
of the variable x global to P. Thus. in x-5 v ( ?x)(f(x)--5) the first
occurrence of x is free but the remaining two are not. they are bound
occurrences of x.) For example. (x+2=31 ?+2 (x-3) and (1-2] ?l (x-2J
are both valid since the truth of the orecondition (to the left) before
executing the assignment insures the truth of the nostcnnA,?.on (to the
right) afterward. In a correct asserted program. if a precondition is
equivalent to false (as in the latter example) then control will never
reach the succeeding statement.
The axioms that characterize simple statements are augmented by
inference rules that describe composite constructs. thus:
(pAl) s1 (?) (PA?,g) s2 (q)
election
(11			li			B then			s1			elae S2			li			(Q)
(PAR] s Ip)
ite?ario			___
?ie g ? s ? (pA?B)
(P is called an inva?jant because
it is true before and after every
iteration of the loop.) e
P?PIa QI?Q. (pi] s (Q'J
(Pi s jq]
--HIl--H
vbere the horizontal line indicates that the conclusion below follows
frou the hypothese. above. Since ?oare?s original work auch attention
has been directed at axiolatizing a wide variety of additional language
constructs (Clint and Hoare 1972. Noare 19?2a flcare 1972b Clint 1973.
Hoare and Wirth 1973. Otricki and Cries 1973. Shaw et. al. 19763.
A program nay be forsally shown correct by providing assertions
throughout that are related by the axioms and inference rules of the
logic. The following shows a fully asserted program to eearch a sorted
array. It is correct according to the above rules.
-12-
let sorted--H( Vt.i)(l??j'N?AEi?'A(iJ)
and in(i.j)--H(3k)(??j A Atk)?x)
tbe total specification for tbe progral is
(N?l A sorted)
(in(1.N)?A[K3--X A ?tn(l.N)nK?O)
(N?l A sorted)
(lSlSNsN A sorted A in(l.W)?in(l.N))
(1s?NsN A sorted A in(1,N)?in(L,M))
(1??HSN A sorted A in(1.fl)?in(L.R))
while L<il ?
(1?laHsN A sorted A in(l.N)?in(L.H) A L<HJ
A sorted A in(j?W)?
( (AFLOOR((L+11)/2))<xAin(yLoOa((L4H)?2)$l `i))
v (A(FLOOR((L+li)?2))?KAin(L,FLOO1((L+H)/2))J ))
K?FLooR((L+H)/2);
A sorted A
(LALK)?xAlj(x?1.u)) v CAL?JxAiI(L.K)))J
li AlKJ<x then
(lsLsK<I!sN A sorted A
(EA?K)<XAin(K+l.1i)) v (A(K)?XAin(L.K))) A ALK)cx)
(isK?IsI?N A sorted A
tlsIsusN A sorted A in(1.N)-?in(L,H))
A sortsd A in(I.N)?
((A(K)<XAin(K+I.H)) v AIcJ?xAin(L,K))) A ?A(k)<x1
i1'La?N A sorted A in(1.N)nic(L,K))
A sorted A in(1.N)?in(L,H))
li
i1'?H?N A sorted A in(l.N)?in(L.I1)J
A sorted A in(1.N)?in(L.H) A
A in(1.N)?AL]-I)
li AfL?--x then
?jS?? A in(1.N)?AtL)--x A
(in(1.M)?A(L3--I A ?in(l.N)?L-O)
L?L;
A in(1.?()?AL)--X A
?in(1.N)?Ao)--x A
1-0;
?in(I.w)?A(i)-x A
li
(in(1.M)?A?)'I A
-14-
Certainly t?e above text is larking in readability. but human
engineering concerns aside. there are three technical ways in which the
asserted text shown fails to capture one's intuitive understanding of
the program's correctneas. First, the program need not terminate --H--H the
output assertion will hold if control reachcs it. but it has not been
shown that this will necessarily occur. The difficulty lies in the
iteration rule; it guarantees only nar'i?1 correctness. To show toral
correctneas, i.e.. that the program will indeed terminate with the
output assertion true. a hypothesis must be added to the iteration rule
placing some further constraints on the loop body. The usual technique
is to require each execution of the loop body to decrease the value of
some integer expression that must remain strictly positive for continued
iteration. Thus, a total correctness iteration rule might be written
pAgAt--t' is) PAt<t'. tso??3
iteration			___
p (? g ? s ?) pA?5
where t is an integer expression of the program variables and t' is a
new name not occurring elsewhere in the proof. In the search program
loop one could choose t,,H-L since U-l5O??,L<ll and the body will bring
11 and L closer at every iteration. Several recent forssslisms,
recogniLing this limitation of I3?5?5?5 original approach, are based on
total correetness (Diikstrs 1976, Constable and O'Donnell 1978).
The second failure of the asserted program method is that program
segments cannot conveniently be restricted to changing only selected
variables. Thus. the specification
--H1?--H
!N?l A sorted)
tin(l,N)?A(g)-? A ?in(l.N)?g=o)
is satisfied by a program that sets all M elements 0 A to one and K end
X to zero. The usual solution here is to introduce loe?cal constants
that cannot be referenced by the program. These may be uaed to record
the initial values of any program variables that should not change. The
complete specification for the search example is then
(N?l A sorted A X=11 A N-N' A
(xal' A N-N' A (Vi)(lSi?N?A(i)-A'[i]) A
io(l.N)?A(K)--X A ?in(l,N)?K=O)
where x', N', and A' are logical constants. A difficulty with this
solution is that every assertion in the program must include clauses
stating the invariance of selected variables. With top down development
each program contains independent segments that have their own
specifications; the proofs of these segments are then permeated with
assertions about the invariance of global variables that are not
referenced end should not even be considered within the segments.
The final problem with asserted programs is that uses of the rule
of consequence are not fully justified in the asserted text. In the
search xanple. ?ach occurrence of two sJjac?.flt esaertio?a corr.sponds
to a logical implication that must hold for the proof to be valid.
These implications. called veriticnrion condirina (VCs). are assumed to
be proven in text external to the asserted program using the theory of
the underl>it'g logic (e.g.. integer arit?rnetic). Since these proofs are
-16-
necessary to demonstrate the correctneas of the program. and often
contain reasoning essential to understanding it. I believe they shoold
be an integral part of the program text. As will be shown. PIL
overcomes these technical problems of Hoare?s logic.
yloyd?s early work on the inductive assertion method has been used
aa the basis for nany verification syatema (ring 1969. Good 1970.
Deutach 1973 Bledsoe and Bruell l97?. Waldinger and Levitt 1974.
Igarashi et.al 1973. von Henke and Lorkham 1975. Good et.sl. 19753.
These systens typically require only that the user provide invariants to
cut every loop; they autonatically generate the necessary verification
condition. (King 1976J which are sent to a theorem prover that attempts
to conplete the verification. sonetinee with interactive user guidance.
The fundanental approach to correctness here is 5after the fact5
verification in which completed programs are submitted for vC generation
and proof. Thus. theae systems are completely independent of the
methods used to construct input programs.
Nany researchers interested in correctoess find existing
verification systems lacking. Their objections divide them into two
distinct groups. however. One group finds that the information users
must supply to allow a posteriori verification is too great a burden;
their gosi is to increase th power of mechanical vsrifiecs 5. much as
possible so that all interral arsertions can bc automatically generated
and proven frou the spoc iL IcatIons and code (??spss 1974. ?eca?n and
Weghteit 1975. Xat? and ?anns 19763. The other group rejects a
poateriori verification as a rana of achieving rrrctness: rather.
they argue that p?ogrc?a si0 6 c?'? ? cuctt? :???, wi h )?ric proof.
--H17--H
in such a way that correetmess is assured at all stages cf development
Enjikatra 1968h. Nills 1975. Dijkstrs l9?6. Cries 1976). Study of this
constructive approach to correctness. generally considered programming
nethodology. has yielded informal techniques as well as psychological
attitudes that enable programmers to greatly increase their productivity
(Nills 1975]. This thesis is based in part on the bel?ef that automated
aids for insuring correct software should support these techniques for
correct program development rather than after the fact verification.
Dijkstrs'a calculus of guarded cotmands is a useful mathematical
tool that aids in the formal development of correct programs EDi?kstrs
1975a). In his recent book each program is developed with an informal
discussion that makes heavy use of formal techniques. but the correct
programs that result are pure code with none of their correctoess proofs
contained in the program text fDijkstra 1976]. I see this as a
significant fault; since proof and program should he developed as a
unit, so should they be presented.
In contrast. PLfCf is a formal logic whose well?formed formulas are
correct program/proofs (Constable and O?Donnell 1978. Constable and
Johnson 1979). These combined objects are a variation of asserted
programs in which all the reasoning needed to establish total
correctoesa is combined with the program text in a relatively natural.
rudable way. The formality of the logic allows reasoning to be checked
sachanically. thus justifying a high degres of confidence in tha
correctness of programs.
-18-
Pl?CV is a significant step in the solution of the software crisis.
yet it too is only a step. Its major failing is the lack of a
methodology for producing program/proofs in stages, as the constructive
approach calls for. PRL is the result of an attempt to remedy this
failing by formaliring a logic of program development, not juat
programs. where each well formed formula describes a mechanically
verifiable idealized top down development of a program. Such a logic
should be a souod foundation from which to build automated interactive
systems thst aid in the consteuction of programs.
The interactive developmeot of correct programs is an attractive
idea that has been discussed before, Floyd presents an imaginary
dialogue between man and machine that leads to a search program similar
to the example above (Floyd 1971]. Though quite brief. his discussion
provides much worth conside?ieg and clearly demonstrates the potential
benefits of the system he envisions. Moriconi has developed a system
for incremental development that aids the user ir determining the
effects of changes to specifications, code. and proofs when using the
embedded vc generation based verifier (Moriconi 19773. A limited
facility is provided for partially refined programs and top down
development, but Moriconi is mostly concerned with an intelligent
natural language interface and reducing verification effort by keeping
intact any work still valid after given changes are made. A recent
paper from MIT describes the theory and initial construction of a
orozramner's anorentice that aids experts in the development of LISP
programs (gich and Shrobe l9?83. The proposed system 5knows5 enough
about the prograaamins task and specific Programs to watch development,
--H19--H
notice inconsistencies. suggest correction.. vrite programs by
inatantiating abstract achena. and answer questions. Though still under
devalonnent. the LISP apprentice appears to be an inportant step toward
the reslixation of rloyd?s ideas.
A somewhat different approach to correct program development is
taken in work on correctness nreaerv.ne rrafl.tormnr?ons (?ernart l975s.
Cerhart l975b. Surstall and Darlington 1975. Baizer et.sl. i??6.
Wegbreit 1976. Schwarti 1977). Here much of the complexity of real
programs is tbought to result from the need for efficient execution.
Thus. a methodology is proposed whereby the program ia first written in
as simple a form as possible. so that correctneas is eaeily shovn. and
then correctneas preserving optinizing transformations are applied to
produce an acceptably efficient equivalent. Cerhart further proposes
that many conon program constructs. e.g.. search loops. could be
abstracted. proven correct. and listed in a handbook of valid schema.
Large segments of the initial (simple) program might then be formed by
combining appropriate instances of these established achema. A catalog
of program transformations has been developed to support this
methodology (Standish et.al. 1976).
In its pure form. the program transformation approach is limited by
the ability of programmers to express short. clear solutions to real
programming tasks. It seems to me that the approach would benefit from
the introduction of a specification language of substantially greater
power than the programming language. Creating a fully recorded
transformation from initial specification to final code is similar to
constructing a PRL program developm?nt. Thtrc arc two main differences
-20--H
Pint. PIL restricts tbe class of transformation rules to refinenenta of
individual specifications. guaranteeins that each development is a
simple hierarchy of transformations. Second. PIL specifications 157 be
ststements of pure logic. rather thsn only progral specifications.
These logical statements carry constructive (executable) leaning. thus.
correctnees and execution are highly intertwined concepts (see section
2.4).
The final area of correctness research that will be considered is
automatic oroerammin?. The goal is to automate th? programmer. and
possibly the analyst. out of existence. There are two overall phases in
the use of an automatic programming system. though they nay overlap in
time: problem ecquisition and progra synthesis. Some researchers.
studying the simpler task. describe techniques for synthesis that start
from some formal specification of the problem (Manna and Waldinger 1977.
Long 1977. Nanna and Waldinger 1978). A few more ambitious researchers
are attempting the construction of synthesis systems capable of
acquiring the problem specifications directly from con?ersation in
natural language with relatively naive users. much as would a
programmer/analyst (Belter et.al. 1974. Green 1976). Though Dijkstra
considers efforts at producing such systems 5a theme that recurs with
the same regularity as influenza epidemics' and the likely result of
using tiem `design specif lcati?na jruduc?d a. a kind of p5?l????n
alobber11 (Dijkstra 1971b]. it seems probable that systems of this t?pe
would be extremely useful in bringing th- power of computers to the
public. In any case. ?any of t?e prohl-ma studied in automatic
programeing re:e?e			imila.us inrional programming
-21-
(e.g.. specification languages. program synthesis methods. insur?n
correctuess) and the work being done is of interest. even if successful
autometed systefla are far off.
This completes my lengthy but necessarily incomplete review of
existing work on the problem of producing correct imperative programs
(ses (London 1972. gispas et.sl. 1972. London 1975. Greenspan end
Homing 1977. Barnard 1977) for further references). The last decede
has seen a tremendous volume of work done in this area with tha
attendant publication of many hundreds of papers. I have tried to
present enough background to enable the reader to understand and
evaluate tbis thesis in the light of current knowledge; I will provide
fly own comments and analysis in the following pages.
2.2 Zh formal efinenent A??
I have had the valuable opportunity to observe several programmers
whose programs almost always ?ork properly the firat time executed. The
most important aspect of tbeir rare ability seens to be an attitude of
precision that might be phrased 5programming is a task in which I must
carry out a series of discrete decisions and actions. each of which is
simply acceptable or not; therefore. I can and will take care never to
introduce a line of code whose correctness I am unsure of5. Given this
attitude. the appropriate time for machine aid in avoiding coding errors
is not during program etecution5 nor iC it during a post-development
reading or verification. The appropriate time for machine aid is during
program development.
-22-
In order to determine meciicatly whether the construction of a
program is proceeding along an acceptable patb. one needs a formaliam
for expressing both the stages of partial development and the reasoning
that justifies their correctoess. The method of top down programming.
in which problems are repeet?dly bro?cn down into a composition of
smaller ones, has been proposed by many and found beneficial for
constructing complex systems (Wirtb 1971. Nills 1971. tiskow 1972, Baker
1972a, Baker l972b). I have chosen to explore s?logic of formal top
down development in which the well-formed formulas are correct partial
refinements of progr?ms from their specifications. The remaining three
sections of this chapter informally describes the fundamental features
of PIL in preparation for the formal development of chapter 3.
Consider the following top down description of the search program
that vas presented in section 2.1.
/a If x occurs in A1:N) then set t so that AXl--L
otherwiae eet K to zero. Assume N?1 and Ail:N)
is aorted in increasing order. a?
var L,B: inte2er;
?* With the invsriant (1?1sH%N, A(ltN) is
sorted in increasing order, and AfL:H) contains
X if A(ltN] does), decrassa l1-L to asro, a?
flila L<li ila
?* Split AEL:H) into noneepty parts
and adjust L H to bound a
part of A that most contain X
if AfL:Hi itself does. */
K?FLooR((L+?)?2)?
li A(xJ<x
then L?+1
Ii
li A(LJmx
then I?L
liu 1*0
li
Ineb Inglish comleent dascribes the function of the proarai text
indanted belov it. In general. one may delete the refinements for any
set of coflents and obtain a correct. though incomplete. program. This
provides a natural view of the text as a tree of specifications with the
initial specificstion at the root and executable code at the leaves.
The program may be read and underntuod level by level. Its correctnees
can be insured by checking the validity of each refine?ent step without
regerd for aitber surrounding text or !uwt'r levels of refinement. These
two properties of refinement validity are most important: the freedom to
ignore deeper refinements slle?s cor?ec5 to be cb?cked coot inually
24-
during developaent5 thus (in theory) perlitting use of the attitude of
precisiont the freedom to ignore context insures that correctoess is a
local property of limited complexity. thus guaranteeing the practical
feasibility of developing only correct progrema. A foriali?ation of top
down description should maintain these essential properties.
The first step in creating a logic of progran refinement is to
capture the tree structure of developments. In PaL each level of a
development has the form
specification ky
refinement
where the refinement specifies a set of subproblems and describes bos
solutions to these subproblema may be coaposed to for, a solution to tbe
original problem. All specifications are expressed in the same
notation. A certain class. subject to direct implementation by the
5compiler5. nay be written at the leaves of a completed development.
A specification is said to he ?jg when it defines a terminating
computation. The easily implemented specifications that need no further
refinement are the axioms of PRL. The rules of inference (allowing
validity to be extended to other specifications) are formulated as a set
of ,?f?n,'m?nt nLLn that describe legs! reasoning steps in furmel
developments. A aucceasful development begins with a problen
specification. proce?dipg by repeated application of refinment rules
until all remaining unrei??eJ apecifications are axioms. Although
backup and modifi			- a?) ccc d			g itE cunstructiun the final
--H25--H
text describes a complete, idealized, top down devetopmcnt or a program
meetins the original specification. Equivalently, the final text is a
trss structurod proof of the oriatnal specificatton's validity,
The informal example developed above leaves out much of the
reasonleg needsd to assure correcteess. In the fore?l system, however,
each refinement should include the complete argument by which solutions
of the subproblems may be combined to form a solution of the whole.
Hence. refinements will include aubproblema that are statements from the
domain of pure logic. These will be proven in the same refinement style
by which programs specifications are implemented. This style is a
variation of Gentxem's natural deduction systems [gleene 1952. Prawita
1965. Sxsbo 1969) in which the structure of proofs is made explicit. I
wilL use the term oronosit?on to denote both program specifications and
logical statements; the refinements of both are oroofa, A program
development is the constructive proof of its specification,
Since correctoess should be a local property of the text, it is
important in the development of a large proof that the validity of
refinements not depend on dispersed information. This means that
propositions must be stated in full without any hidden assumptions or
dependency on surrounding text. Nevertheless, they muat also be concise
and readable, so PRL provides for a uniform user-defined global
environment of definitions and theorems that can he explicitly
referenced, Definitions allow the specification language to be extended
to higher levels of abstraction; theorems serve to capture and name
generally useful facts so that they can he used later without repeated
proof. Yor instance, simca a specification is proved by a program
-26-
development a theorem thnt claims a specification associates a name
with a program development (i.e.. a segment of code). Such a theores Is
simply the dafinition 0 5 procadure. Tha uniformity 0 tIc Slobal
environment allowa nun-local rsf.'rences Lo be intsrp?sted without
concern for their context.
The development of P?L has been confined to the study of imperative
program segnents whose only noticeable effects when executed are to
modify the values of global variables. Though I believe the idea of
formal refinement is applicable to other constructs. such as
expressiona. data types. and CLII iterators [Liskow et.al. 1977). these
extensions are not herein discussed. Facilities for input/output are
also omitted. though they may be modeled by introducing explicit input
and output variables of appropriate types.
The specification for an imperative program segment must state the
way in which variables global to the segment ar changed by its
execution and the orecondjt?qn under which the program segment may be
executed to achieve the deaired effect. I shall discuss the
specification language in depth in the next sectionl for now it is
sufficieut to assume these two components. Thus.
N>O set X to the minimum?f A[J:N)
specifies that the refinement only need apply if N is positive and them
it should change only the variable I (to the minimum array element).
The following shows how the aaarch example might look when
expreased (still informally and incompletely) according to the above
discussion.
--H27--H
gaL sorted --H			AL
gaL in(i.j) --H (?k)(iSkSj A A(k]--x)
N?1Asorted set K ? li in(1.L) tb?n AK)?x pigs K-O li hx
vsr L.H;
N?iAsorted 5cr L.H AL 1?1S1tsN A in(1.N)?jn(L.?) kx
set L.H ? 1.1;
i?vpripnr 1s?HSN A sorted A (in(l.N)?in(L.H))
IA U-L+ whiie L<H ilg
1???NAsorted set K.L.H ? X?.L'.H' LL
?L'SH'?H A H'-L'<H-L A (in(L.H)?in(L'5H')) kz
p?ove L?FLooR((L+H)/2)<H;
ifl K ? FLooR((L+H)?2).
i??I?NAsortedALSK<H ili L.H ? L' 11' AL
1SL'sH'?H A ll'-L1<ll-L A (i?(L.H)?in(L'5H')) b:
1?LSHsNABortedA?K<H Drove
IL A(K)<x then in(L.li)?in(K+1.M)
liu in(L.H)?in(L.K) li
IL AEK)<x then ? L ja K+1
else set H ?			li
1StN?NAsortedA(in(1.N)?in(L.H)) Drove iD(1.L)?A(L1sX
if A(L)--x ?hu in K ? L ? K ? 0 li
-2S-
The text of a development in PIL is not a ptogra in the esual
sense: rather. it is a proof presenting all the reasoning needed to
establish that Come program exists which meets a given specification.
All such existence proofs are required to be constructive so that a
compiler for the logic can extract a suitable program without undue
difficulty. Aside from this restriction. however5 there is considerable
freedom in the choice of proof system employed. This work explores only
a rather simple system in which the construction of programs from proofs
is eaaily accomplished. ?owever I can imagine e' interactive faci?lity
supporting semi-automated refinement in which a proof is any discussion
or strategy that leads the ayatem to an acceptable implenentation of
guaranteed correctoesa (Cordon et.al. l977a. Cordon et5al. ls?7b1. The
final recorded text may be either the complete discussion (including
dead ends) or only the reasoning actually needed to construct the
implementation. I have chosen to study the latter variation5 where
texts are both idealized developeents and static proofs.
This view of an entire development as a proof helps keep the
programmer5s attention on the logical soundness of his reasoning. not cm
the extracted pr?gram and its execution. It also assures that the
development process is not programming followed by verification. but a
unified activity of proof in a single logical system. In contrast5
asserted progree logic. allow the dev?lopment of code before much
consideration ia given to corr?ctneaa. The very existence of execotable
code as an entity indep?ndent of any reasoning encourages the view that
verification is a diversion from tie troe task of producing code5 In
reality. caruful reas?ning is th.?.f programming. Avoiding a
notation in which pure asecutable code can be expressed forces the
shift. tbat I believe eeeentiel. away from the paradigm of verification
by program aoalyeie.
The natural method for producing PRL proofe is. of course. top down
develupsent. in euch e development sech refInement etap repreeente e
decompoeition that the programmer feels je most appropriate and
underetandable. The pure logical propositinne that muet be proven ariee
only from local considerations of refinement correctneas. Since they
follow the top down development. rather than resulting from analysie of
lower level code. they are expected and understood by the programmer.
Thus. PRL avoids the problems of logics for program analysis in which
programmers must often prove verification conditions involving
aseertione that have been 5pushed through5 large aegments of program
text. For example. in contrast to Diikstra?s weakeat precondition
method of code analysis Di?'katra 19?6), the top down derivation of
specifications yields `appropriate5 preconditions. i.e.. logical
formulas whose terminology and content are appropriate to their
refinement level.
An apparent disadvantage of the PRL notation is that the
hierarchical nsture of proofs is not easily accommodated on paper.
Reading end writing of tree structured pronfe requires display of a nods
and its anne alone. without the descendants of the sons getting in the
way. ?owever in an age of inexpensive and powerful computing hardware.
there is reason to believe that the inherent limitations of paper ars no
longer relevant to progremming logic design. Rather5 advantage should
be taken of the flexible seodee of text structuring made possible by
-30-
dejira:,a cnmpor?rs (kay a, Coldherg 1977. Nelson l97A3. Ons
cnn envision the 5smart editor5 comlonent cf an interactive program
development system conveniently allowing one to traverse hierarchical
proofs, examining and creating them level by level. The presentation of
PRL proofs in this exposition is hindered by the linear nature of the
paper. but the reader should imagine that proofs are being manipulated
on a display acreen sufficiently large to present any single refinement
step in full.
I would like to make one final coesaent on the refinement style of
reasoning. Even before it was so apparent to me that FRL should be
considered a logic for reasoning about specifications. I had decided to
use refinement as the fundamental technique for structuring
developments. When I needed to introduce a method for reasoning about
logical formulas. I chose ????????? natural deduction method and
transformed its inference rules into equivalent refinement rules.
Subsequently, I have learned that in his later work Geotzen perform?d
this very transformation himself. Though he still thought natural
deduction was proper for presenting completed proofs. he developed the
senuent calculus as a vehicle for studying decision procedures, i.e.,
methods for finding proofs (Xleene 1952, Siabo 19693. If one considers
the programmer as embodying a general decision procedure, tentzen'a
arguments favoring the sequent calculus over natural deduction systema
apply to the domain of program/proof development. With the advent of
the technology discussed above, it is my belief that the refinement
style is appropriate not only to proof development. but to proof
presentation as well. This notion5 one step beyond Centzem's ideas5
--H31--H
Mist avait a PRL Laspiesentation for verification. If it is a valid
viev. it La applicable to more than the theory of program development;
the refinement style applies to any proof system that might benefit froa
uachine support.
2.3 The o+necifricstion Af imnerative nroera seementa
The question of correctnesa for a well specified program may ha
divided into two distinct concerns: first. that the program meets its
specification and. second. that the specification adequately captures
one's intuitive understanding of the program1s intended behavior. The
former is assured in PRL, since any executable code is always extracted
from a correct proof of the specification. The laLter, however. cannot
be guaranteed. Nonetheless. the validity of 5correct5 programs is
lieited by the aptness of their specifications. Thus. the design of a
good specification language requires careful attention to the problem of
obtainins appropriate specifications; it is insufficient that the
luguage be technically complete (i.e.. powerful enough to express any
computable operation).
There are several ways to determine the aptness of a s?ecification.
One1s intuitive understanding of the desired program behavior is often
eoat precise for a set of specific inputs. In this case. the
specification may be tested at selected points for conformity with the
expected results. The known limitations of testing (tiat only a very
small part of the full meaning of the specification is likely to be
exa?ine?) apply here. of course. An alternetive is to expreaa tbe
desired bebavior tn another form and prov? th two specIfications
-32-
equivalent. However. this not only requires substantial additional
effort. but resinds one of the philosophy of poat-developient progras
verification (`we can't get it right the first tine so let's fix it up
later5). Clearly. the point in producing a specification is to capture
fully and precisely the ideas one has in aind. with the bope that efter
careful formulation the original specification is so concise and
understandable that its correctness is evident fros a aia,ple reading.
If this hope is to be realized. the specification language ?uat permit
the easiest and noel natural (formal) expression t-f one's informal
ideas.
The execution of an extracted progras segment results in the change
of a selected set of global variables. A PRL specification describes
the way that these variables are accessed and modified. Thus. since a
specification defines a mapping from initial to final state, it Say be
viewed as a very high level progras,. However. it need not he
(efficiently) executeble; indeed. a goal of the specification language
is to separate completely concerns of correctness from those of
performance, so that the couplexity of specifications results from
correctness requirements alone (Pratt 1977).
At each point of execution the jAslt of a PIL computation is quite
simple: it is a napping from program variables to values of the
appropriate types. The neaning of a particular specification Is a
(nondeterministic) eappin?. called a :r?,.?tun. from initial to final
states. The comments used to .pecify transitions in the top down
description of prograns t?nd t? be b'gh l-?el imperative statenents.
such as 5act X se tat ...` or find the lcast Y sstiafyin? ...?. These
-33
isp?rstiwes frequently allow the specification of transitions in a mors
natural fashion than is possible ?ith precondition/postcondition
notation. For exeaple. 5increment X5 would be written
in the lstter notation with the necessary introduction of a logical
constant 1I to record the old value of X. As was noted in section 2.1.
the complete specification of tranaitions using aaaertions requires the
introduction of logical constants to guarantee the inwariance of
variables that should not be changed. In an attempt to avoid the
cuabersome task of carrying these assertions throughout proofs. I have
chosen to base the PRL specification language on an imperative notation
of generalized assignment. (As will be seen. this attempt has not
entirely succeeded. Logical constants still enter into proofs. though
less frequently. Some further approaches toward their elimination are
discussed in chapter 5.)
The assignment symbol ??? has the property that the name on the
left represents the new value of a variable while the same name on the
right represents the old value. Ta?ing advantage of this
interpretation, 5increment X5 is specified by writing CX ? X+15.
requiring that any valid refinement increment X. but change no other
variable. In general, a transition modifies the values of several
var?ables; the corresponding transition specification has a tuple of
names to the left of the arrow and a construct on the right that yields
values for each variable. Thus, 51,T ? f5A5 interchanges the values of
Z and Y.
34
In addition to c?nventiunaI aasig?ents. which define deterministic
(functional) transitions the specification language must permit the
expression of nondeterministic transitions (those that do not have
uniquely specified final states). Typically. this is accomplished by
characterizing the final state with a predicate. One might apply this
technique here by allowing transition specifications of the form
X X' such that P(x.x')
where X' is a new name that denotes the final value of X, Ny interest
in specification languages has led me to study a generalization of this
form that retains the imperative flavor of conventional assignments.
This specification notation is largely independent of other aspects of
refinement logics; I view it as an orthogonal excursion into methods of
program specification.
Nondeterministic transitions are specified by placing to the right
of the arrow a construct that produces a set of (tuples of) values,
Such a generalized assignment characterizes any plogram segment that
places one of the generated (tuples of) values in the variables. Since
set generating constructs of this sort are used in several contexts
throughout PRL. I shall digress briefly to discuss their form and
meaning.
A seneraror is a construct that evaluates to an unordered,
nonrepeating group of values. For example. a set valued expression may
be formed by placing a generator inside of the set brackets (...). All
the values produced by a generator are of the same type; the type may be
determined easily by examination of the proof text. Cenerators include.
among others. the forms:
expression denoting a single value.
expression ta expression denoting a closed range of values.
c set-expression denoting the elements of a set.
type denoting all the values of a type.
Some contexts require a generated group of values with a locally
defined bound variable ranging over elements of the group. The
construct serving this function is called an li???. It is used. for
instance. in quantified boolean formulas such as (Vx:l ? 3O)P(x).
where the bound variable x (ranging over the first fifty natural
numbers) is accessible from P(x). Though generators simply yield sets
of values. iterators may define several variables that are
simultaneously bound to distinct values. For example.
(3x:sS.y:sT)P(x.y) contains an iterator in which the pair of bound
variables x.y range over the cross product of sets 5 and T. Thus. in
general. an iterator denotes a tuple of bound variable names ranging
over an unordered. nonrepeating group of tuples of values. They
include. among others. the forms:
var : generator
iterstor li boolexp
denoting a variable ranging over
all values of a generator.
denoting an iterator filtered to
range only over valucs satisfying
a buolean eapreasion.
denoting the cross product of iterators.
iterator . iterstor
-35
One may use an iterator with one bound variable in place of a generator.
A act of small prime numbera could bc formed in this way by writing
(p: 1 ? 100 IL prime(p)).
Cenerators and iterators arc presented formally in section 3.2. My
development of them is based on ideas present in VERS2 (Esricy 1973.
Earley 1974s) and SETL (Schwartz 1975). Their preciac meaning depends
on the context in which they are used. but the abovc informal
description should suffice for the remainder of this chapter. I shall
now return to their use in the specification of transitions.
The general form of a transition specification is
varvarn			anv iterstor
where the iterator defines n bound variables and varvar arc all
distinct names. PRL is a language of pure values; it provides no
structured variables. In conjunction with restrictions on procedure
invocations this assures that distinct names arc never aliases for the
same variable. Any valid refinement of the above transition
specification must set vatvat to some n-tuple that the iterstor
would produce (if evaluated). but must not modify any other variable.
The reader may ronsider the following specifications and their informal
interpretations.
a			?? bt"8
5 to an o+¶thitr?ry clement of 5.
-3?-
x.y.z ? ax (a:ja?, btj?? c:?) it a.b.c>O A an+bnscn
Find positive values for z5y5: that
satisfy 1n.yu.5n (vithout changing n).
closure ? -ny S:?(edge) At nodes(S)Cnodes(C) A ( Ve:edae)
(e.S?( ?p:path)(first(p)-tail(e)Alast(p)hesd(e)))
Set closure to the tranaitive closure of graph G.
A transition specificetion. interpreted as a proposition. claims
the existence of sole progral that changes variables in the specified
way. Tho sspects of such a cisi. are not presented in the trsnsition
specification. bovever. They asust be provided by extending the fom of
propositions.
First. given a specification. a program might exist only under
suitable restrictions on the initial values of variables. In this case5
the proposition is written as an implication mediated by the symbol ?
(prove). as in
pr I ? n? b:eS.
In fact. for syntactic uniformity. the refineable propositions of PRL
always take the fore
h?pothesishypothesis ? conclusion
where the hypotheses are boolsan expressions and the conclusion is
either another booleam o+zprassion or a transition specification.
-38-
Second, any program implemcnting a given specification may access
only those variables declared in surrounding text. These variable
names. together with their types. era collected into an environment for
the proposition. The well-formedness of the proposition ia determined
by analyzing its hypotheses and conclusion In its environment. At the
start of a refinement, the environment is small. It contains only those
names needed to state the original problem. As refinement proceeds, new
variables may be declared and added to the environment of lower level
propositions. Alternatively, variable names may be dropped from
environments to eliminate clutter or assure modularity of the proof.
Each PRL refinement rule describes the environments of its subgoala in
terms of the environment of its goal, Thus. environments carry global
information downward into proofs with modifications at each refinement
step determined by the choice of refinement rule.
These three components, hypotheses. conclusion, and environment.
constitute each refineable proposition. They are formally developed in
chapter 3, However, the above background will suffice for an
introduction to the PRI refinement rules.
2.4			Refinement i&Lu AwL the emantie content			n?nfa
I shall now turn from the specification language to methods for
reasoning about specifications, These methods, the refinement rules,
enable one to extend the class of valid formulas from the axioms by
successively developing propositions of increasing complexity, The
rules described in this thesis formalize reasoning in the domaina of
first ordsr predicate calculus, integsr arithmetic, set theory, and
-3,-
Liperetive proarale. They are briefly discussed below. Sc motivation
for their forwal introduction in chapter 3.
Following Centzen's ideas on natural deduction syeteme (Klesne
1952. Constable and O1Donnell 1978. Prawita 1965. Szabo 1969). I have
divided the refinement rules into two classee according to their
treatment of the goal proposition: the svnthesis rules derive subgoals
from the conclusion. the analvsi- rules derive eubgoals from hypotheses.
This division is somewhat fuzzy. indeed all the rules are of equal
semantic standing and of similar form. but it aids one's memory and
provides convenient terminology.
Consider the synthesis rule for a conclusion that is a conjunction
(Asynthesis):
9 jut AAB Ig
9 jut A
9 jut 9
wbere A.9 are boolean expressions and 9 is a set of hypotheses. This
rule is one of a class for proving structured logical conclusions. In
this case. the proof of AAB from 9 breaks into two independent proofs.
that of A from S and that of 9 from 9. If these two propositions can be
refined. then the orlainal conclusion. AAB. follows from the hypothesis
set 9.
A similar rule. ?syntheais. is as follows.
___			5 ? A?B ?
S*A ? B
This allows the iMplication's antecedent to be brought over into the
hypothesis set. If B follows fro, 5 and A* then A?B follows ftc, 5.
Beside. producing composite lo8ical formulas. the synthesis rules
refine transitions specifications into iMperative control structures
such as looping and sequencing. The following example is a valid
instance of the comorule presented with other transition
refinement rules in section 3.7
? i.y l/x2 I/i lx
x?O &L Y ? lIx
&g 1 ? y*y
Corresponding to Asynthesis there is an Aanalysis rule for refining
a proposition whose hypothesis sat containa a conjunction:
S*AAB ?			lx
S*A*B &L F
where A*B*S are as above and 7 is a transition specification or a
logical formula. This rule allova one to replace the hypothesis AAB by
the two distinct hypotheses A and 5. With the remaining analysis rules.
it allows the proof of piopositiona containing structured hypotheses.
Two further examples follow.
o+.AvB a:
S.A a: V
5.5 a: I
ajpnlifi.s 3A
S.( 3xsiar)P(x) a: I ?
S.P(c) a: I
where c is a new name of type integer
The firat rule. or amalyain. peraits the conclusion that I followa fron
Aws if it follows fron A and also follows from 5. The second rule.
exists analysis, peraita the conclusion that F follows from (3x)P(x)
if it follows froa P(c) for some fixed c (of which nothing else is
1ecutable programs must be automatically extractable from proofs
of propositions whose conclusions are transition specifications. That
L5, proofs of the existence of programs must be constructive. This is
?naured by associating with each refinemcnt rule an inverse operation
that combines the solutions of the aubgoals into a solution of the goal.
Starting with the solutions of axioms, which are provided by the
5compiler5. the extraction process proceeds up the proof tree
inductively until an implementation is produced for the proposition at
the root. Though this method is intuitively clear. 1 shall demonstrate
that treating transition specifications as propositions introduces some
s?btlety into the logic and tIe extraction process. In particular. the
classical asnantica for boolsam axprassions must ha abandoned in favor
-42-
of a constructive interpretation.
Conaider an instance of ?a in which the conclusion is a transition
specification. T.
S.AAn aL T kx
S.A.B ? T
The goal describes a progran that coMputes T whenever 5 and AAB are
true. A solutico to the subgoal provides just such a program. aince the
truth of AAB guarantees that of A and that of B. so extraction fros this
rule is trivial.
Extraction from Va. however. presents problems. Choose a specific
Turing machine, N. and consider an instance of Va in which 5 is empty. A
is 5M halts5, B is 5M diverges5. end F specifies a program which yields
o+l' if tt halts and ,,O? otherwise. A. B, and F are all easily forialiaed
in soy sufficiently powerful logic (including PPI,'. Thus, one baa the
following instance of Va.
N halts V ? diverges ? x ? 1 if N halts. 0 otherwise Ig
H halts ? x ? I if tt halts. 0 otherwise
N diverges ? x ? 1 if M halts. 0 otherwise
Clearly. the first subgoal is satisfied by the simple program ?l. while
the second subgoal is satisfied by a-0. Further, the hypothesis of the
main goal is usally considered equivalent to ?. Thus, the program
extracted from the above proof should set x to 1 if N belts sod to 0 if
)( diverges. Since this argument can be built for any given )(, the
-`3.
assuaption that prograsas can be extracted froa Va leads to a solution of
the halting proble-? Theref,re. prosrana cannot be extracted fron the
above fore of Ye
The preceding argulent shows that classical logic is inconsistent
when applied to formulas having constructive neening. In particular. Va
say be incorrect when the conclusion is a statenent of the form 5we can
find a progral such that ...?. ?owever. transition specifications are
conclusions of precisely this form. Thus. if specifications and logical
formulas are to be treated uniformly in conclusions. PRL nust adopt a
non-classical approach to reasoning.
One possible approach is to replace the conventional Va rule by the
rule
S.AVB ? F hx
S.A ar F
S.fl ? F
s?AvB mL A ??fl
where Q is an obviously testable boolean expression (one that does not
involve unbounded quantifiers. large sets. etc.). Though logically
sound. this approach say require repetition at each use of AVB of the
reasoning that initially established its truth. Fnrth?r. one would
probably apply tIja rule only to the refinenent of transitions and use
the original. Issa restrictive. Vanalyais rule for refinenent of logical
propositions. counter to the desire for a unified set of analysis rules.
The alternative I bave takes is based on the relatively veil
studied area 0 constructive (intuitionistic) logic. In this approach5
one aaintains lost of the classical reasoning rules by assigning a non
classical interpretation to logical connectives, and thus to logical
foriulas. For exanpie. the iaterpretstion of AvB is that not only is
one of A or 3 true. but we can detemine ?bich one is true. Thus, a
proof of Av3 lust supply a way of detersining which alternative is true.
Including AvB as a hypothesis allows one to iaka use of the supplied
decision netbod. With this interpretation, Vs ii a valid reasoning
technique. because the decision netbod supplied with AvB provides a vay
of choosing the subgoal that gives the desired result.
I cannot lotivate and develop. in this dissertation5 elI of the
constructive logic relevant to PIL. Instead, I will siaply present an
interpretation of connectives that is appropriate. Actually, PILL is
founded on only the noat basic ideas of constructive inthematics. I
understand these ideas in terse of Coaputer Science concepts (e.g.5
co?pilation), so I will present thei in these terse. The reader
desiring a deeper understanding of intuitionise is referred to the
hibliography (Kleene l9?2. Prawitz 1963. Du-ett 1977).
The following table informally describes the constructive ee?ings
of the connon logical connectives. These leanings light he used for
informal constructive rtasoning, c.g., reasoning constructively about
PILL. Sections 3.4 and 4.2 introduce a formal interpretation for PILL
fomulas, lilicking the interpretation presented here.
let C(1). for any foriula 7. be read a. 57 j? constructively true1.
Then.
C(AAg) o+eaea c(A) and c(B).
c(AvD) seen. either C(A) or c(B) and a netbod (called the
selector) is available for deciding which.
aneana that if C(A) then c(B).
C( ?) leans fron c(A) a contradiction nay be
conatructively proven.
c((3i)p(x)) scans a value. b. nay be deternined such
that C(P(b)).
C((Vz)p(x)) scans that for any value. b. C(P(b)).
For exaiple. (Vx)(3y)(y?x) is constructively interpreted as `for any
z one can find a value y which is larger than x'. This statenent would
be satisfied by the progran 1set y to x+l".
The constructive interpretation of formulas forces the ahandonment
of certain classical truths. In particulnr. AY?,A is no longer valid
for any A. e.g.. if A is o+M halts'. because no nechnoism nay be
available for deciding which alternative is true. Loss of this azion
forces loss of the inthod of proof by contradiction. Showing that A
leads to a contradiction establishes ??A (by the definition of ?).
tnt does not assure A. since botb A and ?A could fail to be
constructively true. Abandoning these `truths' is entirely appropriate
when one is trying to constructively deneonstrate the existence of
prograss that lest specifications. A progranler is generally not aided
by a proof that the non-ezistance of the progras he is about to write
4-
implies a contradiction.
Consider. now. bow the constructive interpretations are treated in
PiLL. Each formula is justified by an object that provides the
constructive meanini of the formula. Thus, a proof of AviL yield. a
?..atjf?ca?inn that simultaneously tella which alternative is true and
provides a justification of the true alternative. A proof having AviL as
a hypothesis can only be used when AvB is constructively true. In that
case. a justification of AvB is provided as the certification of Avfl's
constructive truth. In turn. the proof may use the information
contained in the justification of AvB to produce a justification
certifying its conclusion. Thus. proofs denote ?ust,fcar?o
t?an,fnrme?a
It ehould be clear how the va rule uses the justifications for S
and AviL provided to it. The juetification for its conclusion. F. is
produced by one of the subgoala. The correct su??oal a dttermined by
examining the selector of the Avfl justification. If. say. it selects A,
then the justification transformer for S.A ? I is applied to the
justification of S end that of A (vhich also is a component of the AviL
justification). Thus. the subgoal yields a justification for I which is
then yielded from the Vs rule.
Justifications for Avi can be provided in several ways. An
instance of vaynthesis looks as follows.
5 ? Awn ?
8 mL A
This rule sieply applies the justification tranaforeer for 8 ? A to the
justification for I to obtain one for A. Then it return. a
justification for AVI that always selects A and provides the
justification for A. The rule of trichotony.
S ? x<O v x?O.
simply tests x. then yields an v-justification which tells which
alternative is true and justifies that alternative (it happens that the
justifications for relational expresaiona ere trivial. in the sense that
they need not supply any interesting inforastion).
These notions of justifications end justification tranaforeers are
further developed in section 3.?. Chapter 4 includes a recursive data
type definition for justifications which is uaed in an extractor that
?aps proofs into justification aanipulating executable prograus.
Ny ideas on extraction and constructive logic have developed. in
part. froi an early paper of Constable's Conatable 19?l) and his recent
work on P'Jcv. The latter systes has a constructive founderion which
enables proofs to be inter?reted as executable text. Constable has
developed such an interpreter on peper (Constable 1978). An
iaple:ae?tation ?f this facility. integrated into the existing PL/CV
eyetea `asy be forthcoelng.
CWtEI 3
PILS A LOGIC FOR CORsgCf PIOcw Dm1A)PKsxT
Chapter 2 motivated and introduced the lajor ideas of formal
refinement. This chapter preaents a formal eye am for program
development based on those ideas.
Sections 3.1-3.3 introduce the fundamental syntactic components of
propositions. Section 3.4 discusses the form and meaning of
propositions. the interpretation of free names in propositions. the flom
of environments down proof trees, and the constructive interpretation of
propositions. Refinement rulea for constructing proofs are presented in
sections 3.5-3.7 with examples of their use. Section 3.8 describes the
definitions and lemmas that extend the conceptual base of PRL to more
abstract notions. The chapter concludes with the presentation of rules
for checking that proofs satiafy the type and naming constraints set
down in earlier sections.
I have used severel nonstsndsrd notations in ths logic's
description. The form A where A Is any syntactic unit and 1 is a list
of names, has the same ?,snlng as the unadorned tore A. ascapt thst
attention is being brought to the possible use of the names of I as free
variables in A. There may be other free variables in A and not all
names of a need o+?c?or free n A. TI?is device. though of no formal
-49-
significance. is useful for communicating the intent of various
constructions presented below. The coimnon notion of substitution is
vrjtten A?e vhere e is a list of formulas to replace all free
occurrences of corresponding names of I in A. Again. the names of x
need not occur in A and. if they do. only the free occurrences are
replaced. There is an important restriction. called abaencs ? canturs
that a substitution ii valid only if no free name of e becomes bound in
Thus. the meaning of e in the substituted form is identical to
its mUning before substitmtion. The refinement rules later in this
cbspter are applicable only iben this condition is satisfied. The
dettrmination of free and bound variables for the syntactic forms of Psu
is informally explained witb the introduction of each form; it is made
precise in section 3??
3.1 Tyn.. and P?nre.a,n?a
An expression is a structured formula that naps each possible
execution state into a single value. Evaluating an expression never has
any side effects on the state this makes the semantics of expressions
tractable in particular. it guarantees the validity of such common
algebraic laws as the comietativity of addition. The criterion of an
understandable and readable specification language would be bard to
satisfy without these widely known properties.
The values produced by expressions are divided into an infinite
number of types: booleans. integers. and a variety of sets. Booleans
and integers are atomic types whose values may not be decomposed. Sets
-50-
of type AA?(T) are unordered. nonr?peating. finite collections of values
of type T. where T is integer or another set type. but not boolean (for
technical reasons that are explained in section 3.6). Thus, boolean and
integer are base types and set is a type constructor. The names for
types may be generated by the following context free grammar,
type ?			element type
etement type			I in ( element type )
Each type bee forms for denoting constants and operators for
combining values. The operators are defined only for operands of
certain types; they yield precisely typed results. The table below
enumerates the methods for forming expressions. Within each type. the
operators are listed in order of decreasing precedence (e.g.. A binds
tighter than v), Assume throughout that i.j era integer valued
expressions. A,B era boolean velued expression?, T is an element type
name. R,S are ?(T) valued expressions. and a is an expression of type
T. Finally. individual variables are free when considered as complete
expressions and the free variables of composite forms are those of the
components. unless stated otberwise.
-31-
IMtIGw
typet in
valuest			....			-2.			-1.			0.			1.			2.
basic format			..., 2. --H1. 0. I, 2. ...			constanti
variable name			tbe current value of
the variable
definition reference			the value returned from
an instantiated
definition (further
explained in 3.8)
product
sun. difference. negation
composite forms: itj			in
i+j. i--Hi. --HL			in
mt--Hlist relation mt--Hlist
relation o+.. relation jut-list hool
where each relation is one of -. ?. <. ?. ?. ?
end each int-liat is a list of integer valued
expressions separated by coemas. This is
logically equivalent to the coniunction of
the binary relations formed between each
element of adjacent jot-lists. ?or example.
l?i.j<k.l?n means lSiAlSjAl<kAi<lAj<k?I<lAk?nAl?n.
-52--H
BOOLFANS
type: honi
values: ? li1a
basic forms: ??. LL1iL
variable name
definition reference
composite forms: ?,B			bool			negation
(? iterd)Bd ?			bool			eiistential quantificatiom
(Viterd)Ba			bool			universal quantification
The notation iterd is defined in section 3.2.
It represents an iterstor that defines the nesea
given by the name list d. The free variables
of these fonna are those of the iterstor together
with those of not appearing in d. Free
occurrences in of na?es of a become bound
in the complete quantified expression.
h??:			conjunction
Av3			? bool			disjunction
A?B			? bool			implication
A?B			+ ??			equivalence
A?l ?tsns A?B and it is treated this way. but
e?uslity is always writtsn O for boolean operandi.
g?TS
types ?(T) (for any given element type T)
values: all finite acts 0 elements of type v
basic foresa: ?(T)			the empty set of type flL(T)
( generator ) the set of elements produced by the
generator. The free names are those of
the generator. The generator must be
automatically evaluatable (defined in
section 3.2). hence5 tbe set finite and
easily coeputed.
variable name
definition reference
colposite foris:			?(T)			intersection
?(T)			union
1-s			?(v)			difference
n?			nunber of elements (size)
ass			bonS			element of
buol			not element of
set--Hlist			relation set-list
relation ... relation set-list
where each relation is one of -. ?. c c and
each set-list is a list of set valued expressions
separated by comsmas. For example. RA?.:c?s
is a fact about union and intersection.
In the present (ormulatton. sit espressions are total functions.
i.e.. they are defined for any ,hotcs of input values. This simplifies
the logic since the well-formednes. of expressions is reduced to the
question of type correctoess. rather than requiring more general
reasoning shout tie properties of poseibly undefined compntstions.
Though this restriction rules out many useful partial functions. such as
integer division. it does not hinder presentation of the essential ideas
of PRL. Nonetheless. as this is a central concern for any practical
logic. I have spent significant effort toward finding a pleasing
treatment of partial functions that introduces the least additional text
into proofs. I have not yet found a satisfying solution. but my
thoughts and some directions for further research are presented in
chapter 5. The P'JCV project has considered several solutions to this
problem in their programming logic (Constable and O?tonnell 1978).
With the type restrictions presented above. the types of all
expressions may be statically determined. Illegnl expressions are
forbidden from specifications and proofs by easily applied type checking
rules. The envisioned program development system performs this checking
as proofs are interactively produced so that all intermediate
developments are assured type correct ?ithout any programmer assistance,
A more flexible type system. e.g.. allowing heterogeneous sets through
union types or a typeless semantics. would require the introduction of
proof text to show the absence of type errors. Such a system might be
appropriate if one had a general approach to handling errors as called
for above. but it is inconsistent vith the present philosophy of
treating only non-erroneous expressions.
--H`s-
3.2 Cenera?prs amA 1?era?pra
Nany PAL constructs are fossed from coeponents that represent
groups of values. for exampla. sets are formed by placing braces (...)
around such a component. These coaponents are called eenerators As
discussed in section 2.3. each denotes an unordered. nonrepeating.
possibly infinite collection of values of a single type. Generators are
total. aide effect free mappings from the state whose types nay be
atatically determined. I will formally present then shortly.
A related construct is the iterator also introduced in section
2.3. in which a tuple of variables (the hound variables) ranges over an
unordered. nonrepeating. possibly infinite collection of tuples of
values. Each bound variable of the iterator has a specific statically
determined type. but no relation is assuned between the types of
different variables. The context of an iterator determines both the
scope of its bound variables and the use of its collection of tuples.
(For exanple. in the universally quantified formula (Vd:l tg 50??d5 the
iterator?s scope exte?ds over the quantified predicate. The truth of
the formula is determined by evaluating the predicate many tines with d
bound to each successive generated value.) An iterator that.binds a list
of variables x is written iterX. Thus given S of type aAL(T).
(?x.y:?S.R:cg)... contains an iterator. ????x.ysR providing the nanes
x.y.R of types T.T.?(T) that range over all tuples fron SxSx2?.
In any logic of sets or quantified expressions. some decision must
be made about what may be written inside of set braces or after the
quantifier. Conventionally. the choice is to rEquire a name and a type
-5'.
vith an optional restricting predicate (thws. (VdIinL)fld or
(d:jnL 11d1? 1 have chosen to explore am extended notation for these
constructs for two reasons. First. it is important that the prograning
system supporting FILL be chIc to evaluate expressions sutonstically
whenever possible. This task is simplified if one can easily express
varieties of bounded quantifiers. bounded set formers. etc.. because the
system can then determine by syntactic examination whether a construct
is autonaticelly evaluatable (more below). For example.
?,(3x:2 ? p-l)(3y:l LI p)(p-x*y?
is computationally wore tractable (to a simple automatic evaluator) then
?( ?x.y:?)(l<x<p A l?y%p A p-xty).
Second. I have long been intrigued by Earley's work on iterators ?Earley
197451. He seems to derive a great deal of expressive pover from these
sorts of constructs. in particular from pattern matching facilities.
Though FIL iterators are very limited in comparison to his ideas. I
wanted to begin developing a feel for them. One option for later
research is to increase the power of the specification language by
extending the class of iterators.
Let us now examine the methods for constructing iterators and
generators. An iterator, iter . nay be formed in four ways.
x : generator binds the names of x with a set of tuples in
which each name of x takes on all the values of the
generator. The free variables are those of the
generator. For example. `i.j:l ? n5 yields n2 tuples
?here n is a free variable.
?7-
iterx i? ?x hinds the naees of a wit tit.) aubset of the
tup1?s of iterX that satisfy tI?e predicate. The free
variables are those of lterX together with those of B
not?appearing in x. For example. 5pt? IL
? itiAL)(p?dsl?r)" yields an infinite ctass of values
for p that satisfy p no? dr for (given) free d and r.
iterz for iter7 binds the names of x with the set of tuples
7
fomed by unioning the sets of tuples produced by iterX
y
for each assigonent to y yielded by iter7. The free
variables ate those of iteJ together with those of iter1
y
not appearing in y. For example. 5m:esons(n) for
n:ecnrrentnodes5 produces the name I end the set of sons
of all tbe current nodes. The only free name is
current?odes.
iter7 . iter1 (where x is y concatenated with z) binds the
names of I with the set of tuplee forned from the cross
product of the tuplee of ????? with the tuples of iter1.
The free variables are those of iter7 together with those
of iter1. For example. 5S:sstart?states.
f:sfinal_states5 produces the set of ell pairs of
starting and final states.
The generators are sore easily described. (Though 1 shall use the
tam `set of values' to describe the result of evaluating a generator.
this is a distinct notion frota the set expressions described in the last
section. Cemarators snat be enclosed in set brackets to produce
-`8-
directly asnipuletable values.)
type generates the set of values of the type. Thers are no
free variables.
exp generates the singleton set containing the velue of the
expression. The free veriablee are those of the
expression.
exp ? exp (where both are integer ?slued) generates the set
of velues in the inclusive range fron the first to the
second expression. The fres variables are those of both
expressions.
sub exp (where sub is e. c or c and exp is set valued)
generates the set of elements of exp. strict aubsets of
exp. or subsets of exp. according to the choice of sub.
The free variables are those of the expression. ?or
example. (?s) is a set valued expression that represents
the powerset of S.
iterx (where x is a single name) generates the set of values
yielded by the iterstor. The free variables are those of
the iterstor. ?or example. 5p:iaL it prime(p)5 generates
the collection of prime numbers.
gem? for iterx is similar to the use of L2L in iteratora.
It generates the set of values formed by unioning the
sets produced by genx for each aaaignment to x yielded by
iterx. The free variables are those of iterx together
5?
witb those of gen? not appearing in x. For example.
`n2 f? n:1 ? 50' produces the first 50 positive
squares.
gen ; gen generates the set of values formed by unioning the
sets produced by the two generators. The free variables
are tbose of both generators. For example. (l;2;3J is
the Bet containing I, 2, and 3.
pro?ing properties of constructs containing iterators and
generators requires a more fornal characterization of the values
produced then given above. This cbaracterization is provided by a map V
from iterators to predicates -- V(iterX) yields a predicate on names of
I (among other free variables) which is true exactly when the values of
I are some tuple produced by iter'. For example. ?(i.j:l ? n) is
l?i.jSn.
V is defined inductively on so extension of the syntactic class of
iterators. The extended domain includes the form exp-list:generstor in
addition to the various iteratora. ?ach form of iterator. including the
various forms of exp-list:generator. is handled as a distinct clause of
the definition. This enlarged domain increases the usefulness of V;
however. it does not modify the class of legal iteraturs.
V : extended iterstor form			?			predicate
Cap???n ` gen			V(exp1?gen)A ... AV(exP?:gnn)
exp type			??, the extended iterator cannot
be legally forand otherwise.
This sort of type information
-60-
sip I sip'
sip I sip1 La sip2
sip I sub sip'
sip I iteri
exp I gen? for iter'
sip I gen1 3 gen2
itor ? 5
iter for ?????
is carriad in the environlents
discussed in section 3.4.
expexp?
sxp1ceipsexp2
sip sub exp'. where sub is 5'. c. or c
V(iter') since exp is produced
by iter1 exactly when the
predicate cbaracterizing iter'
holds with exp s'?h?tit'jted for I.
(??????)v(??p?gen__). where
___			iter
is iteri with a change of
bound variables from x to y.
(y nust not occur in exp. gen.
or iter1.) This name change
is needed since exp is placed in
the scope of the iterator.
Any free occurrences in exp of
variables of x must not be
captured by the eiistential.
For example.
V(n:(msucc(n) for n?emsrked)) is
is ( 3y?emsrked)(n?succ(y)).
V(exp?gen1)vV(exp:gen2)
V(itsr )AIx for rxampls
V(a:--HS li aso) is a5'SAaSO.
3 iter?)v(it?r?). for ?xa?ple
--H.?` (u)) j? nL5'?rked)
te ( 3n:?nsrknd)(naxt?succ(n)).
itsr? , jtsrz			V(iterY)AV(itsrZ)
(Iota: Though the syntax of lt?rators and generators is ambiguous (the
precedence of operators is not specified). all choices of parentheses
produce extensiunsily equivalent ?redicatea according to V. Since the
seaning of these constructs is formally defined by V alone. the
ambiguities are harmless.)
The inclusion of the form 5type5 for generators permits the
expression of unbounded generators and iterators. The complete proof of
a transition specification will eventually refine away any use of
unbounded iteration, so that the ayatem can extract a program that is
guaranteed to terminate. (This restriction is needed only because the
extractor is very limited -- eany tranaition apecificatioos using
unbounded iteration do characterize terainating programs.) Thus, though
proofs say reason about forms whose values are not obviously computable.
b7 the tise refinement reaches the leaves of a proof only easily
coaputed forms remain. This property of being easily computed is called
utosat?ratlv evai"?tahIe, ahbreviated a.e.. It is defined as follows.
Def An expression. generator, iterstor, or
transition specification is a-a iff it
does not contain any generator of the form 5type5.
It is a purely syntactic question whether a construct is 5.5.. Tn
particular. though boolean expressions are not a.e. if they contain
unbounded quantifiers. integer and set valued expressions are always
-62-
a.a. as may hn 5 I?y x (uteg s.ct I?n 3.1. (See sect ion ?.8 for
treatment of definit un rrf?r?'nr?s.) Tus,
(p:l ?o 50 si (Vk:?)(k divides p ? k?lvkp)J
is not a legal set expreaaion. This is the technical meaning of the
remark, in s,cticn 3.1. tat setc are finite and easily computed. The
elements of an a.e. generator can be enumerated by a straightforward5
though inefficient. algorithm. so all sets can be computed.
The characterization of iterators by predicates necesaitates a
restriction on the use of namea for bound variables. Consider the
iterator x:x. presumably meaning that bouud variable I rangea over the
single current value of free variable x. V characterizes this iterator
by xx, thus losing the distinction between bound and free variables.
The usual sort of solution would resolve this naming conflict by
uniformly renaming bound variables throughout their scope. ?owever, as
V generally does not have access to the entire scope of variables
defined by iterators. a reatriction is made that insures no name
conflicts will occur. Thus.
no bound variable name of any iterator may
occur as a free variable of that iterator.
This restriction may be formulated by cases:
I) in x:generacor no variable of x may occur free in the generator,
2) in iter1 for ????? no variable of y may occur free in iter15
3) in iter?5ite?I no variable of y may occur free in iter5
and conversely.
Thus, a:o(a;b), a:a, (a:'sS, S:st), and (b:a jt a+lO) for a:b-lO ? b are
-53-
atb--HlO ? b are legal. In practice. this restriction is of little
consequence since UCIC conflicts can be easily avoided by the
progran-er. Checking for conflicts is essential. however. This is part
of the static analysis described in section 3.9.
3.3 Transirio snecifieatin?s
The major purpose of P%L is to persit expression of the
specification and refinement of programs. As discussed in section 2.3.
the only visible effects of the programs considered are changes to the
values of globally declared variables. These restricted programs define
nondeterministic nappings (relations) from initial to final state. where
states are simply associations of values with variable names. As there
are no structured variables and no discernible sharing of representation
by values. the logic for reasoning about values and assignment is
straightforward.
The general fors of a transition specification is
va?liet ? anv iter'
`rhere x has the ease length as var-list. This aeans that the var-list
asy be set to any tuple of values produced by the iterstor.. After
execution of the transition specification (or its refinement). the
values of var-list satisfy the predicate
V(iter?)var?1ist.1 * var0-list.vsr-list
where vsr0?Iist is var-list with each va?iable v replaced by v0. This
predicate relates the current values of var-lieL to the values of the
variables before they were changed (var0-lis?).
The above transition form is used in formal description and
analysis of the logic. However. in specification. aucb as i an, iriti
and I ? lax b:aS. it requires the introduction of seaninalass bound
variables. Therefore. when writing specifications there are two
additional acceptable forms:
va?list ? lax gen-list
and var-list ? lax gen-list1 L2L iter1
Also. the word lax nay be dropped if desired. e.g.. if the generators
are single valued. These forms are interpreted as
var1var0 lax var15:genvar05tgen0
and			varvar0 ? lax (vsr;:aen1var?S:gen0) fror iter15
respectively. where the var? are new variables. Thus5 i ? 2ai and
I ? lax Is are legal abbreviations for specifications.
There has been a constant tension between my desire to eliiinata
unnecessary auxiliary names from specifications and the need to keep tha
reasoning rules simple. Although auxiliary nanes have been largely
removed from specifications. they are generally re-introduced in the
refintetot text. I am not aware of any satisfactory method for
.In? ab??t vari?birs that avuids tija difficulty. !desl!y. the
logic utuld allow dit?ct algebtaic reasoning about transition
spec?fltatfuns. boat th?ttglts in this direction are presented in
chapter ?.
3.? ??1li?1L. atnttt1ac?ie. AwL Jjia???j???
A propos?tion. of the form hypothesis-list ? conclusion. is a
clais that some conclusion follows from certain hypotheses. The
hypotheses are boolean expressions that characterize the state of the
proposition's free variables. The conclusion is a boolean expression
tbat is claiaed true or a transition specification that is claimed to
apecify a computable mapping from state to state.
The propositions" of a hypothesis-list are necessarily written in
some specific order. ?evertheless, they are interpreted as lacking
order, in that they say be freely re-ordered as desired. ?any
refinement rules single out a specific hypothesis for manipulation, for
example.
S.AAB ? c k?
concerns the con?unction AAB. These rules nay be used even when the
selected hypothesis is not last in the hypothesis-list, without explicit
mention of the require? re-ordering. This essential informality entails
a slight complication of the extraction process.
The discussion of top dowr development in section 2.2 recommends
that `seaning be assigned to propositions without regard for surrounding
context, so that refinement validity is a local property of proofs. In
order to achieve this, it is necessary to associate with each
proposition an environment describing the types of all accessible global
variables. If a proposition references other variables, or is
incoipatible vith the types of the variables it does reference. then it
is considered ill-forsed.
-66-
InrurporatJ?g en?i???s int? pruufs ?stenAs the form of
propositions to
<env> I?yputhesia-Iist ? conclusIon
whers eny Is a s?t of 5n r!typu" pairs. for xampla.
<x:? S:?(?)> ? ? anv b:eS.
The environment of the outermost proposition cf a proof is formed fron
global variable declarations of the form ?? name:type5 (definitions
and lemmas are also introduced at this level). This initial environment
is then modified according to the refinement rules as it flows down the
proof tree. The acceptable refinements are those whose subgoala are
well-formed with reapect to their inherited environments. Thua, the
validity of a proof may be assured by checking that each refinement step
is legal according to the rules of the next few sections and that each
proposition is well-formed according to the rules of section 3.9.
I shall often omit the environment clause from propositions
occurring in examples since the examples are usually simple and the
environments obvious. Nonetheless. during development of proofs with
machine aid I expect that environments would be at least partially
displayed. as they provide information essential to correct refinement.
As explained in section 2.4. the interpretation of propositions is
constructive in that a justification is associated with each proved
boolean formula certifying its truth. A proof of a proposition denotes
a method for transforming justifications of its hypotheses into a
justification of its conclusion.
-67
Tne choice of precisely what information to carry in justifications
is determined by how the justified formulas are used in the proof rules.
The Va rule of Cection 2.4 demonstrated that an v?jostificstion must
include a selector telling which alternative of the diajunction is true.
The remaining varieties of justifications have been similarly developed.
I will present them informally below. Section 4.2 supplies a precise
discussion of justifications sod their properties.
Some boolean expressions need no justificationt the extraction
process requires only that proofs establish their classical truth. I
will say that such an expression has no ? const?uctive meanine or
that its justification is trivial. Arithmetic relations. for example.
have this property.
Transition specifications do need justifications. because after a
transition is executed. the chan?ed variables are supposed to be related
to their old values by a constructively true predicate. The extracted
program for a proposition of the form 5 ? X anv iter uses the
justifications of the formulas of 5 and the current values of the free
variables to compute new values for x and a justification for the
predicate V(iterd). That is. in addition to perforaing the tranaitiQn.
the extracted program provides a justification for a specific boolean
expression. If one lets x represent its own values before the
transition and d represent xts values after the transition then V(iter )
describes how the new values relate to the old values. Though this
justification nay appear unusual. it carries precisely the information
needed to permit extraction.
-68-
The justifications for each kind of formula are enuserated below.
Note that those for the logical connectives mirror the constructive
interpretations presented in section 2.?.
syntactic form: is justified by:
AAB a pair (justification for A.
justification for 3)
AvB a pair (selector.j) where if selector
is o+left5 then j justifies A.
otherwise j justifies 3
A?3 a justification transformer which maps
justifications of A into those for 3
A?B a pair (justification transformer for A?B,
justification transformer for ?A)
the trivisi justification. since a
demonstration that 3 leads to a contra-
diction provides no constructively useful
information
(?iterd)B? a triple (value. justification for
V(iterd). justification for 3d?'
where d-value satisfies V(iterd)ABd
(Viter ?td ? justification transformer that maps pairs
(value of d justification of v(iterd))
into justifications for 3d
x anv iterd a justification for v(iterd)
the trivial justification (hut note that
a j'?stification for ?1li will never
-69-
actually be used because LA1u can
never be proved true)
boolean variable the trivial justification (but see
section 4.2)
boolean definition
reference
eiP,set-exp
ex?o+aet-exp
int-exp relation
... Int-exp.
set-eap relation
... set--HsIp
(see sections 3.8. 4.2. 4.6)
the trivial justification (for reasons
explained in section 3.6)
the trivial justification (it is
equivalent to ?,(expsset-exp))
the trivial justification, but recall
that conpiex relational expressions are
treated as conjunctions of simple ones,
e.g., lSi.jsn neens l?itnAlSjcn,
Extraction is ?n inductive process. in order to carry it out. for
each refinenent rule one must be able to construct a justification
transformer for its goal from those extracted from its subgoals. This
means that a description of the justifications chosen for each formula
is really an inductive property characterizing extraction. if the
description is too weak. the subgoals will not provide enough
information. if the description is too strong, the goal will require
too much information. The reason for choosing the above varieties of
justifications is that they work.
-70-
3.5 Refj?eaent loeical rules
The logical refinenent rules describe the analysis and synthesis of
boolean expressions. the use of substitution. and other fundamentals of
the proof system. The analysis and synthesis rules are a variation of
those presented by Centren in his development of natural deduction
ayatems and the sequent ca?culus [Kisene 1952. Constable and O5Donnell
1978. Szsbo 1969]. In particular. recall fross section 2.4 that proofs
are trees. the aubgosls of a goal are independent propoaitions. and
there is no implicit flow of information between subgoals. Thus. the
ordering of subgoals in the refinement rules is of no significance.
Let Ai 8 be boolean expressions. C be any conclusion5 and S be a
list of boolean expressions (representing a set of hypotheses)
Consider the rules for composite boolean expressions. These rules are
named by the operator to which they apply suffixed with 5a5 or 551 for
analysis or synthesis. respectively. Unless stated otherwise. the
environments of subgoals are the same as that of the goal.
?			S.A1AA2 ? C ky
S.A15A2 ? C
?			S ? B1AB2 ?
S ? B1
?
The rule of Aanslysis allows splitting hypothesis A1AA2 into its
components for further separate analysis. The corresponding synthesis
rule allows combining independent conclusions ?? B2 into ?lA?2
S.A1V? ? C ?
S.A1 ? C
S.A2 ? C
--H71--H
s ? B1vB2 If			s ? 31V?2 If
S ? B1			also			S ? B2
If C may be proved from S.A1 and from S.A2 then it may be proved from
s.A1w? by wanalysis. The justification of A1VA2 deternines which proof
of C is used. Conclusion 131vB2 ?ay be proved by establishing either B1
or B2 and using the appropriate form of veynthesia. The justification
for ?1vB2 depends directly on which form of veynthesis is used; other
rules for synthesizing diajunctions. e.g.. trichotomy. produce more
complex justifications.
?a S.A1?? ? C If
s ? A1
S.A1.A2 ? C
?e S ? B1?B2 If
S.B1 ? B2
Tbe first rule allows the splitting of bypotbesis A1?A2 into A1,?
given a proof of A1. The justification of A2 is obtained by applying
tbe justification of A1?A2 to that of A1. The second rule allows the
antecedeot of B1?B2 to be treated as part of the hypothesis-list. The
justification transformer extracted from the aubgoal is applied to the
-72-
justification of S. but not applied to that of B1. This leaves a
transformer that juatifies 31?B2.
a			s ?B ? false ?
S ? B
s			S ?			bg
The ?analysis rule says that a contradiction arises if S entails B.
since botb ?? is provable5 and 5from a proof of ? a contrsdiction may be
derived5 are then true. The ?synthesis rule allows the conclusion
5from a proof of B a contradiction may be derived5.
As mentioned in section 2.4. one should note that
S ? B ?
S. ?t false
is not a refinement rule. It is classically valid. but the subgnal does
not provide any information on why Z is true. only thst ?B is
inconsistent with S. It is not generally possible to produce a
justification for B given only justifications for S and a proof of the
suhgoal. Thus. this rule is not constructively valid and is not present
in PRL.
?a S.A1?A2 ? C bg
S.A1?A2.A2?A1 ? c
-73-
S ? B1?B2 Ig
S ? B1?n7
? ?2?B1
These rules capture the obvious relationship hetw?en equivalence and
jiplication.
The rules for quantifiers are somewhat more subtle; they deal with
new nases, changing environneat,, and suhatitution.
<env) S.(Yiterx)Bx ?? c ?
<env> S ? V(iter?)?exp
<env> S.(ViterX)?.B ? c
I ?exp
where exp is s list of a.e. expressions of
the same type in <env> as x (in iter1) in <env>
The Vanalysis rule allows introducing an instantiation of B into the
hypothesis-list for any evaluatable expressions that satisfy the
iterator. The use of V in the first aubgoal is a metanotation, like
suostitution. that disappears in any actual use of this rule. For
ezaeple.
(Yx:ja? li prise(x))( ?iprime(x+7)) ? ?prime(y) kx
? primeCy-?)
IL priae(x))( ?prime(x+7)).?,prime(y-7+7) ? ?prime(y)
inatantiates ?prise(x+7) with y-7 for x. The justification of ??exp
is derived from the first subgosl and the justification of the
univeraslly quantified hypothesis.
-74-
<efly> s ? (Viterx)Bx If
<env.d:T> S.V(iter?)?+?? ?
where T is the type of I (in iter1) in <env>
and d?<env> (if x is a list of names then
Interpret T and d accordingly)
This allows the conclusion of a universally quantified formula if the
formula can he estahijehed in an environment where the hound variables
are free (and thus implicitly universally quantified). The change of
names is needed since names of x may occur in <env>. The justification
of the conclusion is a method of providing a justification of B for any
x satisfying the iterator; this ia precisely what is supplied by the
proof of the subgoal.
<env> s.( ? iterX)B1 ? c ?
<env,d:T> S,V(iter1)??.B? ? c
where T is the type of I (in iter1) in <env>
and d?<env> (if I is a list of names then
interpret T and d accordingly)
3analysis allows one to assume the availability of a value for each
name of d that together satisfy the existential. These values may be
used in the proof of C. The needed values and justifications for the
hypotheses of the subgoal are provided by the justification of the
existential. As with vanalysis. this rule illuminates the need for
constructively interpreted formulas when one considers that C asay
represent a program hasing its calculations on the value of d.
--H75--H
IL			<env? 9 ? (? iterx)Bx bat
<env.d:T> 5 ? d			?a? iterx AL
where T is the type of I (in iter1) in <env>
and d#<env> (if x is a list of names then
interpret T and d sccordingly)
This rule introduces a new variable list. d, and permits the stated
concluaion if one can develop a program that sets d to appropriate
values. Thus. an existentially ?uantified formula may he viewed as a
device for packaging a computing mechani&m and sending it to other parts
of the proof. The justification for the existential formula is built
from the justification of the transition specification. As the
existential must provide both a list of values and a justification of B
for those values. so must the justification of the transition
specification. Therefore. rules for refining the latter must permit the
extraction of both code and justifications describing how calculated
values satisfy their iterators. For example. extracting from a proof of
j snv i:.? AL prime(i)vprime(i+l)
must yield code for computing j and a justification telling whether j or
j+l is prime. Such a proof would allow synthesis of the conclusion
3 i:ji??)(prime(i)vprime(i+l)).
The next set of rules describe some fundamental properties of the
logic. They need no refinement for their validity and may he thonghr of
as axioms.
-76-
AlL			S ? rfl?e
lAin AlL			&L
xcluded middle S ? Bv?fl
where B is an a.e. boolean expression
S.B ? B
_ AlL
S ? exp1xexp2			?,(exp1?exp2)
The false definition rule has the interesting property that since one
can never be presented with a justification of truth of the hypothesis.
one need not be concerned with producing a justification for the
conclusion. The excluded niddle rule is quite useful in conjunction
with vanalysis when the cases are determined by the truth value of an
sutonaticelly evaluateble boolean expression. The ? definition rule is
a logical (rathcr than. asy. integer) rule Lecause equality and
inequality are applicahie to any pair of expressions of li?e type.
--H77--H
consenuen?P			<env> 5 ? C ?
<env> 5 ? B1
<env> S.B1 ? B2
<env> S.BBn?l ? Bn
<eny> S.BBn ? C
The rule of consequence permits the joining of sequential proofs into a
cosposite whole. The justifications flow from the initial hypotheses.
5. through the subgoals in sequence to produce a justification for C.
snecsI'z???n			<env> 5			? C			?
?exp			?exp
<env.x:T> 5 ? C
where exp is s.e. and T is the type of
exp in the context of <env> (if exp is
a list of expressions then interpret
T accordingly)
The specialization rule allows the replacement of free variables x in 5
and c b7 any s.e. expressions of appropriate types. Such a substitution
is permissible since if 5 ? holds for any tuple of values. then
surely it bolds for the particular values of exp. In the case that C is
a boolean expression. the same effect may be achieved by synthesizing
(Vx:T)(5?C) fro. 5 ? C using Vs and then analyzing it using Vs with
ezp replacing I. However. this separate rule of specialization is
needed if C is a transition specification. because 5?C would be ill-
-78-
formed.
As an exanple of logical proofs, consider showing that
?,(exp1?exp2) ? exp1-exp2. This holds in general. if the expressiona
are a.e.. as follows.
?(exp1?exp2) LLL exp1-exp2 ? consequence
?(exp1?exp2) ? exp1=exp2v?,(exp1=exp2) ? excluded `aiddle
?(exp1?cxp2).exp1-exp2v?(exp1-exp2) ? exp1-exp2 ? Va
?(exp1rexp2).exp1-exp2 ? exp1=c1p2 kx assu?ption
?Cexp1?exp2).?(exp1-exp2) ? exp1eIp2 lIt consequence
? exp1xexp2 lIt consequence
? exp1?exp2??,(exp1-exp2) lIt ? def
.,exp1texp2??,(exp1exp2) ? exp1xexp2 lIt ?a
...,exp1?exp2? ?(exp1-exp2). ?(exp1-exp2)?
exp1?exp2 ? exp1texp2 lIt ?a
....exp1??xp2? ??(exp1-exp2)
?i(exp1=cxp2) lIt assumption
.exp1?exp2? ?(exp1=exp2).
exp1?exp2 ? exp1?exp2 lIt assuaption
.exp1?exp2 &g false lIt ?s
o+exp1xexp2 ? exp1?exp2 lIt ass?prion
exp1?exp2.li1L? ? axp1sexp2 lIt false def
--H79--H
The final set of logical refinement rules deal with equality. The
properties of reflexivity. symmetry. and transitivity are captured as
follows.
refip-ivity			5 ? exp-exp
aL exp2exp1 ?
5 ? exp1-exp2
transitiwiry 5 ? exp1-exp3 ?
5 ? exp1-exp2
5 ? exp2-exp3
These rules spply to all types of expressions (recall that equality for
boolean expressions is written ?). Since no ill-defined expressions
can appear anywhere in Pitt. there is no need to mention well-definedneas
in the reflexivity rule.
The fourth equality rule provides for the substitution of equals.
substitution 5 ? c
xeexp1			xeexp1
5???xp1 ? exp1=exp2
5 ? c
?exp2			x+?exp2
This means that to prove 5 ? C one may establish exp1eexp2 from 5 and
then show S' ? c which ia obtained fron 5 ? C by changing aelected
occurrences of exp1 to exp2. Note that x ja used here as a etricke to
-80-
allow selective substitution, but (unless it happens to appear in CIp1
or exp2) it does not actusily occur free in the hypothesis or
conclusion.
With each refinement step of proofs, I sball sometimes write the
name of the rule used and other relevant annotation immediately after
the word ?, The following proof schemes, presented in this atyle, show
that substitution is powerful enough to encompass symmetry and
transitivity.
derived symmetry:
S ? exp2-exp1 lv substitution where C is 5exp2,x"
S ? exp1=exp2 lv
>proof required
S ? exp2-exp2 lv reflexivity
derived transitivity:
S ? exp1--exp3 lv substitution where C is 5x=exp35
S ? exp1eIp2 lv
>proof required
S ? exp2-exp3 lv
>proof required
Despite these reductions, the rules of symmetry and transitivity
are retained. because therr is no sufficiently general facility in PRt
for introdtcing drived proof rules. The lenmw ncchanis,, of section 3.0
provides some abi!ity to c?tc?d tbe lo;?r but it is nc poverful
-81-
enough. An effective solution to this prob?t? that showed the
introduction of derived rules and hints on tbeir applicability (perhaps
along the lines of LCY aetalanguage [Cordon et. el. 1977a)) would permit
aore conpact proofs. It could gradually lead to the semi-autonetic
generation of proofs according to user developed strategies.
3.6			s,frln?enr			nte?ers ? sets
The theory of integera. though of great practical inportence. does
not abed such light on the issues considered in this thesis. Therefore.
such of the theory is contained in a general rule that permits any valid
inference about aisaple arithietic relations. Several additional rules
capture the reisinder of the theory.
An arithietic relation is 5exp-list relation exp-list relation
relation ezp-liat5 or its negation. where all expressions are integer
v.lned and the relations are -. X. < t >. ?. The rule
.??rh			S.BBn ? C
where C is an arithnetic relation that follows
fros arithietic relations BBn alone
according to sone reasonable axiom aystem
provides for the introduction of 5intuitively obvious5 reasoning steps
without further explanation. In an implenentation of PRL this rule
wonld probably be brolen down into nore easily verified rules. However.
as arithmetic relations have no deep constructive meaning. the
extraction technique of chapter 4 depends only on the validity of these
-82-
inferences. not on their dQ?p structure. Accordingly. a mechanis? is
postulated capable of checking arithmetic inferences and further levels
of refinement are safely ignored.
In addition to the above rule, one needs to be able to prove
diajunctive conclusions. The following tbree? rules provide this
ability. I have separated them from the general rule because mom-
trivial justifications must be produced for their conclusions.
trichotomy S ? exp<O v (expo v exp>O)
where exp is an integer valued expression
S.exp1sexp2 ?LL exp1<exp2 v exp1sexp2
where exp1 exp2 are integer valued
expressions
c? S.exp1?exp2 ? exp1-exp2 v exp1>exp2
where exp1, exp2 are integer valued
expressions
The justifications for conclusions of these rules are easily obtained
since the expressions are integer vslued, hence s.e., Deciding which
alternative of a disjunction holds is simply a matter of evaluating the
expre?sions and performing a comparison or two.
The PtIcv project has developed a theory of integera and an
implemented set of reasoning rules that are quite powerful (Constable
-83-
and O?lonnell 1978. Cnam 1978). Thougb the rules are organized
differently from those above. they include an arithmetic rule (similar
to aritb) peThitting significant deductions to be made in one step. The
well studied PWCv rules and their implementation. modified to produce
justifications for disjunctive conclusions. could be used as a
reasonable theory of integers for FRL.
The set tbeory I have developed is simple. Since sIl sets are
finite and easily computed. the set theory axioms are easily shown
consistent by construction of a model in which they are true (see
chapter 4).
Though a theory of infinite sets is of considerable interest. it is
also difficult to develop. I have chosen to stay with an easily
axiometired theory for the present development. Constable bee been
vor?ing on a constructive type theory that is expected to handle
infinite sets (Constable 1979]. Such a theory could probably be molded
into a powerful set theory for PgL.
For the remainder of tbis section. let T be an element type. x.y be
expressions of type I (hence a.e.). Q.R be expressions of type ?(T).
and gen be an a.e. generator of type I.
The first pair of axioms
edef			5 ? xe???(T)			false
and
5 &L xa(gen) = V(x:gen)
-84-
describe the basic properties of e. The latter rule uses the extended
domain of v to characterize the elements of (gen). For instance.
i*j?(a;b) is equivalent to iaj-svi*j-b. As in this example. V(x:gen)
sometimes requires a justification. The conclusion of the latter rule
is a = and thus requires two juatificstion tranaformers. First.
xE(genl has no deep constructive meaning (no information Is ever needed
on why it is true). so producing its justification from one of v(x:gen)
is trivial. (This would not be the case if aCts could contain booleans.
since by avbe(?ui) avb-? = avb, xe(gen] would l?aye tu carry
further information. I have chosen in favor of a simpler the?ry by
limiting the element types of sets.) Second. since sets are always
a.e.. V(x:gen) is a.e. so its justification may be obtained from the
truth of x?(gen) by a recursive analysis of its structure (deferred to
chapter 4). Thus. justifications for the conclusion of the second rule
can be constructed. The first rule yields a simple justification for
its conclusion. Since both sides of the hiconditionsl have trivial
justifications. the two justification transformers for the cm always
yield the trivial justification.
Recall that the characterization of iterators by predicates placed
a restriction on the bound variable names of legal iterators (section
3.2). For example. x:?!x;y) is ill-formed because the resulting V
predicate. x=xvx=y. does not correctly characterize the values of x
produced by the iterator. Howover that preditate does capture the
meaning of xs(x;y) since neither instance of 1 is considered bound. In
general. use of the ? function in the second def rule is correct. even
though x:geo may not be legal a an itecator. because fret uses of x in
-85-
the generator refer to the value of x in the surrounding scope. just as
does the x preceding the colon. This use of V wotivated its definition
(section 3.2) on an e:tension of the class of iterators.
The remaining set theory rules' are presented without individual
discussion.
edef			S ?			?xeq
s ?			A xsg
8 ?			xa?g			?q v ?g
-def			8 ?			x'Q?			ssQ A fl'R
cdef			8 ?			(Va:eQ)(aag)
def			8 ? q?R =			A
cdef			s ? ?g			Q? A
?ef			8 ??w1Lj?(T)=O
also			8 ?			#(Q li'L x)?
and			8 ?			--H #(Q add x)?+l
Justifications for these aIioms where needed. are easily obtained
since all e?pressions are s.e. and the alternatives of diajunctions Can
he directly tested.
The coupleteness of the P&L set theory will not be argued. It is
sufficiently couplete to handle the exauples presented herein. As I
have noted, the da?elopment of a coiprehensive theory of sets snd other
-86-
constructed types is left to future research.
As an example of reasoning about sets consider the description of
set reduction operators for union and intersection. These operators map
a set of sets to the union (intersection) of all component sets. Given
S. a set of sets of ohjects of type T the union I. is characterized by
(Vz:T)(x?R0( ? Q:aS)(xaq)).
The intersection is characterized by
(Vx:T)(x???(Vq:as)(za?))
It will be convenient later to know that these descriptions uniquely
define g I shall demonstrate this by supplying a proof schema which
may be specislized to the two desired proofs.
Suppose a set R is characterized by x'R?P . where F is sny
predicate not involving R. Clearly. P uniquely characterizes R. since
if xag'?P1 then xeR'??1c?xaR, and so R--R'. This is formalized as
follows.
-87-
(VxtT)(?R?P?.( VXo+T)(x'?'?Px) ? R?R' ? def
nr ?`AR'cJt ? As
?			C def
?LL (Va:--HR)(asg') ? Vs
o+ o+.o+,aaR ? a??? kx Vs on first hyp with a for x
o+aaR ? true It true def
o+ o+ o+.a?g.a.Rc'p5 ? a?R' It
o+aaR.amR?P5 ? a?R' It
o+ o+ a?R ? a?R It assumption
? a?R It Va with a for x
o+ o+.P5 ? true It true def
o+ o+?a .amR1?Pa ? It ?a
o+??`?a o+P5?aeR' ? amR' It ?s
? ?a It assumption
o+. .ao+sR' ? a?R' It assum
o+. ?			It c def
>symsetric argument
3.7 ?efinememt? rra-sit;on snecifjcar,o?s
Transition specification refinement rules provide for the synthesis
of programs from simpler ones using several well known constructions.
such aa sequential composition and unbounded iteration. The selection
statement (if-tben?else) of conventional languages is provide? by
vanalysia. Tbt'ae refinement tnlea are theoretically adequate for
itp:?enting any tomputable operation, but rules for other control
-88-
constructs could be included as desired (see chapter 5).
The lowest level transition specifications in a proof are
i?ple?ented by the system. The rules
<env> s ? xxn ? nv 51:expsn:expn
where each exp is an a.e. expression
choice			<env> S ? x			nv a:Sexp br
<env> S ? exp??(T)
where x is a single variable and exp
is an expression of type liL(T) in <env)
say be used to prove 5obviously true5 propositions (choice is 5obviously
true5 because all sets are a.e.). Together with the following rule.
they are the only ways to refine a transition specification without
introducing another one as a subgoal.
null			<eny> S ? x			nv iter5 if
<env> S o V(iter5)
This rule states that no computation need be done if x already containa
a value satisfying the specification. The justification shoving that x
satisfies the iterator is provided by the proof of the subgoal.
Examples follow.
-89-
i abs(x) ? null
x?O ? x=abs(x) ? aritb
(since x ? abs(x) is an abbre?iation for
x a:abs(z) and V(a:abs(x)) is aaabs(x))
z ? ___ b:eS ? null
x's ? x's kx asst=ption
The next rule
s??nljfrjcatinn <env) 5 x an? itera ?
<env> 5 ? x any iterib
<env.b:T> S.V(iterlb) ? V(iter?)a?b
wbere T is the type of x in <eny> and
b?<env> (if x ia a list of names
then interpret T and b accordingly)
captures the notion that the goal specification may be satisfied by
implementing another, apparently simpler. specification. The
justification for the conclusion is obtained by flowing the
justification for 5 down through the two subgoals, For exasaple.
x<O &r I ahs(x) ? simplification
x<O ai x			-x
x<O.b--x ? h-aba(x).
-90-
Often a transition specification cannot be easily implesented
without furtber use of storage. The rule
war			<env> S ? x ? nv itera ?
var y:T
<env.y:T> S ? z.y * any iter?.b:T
where T is any type name. y?<env>. b?a
and b does not occur free in iter
allows the introduction of a new local variable. y. that may be used in
lower levels of refinement. The interior specification does not require
that any particular value be left in y. so it is a uscratchw variable.
The rule shown below for co'nposing n sequential transition
specifications is somewhat overwhelming at first sight. hence I shall
develop it gradually. First. the null and consequence rules are special
cases of composition ?or nO and n=1. respectively. A further useful
special case is for n=2:
<eny> S ? x ? anv itera It
<env> S ? x any iterlb
<env.b:T> S.V(iterlb) ?
x * any iter2c
<env.b:T.c:T> S.V(iterlb)?V(iter2c)?? ? V(iter5)?
where T is the type of x in <env>. b?c. and b.c?<env>
(if x is a list of naaes then treat T.b.c accordingly).
-91-
The second subgosl shova that holds after executing the first
subgoal's code. The last subgoal assures that the value produced by the
third subgoal's code satisfies the original specification. The
justification for S flows downward producing further justifications for
VCiterlb). ?. and V(iter2C). These then yield the justification for
the conclusion. The effect of symbolic aubatitution on the
justifications of formulas is described in chapter 4.
The full composition rule follows.
Connosition
<env> S ? x			any itera It
<eny>			s ? ?1x
QI ? x ? any iterlal
<env.al:T> S.V(iterl51) ? Q2?51
<env>			?2x ?			any iter252
<eny.al:Tan-IST> S.V(iterlal).V(iter2?)?51
....V(itern-lan?I??an-2 ? Qn??an?1
<env>			Qn1 ? x			any iternan
<env.altTan:T> S.V(iterl51).V(iter2al?
....V(iternS?)?an-l ? V(iter5)
a?an
where T is the type of x in <env>, all si ate
diajoint. and alan?<env> (if x is a liat
of names then interpret T.alan accordingly)
-92-
The even numbered subgoals specify transitions that are coaposed
sequentially. The odd numbered subgoals provide the reasoning that
insures each precondition. ?i' holds for its associated transition.
Note that in all odd numbered (logical) subgoals the names of 1 denote
their original values. while new values are represented by the names
alan. In even numbered (transition) subgoals the names of x
represent their 5current5 value, while 51an are inaccessible.
al
Thus. in the last subgoal. s describes x. V(iterl ) relatee a! to 1.
a2
V(iter2 ?x?al relates a2 to al. and so on. The couclusien,
V(iter?)a?an statea that the current values of nates of x (denoted by
an and related to an-I. sn-2, ... according to the hypotheses) have the
desired relation to the original values of names of x (still denoted by
x). As with two-fold composition. the justification of the conclusion
is the final result of starting with justification of S and proceeding
down the list of subgoals acquiring derived justifications from each
conclusion.
This rule is a good illustration of the need for an interactive
system to support FRL. All of the odd numbered suhgoala (though not
their proofs) may be derived automatically from the even ones. Thus,
handling the preconditions and performing substitutions could he left to
the syst?m. The user would indicate his desire to use composition,
entr vrn nunhered subgoals, and the rest of the refinenent step
wonId tit led in.
As cenark?d earlier, logical constants, though not always needed in
ate it cathave returned to the proof systen. They arise in a
particularly na?ty way in this conposition rule, A method for reasonin.
93--H
about transition specifications directly. without first converting to
predicates via V. would be beneficial.
A sieple zaeple of conposition follows.
? lean.var a?v m:div(su?(S)?)
v:div(sujn((xsx for x:as))?4?S) -
div(sum(S)?)?div(suu(S)?) ? composition
?			If assumption
S?1w1LA?LC?) ? mean.var anv el:suu(S).vl:sum((x*x Lli x:us)) If
>proof omitted: this would probably be a loop
S??LL1?(?).ml-suu(S)Avlsuu((x*x for x:--Hs)) ? tru If true def
rru ? sean.var any ml:div(meao?)
v2:div(var?#S)-divCmean?S)?div(mean?) If
>proof omitted: if div is an a.e. function (definition)
then the a.e. rule may be used here
S??LL1LkL(?ll).el-aue(S)Avlsum(((x?x ?
m2-div(mi ?)Av2-div(vi ?)-div(m1?#S)*div(inl ?) ?
12-div(sum(S)?)Av2div(sum((x?x for x:--HS))?S)
--Hdiv(sum(t) ?)adiv(sum(S) a4i) If
>proof omitted: simply use Aa on the last two
hypotheses then use substitution
The final rule for transition specification refinement treats
unbounded iteration.
94-
ireration
<env> s ?			anv itera )ti
jnvar?anr x			any iter1 ? t.+ ble 3
S ? x * any iter?
<env.i:T>			S.V(iter1) It
<env.i:T>			S.V(iteri).Bi It
It x			anv iter2b
<env,i:T,b:T> S.V(iter?),3= .V(iter2b)			It
V(iter )i*bAti*b<ti
<env.i:T>			S.V(iter1).ti?O It ??
<env.i:T>			S.V(iter?).?Bi It V(iter5)??
where T is the type of x in <eny>			b.?<enw>. tj
is integer valued. and 3. is boolean valued (if x
is a list of names then interpret T and i accordingly)
in this rule the names of x denote their original values i.e.. the ones
satiafying S. in all auhgoals except the fourth (x * any iter2b). where
the names of x denote their values at the start of each iteration. The
invariant transition x * any iter1 describes all the values that x might
contain after any number of iterationa of the loop. Thus. the first
aubgoal (the aecond line of the refinement) establishes that the Mmes
of x contain some tuple of values produced by iter -- this is
initialization for the loop. The second subgoal shows that the
predicate 3. can always be tested; the juatification it produces is used
to decide when to terminate the loop. The third subgoal shows tbat
whenever B. holds so will the precondition for the fourth subgoal. The
fourth subgoal (the loop body) changes the values of x to another tuple
which. b7 the fifth subsoal. satisfies iter and is smaller than the
previous tuple when measured by the integer valued termination function
t.. The sixth subgoal insures that when t. reaches zero the loop will
terminate. The last subgoal shows that any tuple of iter that
satisfies ??i is an acceptable result for x according to the original
goal. The flow of justifications for this rule is left to the next
chapter.
The following example shows how the union reduction (introduced in
the last section) may be computed. Given S a set of sets of objects of
type T, this loop computes a set R which is the union of the component
sets of S.
-96-
I? Ra:?(T) IL (Vz:T)(ao+tac?( ?Q:es)(rIq)) ?
? R,V ? anv lta:?(T) IL (V?:fl(xeia? 3q:.s)(req)).
? itera?ion
lwliaL R.V ? any 1i:?(T).Vi:i?L(ALL(T)) IL
vic?A( Vx:T)(x'Ric$ 3Q:evi)(xeQ))
as #(s-vi)+ ?hjle VixS
(let inv mean ViSA( V?:T)(x??i?( 3?:?Vi)(??Q)))
? R.V anv Ri:?(v),vi:?(??T)) iL inv kx simpi
? R.V ?kL(T).w&1?A?L(1li(T)) ? s.e.
R' ????(T).v'-i??CiLL(T)) ?
v'sA( Vi:T)(xcR'cn( 3Q:ev')(x-Q)) ?
>proof omitted
inv ? Vi?SvYi-S ? excluded middle
inv.Vi:S ? Vi?S ?
>proof omitted: VigS.Vi?S?viCS by set theory
? R.V * any (Rh:R?Q.Vb:?(Q)) for q:--H(s-V) ?
>proof omitted: introduce var Q. choose Q fros S-v,
set V and R
inv.Vi?S.( 3 Q:??Vi)(Vb-Vi?fQ)ARh?Ri?q) aL
vhcsA( Vx:T)(xeRbc?$ 3q:cvh)(xsQ))
?(S?vh)?(s-vi) bi
>large proof omitted: should draw on a previous
developnent of set theory
inv?(S-Vi)?O ? ?(Vi?S) ?
>proof ornitted: again. should be based on a
separate development of set theory
inv. `,(vi?s) ? (Vx:T)(x'Ri?( 3?:eS)(x?Q)) ? cons
tnv.?(Vi?S) ? Vi?S Ig
?proof as in section 3.5
inv.Vi-S ? (Vx:T)(xeRi?(3Q:?S)(xeQ)) ? subet
inw.Vi?S ? 8-Vi ? symmetry
inv.Vi--S ? Vi--S ? assumption
inv,Vi'S nr (Vx:T)(x?Ri?(?Q:eVi)(x-Q)) If assus
3,8 Ahatra?tion
Stating and solving complex programming problems requires the
formulation of complex specifications and proofs. These may be far more
easily nnderstood and manipulated if facilities are provided for naming
and parameterizing their components, thus capturing useful abstractions.
I shall present two mechanisms for achieving this abstraction: first
definitions (of two varieties) and then lermas.
The power of the specification language derives from the use of
complex predicates and expressions. A ?efin?tlon associates a
parameterized expression. 1.., a function. with a name. The simplest
for, ia
?ef D(b:T) --H expb
where fl is the definition name. b is a list of distinct parameter names.
T describes the type of each parameter. and expb is the definition body.
The free variables of the expression are limited to the names of b and
the expression must be well-formed in the environment <b:T> (well
formedness is precisely defined in section 3.9).
In order to simplify the logic. definitions may not be recursive
(directly or mutually) and most be global to all proofs (i.e.. there is
no notion of the scope of a definition). Relaxing the restriction on
recursion would be valuable; it ia a purely technical problem for future
research. whether to permit local definitions. and if so in precisely
what fore. is a deeper problem. The goal is to encourage modular proofs
that fit well into the machine sided refinement style. This broad
question is also left to further study.
Definitions nay be referenced with a rule of the following style.
<env> 8?D(e) ? C?D(e) It
<env> 8			? c
?exP?e			?exP?e
where exp is the defined body of D and e is
any list of a.e. expressions ?hose types in
<env> match those of T.
(As in the substitution rule. the name x represents those places in 8 C
where D(e) occurs.) This role is ?ost the substitution rule with the
subgosl ... ? D(e)exp?e left implicit. An equivalent system would
result if definitions were referenced by the rule 8 ? D(e)-exp?. but
the above fore is often more useful. For example:
99-
def divieors(mt?) --H (i:l ? n ? (3j:l ? n)i*jn)
def priae(n:?) --H divisors(n)--(l;n)
? prime(S) kX definition of prime
? divisors(5)--(l;5J kx definition of divisors
.? fisi ? 5 ? (3j:1 ? 5)i?ja5) (l;3) )t
>further proof text
A definition invocation. D(e). is a.e. iff the body of the
definition. expb is a.e.. Since all parameters to an invocation are
a.e,. the value of an a.e. invocation may be conputed by evaluating the
parameters. binding the formal names to the values, and evaluating the
definition body. Thus. given that the definition bodies are available
for inspection. constructs involving definition invocation. can still be
syntsctically checked for being a.e..
Often the parameter types do not affect the meaning or well
forsedness of a definition. For instance,
def flatten(R:liL(liL(?T)) --H (eQ for Q:egj
is a polymorphic (many types) definition that maps
in(liL(element type)) to ?(element type) for any element type. The
variable ?T is an implicit type parameter that may be used as a type
name in the body of the definition. A type parameter may occur several
tiaes in the foonal parameter list. in which caae any invocation muat
define the type parameter uniformly. Thus. the definition
liL overlapping(g:?(?T).Q:ili(?T)) --H ( ?x:?T)(x--HR A xeq)
A (9x:?T)(x?g A x,?Q) A (?x:?T)(?R A xeQ)
-loo-
may be invoked only if the two actual parameters bave identical types
(aet of something). Note the use of tbe type parameter in the
definition body. At each inatantiation. the body of a polymorphic
definition is evaluated with the type parameters replaced by actual
types.
Checking polymorphic definitiona for vell-formednesa requirea
extending the class of typea and environmenta to handle type parameters.
In order to limit the couplexity of the extraction proceas. typ?a nay be
abstracted only with respect to element types. 1.e.. a type ?T cannot be
instantiated as a ??Q1. (Otherwise a formal parameter of type `.T would
have to carry complex justifications anmetimes and trivial
juatifications other times. This leads to extracted code which perforis
different activities depending on the types of variables. In this work.
I have chosen to avoid run-time manipulation of type information.) Thus.
let type names be defined by
type			bool
element type
element type
ser ( element type )
?var
where twar is the class of variable names that start with o+??. An
environment is a set of clauses of the fora
clause			var			type
?var
lOl?
where no var or ?var appears more than once. A type of the form ?var is
legal only if it is present in the environmLnt of the proposition in
which it is used. These definitions ?atend those given in section 3.1.
There are several ways of treating type parameters in a polymorphic
language. This area continues to be widely resesrched. with much debate
on the best approach Demers snd Donahue 1979. Nilner 1977. Liskov
et.al. 1977. Wulf 1978). I have opted for a very simple system; all
type parameters in an environment are treated as representing distinct
types. Thus. two types are equal exactly when their names are
identical. Further. the type of any expreasion is uniquely determined.
These properties enable the introduction of polymorphism with minimal
conceptual extensions; the only changes are to the type checking rules
(still to be presented in section 3.9) and the invocation of
abstractions. In particular. the proof rules. V function. and set
theory renAin correct.
Consider 5 definition
def U(b:T) --H expb
that may be polymorphic. The env1ronm?nt of the body is <b:T> aug?ented
by ?var for each type name. ?var. occurring in the parameter list. The
ezpression must be well-formed in this au?mented?. he rule
for definition reference developed above must be modified to handle
polymorphisa. First. the interpretation of the word 5match" (as in 5e
is any list of s.e. expressions whose types in <env> match those of T5)
must be extended.
102-
Given an invocation with actual parameters of types aan of a
well-formed abstraction whose formal parameters are of types ?
say the types of the actuals match the types of the formal, iff
a)			(Vi:l ? n)(match(f?.a?)?sfailS)
and			b)			(Vi.j:l ? n)(matcb(f?.a?)s"?va?t1, A
match(f..a.)s'?v			? t1=t2)
? ?			s?t2s
where match(f.a) --H
fsa?			`succeed'
`succeed'
--H match(t.t1)
f?var ? "?var4?a5
5fail'.
That is, the types match if all individual parawcter types match and if
the type parameters may be assigned a globally c ?sistent
interpretation. For example. `flatten' may be invoked with any actual
parameter that is a set of sets of T, for any element type T. The body
of `flatten' must be correct in the augmented environment
<R:?(?(?T)).?T>, If `flatten' is invoked with a
?tch yields `?T??(?)'.
Consider a particular definition invocstion and let ?va?t
represent the composite aubstitution derived from the reaults of match
applied to each parameter, Thus ?var+?t changes all uaes of type
parameters into the correaponding actual types supplied by the
invocation. Tbe type of a definition invocation can now be defined as
103-
the type of CxP?Vat4t in an environment vbicb is <b:T>tva?t joined with
any type variables occurring in t that are present in the invoking
environment. For instance. if 5flatten5 is invoked on P of type ?T' (in
the invoking environnent) then the type of flatten(p) is the type of
Lli Q:'R) in <lt:?(in(?T))>?????t joined by ?T'. 1.e.. in
The general rule for referencing polymorphic
definitions is now expressible.
defj??tjnn <env> S			? C
?D(e)			?D(e)
<env> S?(exp?.1va?.t) ? C?(exp?.?vs?e.t?
where there is a definition D(b:T)?exp?
e is any s.e. expression whose types in
<env> match those of T. and 5?va?t5 is
the composite substitution resulting fron
the parameter type matching process.
The fore of definition that I have been discussing is useful for
shortening the expressions used in specifications. but it adds no real
expressive power to those specifications. Often, a value is most easily
specified by a predicate uniquely characterizing it. PRL supports th?s
second variety of definition by allowing a definition's body to be
the iterX
where x is a single name and there is exactly one value for x produced
by the iterator. This uniquely determined value is the result of
invoking the definition.
-104--H
Associated with each definition of this fori are two parts, The
first shows the constructive existence of a value satisfying the
iterator, The second shows that the value is unique. These proofs are
necessary to insure that syntactically legal definition invocationa are
veil-defined deterainiatic expressions. i.e.. that reflexivity holda for
them. Thus,
def D(b:T) --H the iterb'
<y:T',env?>			? y ? Aax `terb
<x:T',y:T?,env'> V(iter?X)?V(iter?X)xo+y ?
where D.h.T are as shove. x is a single name, env' is the augmented
environment of <b:T>. T' is the type of I (in iter1) in <env'>. and 7x1
y#b, The type of the definition when invo?ed is the type of iter?vsr't
in <b:T>?va?t joined by any type variables occurring in t that are
present in the invoking environsent (as explained shove). Such
definitions may he referenced by
definiro evaluation
<euv> 5 ? V(iter2?)x,b,?va?D(e),e,t
where e is a list of a.e. expressions
whose types in <env> match those of T and
"?va?t' is the result of parameter matching
-105-
and
Aef?n?rjnn uniqueness
<Cflv> Sy+D(e) ? C?D(e) ?
<CflV> S?D(e) ? V(iterbX)?,b.?va?exp.e,t
<env> S ? c
?exp			y?exp
where e.1?var?t' are as above. exp is an a.e.
expression whose type in <env> is that of D(e).
and y is a place bolder for occurrences of
fl(e) in Sc C.
The first rule uses the existence property to guarantee that the
value produced, D(s). satisfies tbe iterator. The second rule uses the
uniqueness property to allow replacing D(e) by any expression. exp, that
satiefis the iterator. Thia rule could be phrased
5 ? expcD(e) It
5 ii V(iter?)x.b,tva?exp.e.t
but again it is sore often applicable in the substitution form,
This fore of definition provides a method for computing the values
of invocations even if iterb is not a.e.. Thus. an invocation of this
fore of definition is always considered a.e..
The justification of an invocation, D(e), of this kind of
definition describes bow the value returned. say x. satisfies
?(iter:)b.Tva?.t' This is further discussed in section 4,6.
-106-
The following example denonatrates the use of definitions. Two set
reduction operators. union and int?rsection are defined and used to
sanipulate ordered pairs of integera.
Aef unred(S:?(?(?T)))
the R:?(?T) li (Vx:?T)(xeR?( 3Q:es)(xeq))
? * AaX R:?(?T) li (Vx:?T)(?R? 3q:es)(xsQ)) ?
>proof by iteration as shown in section 3.7
( VxI?T)(xaR?( 3 q:--Hs)(xaq)).( Vx:?T)(xsg5c?( 3q?s)(xuQ))
? = a' ?
>proof as shown in section 3.6
def inred(S:?C?(?T)))
the R:?(TT) li (Vx:?T)(x'?c?(VQ:.s)(x?q))
>proofs as for unred
def pair(i:?,j:?)			((i);(i;j)?
daf iapair(p:?(?(?))),s (3x.y:ia?(p=pair(x.y))
-107-
paf hd(p:?(?(?)))--H
flL li iapair(p)?( 3 t:?)(p--pair(ho+t))
A ?i.pair(p)?b--O
? Y AaX b:ja? ? ispair(p)?( 3 t:?)(p-pair(bo+t))
A ?ispair(p)?b-O ? consequence
? ispair(p)v?ispair(p) ? excluded middle
ispair(p)v?ispair(p) ? o+. ? Va
ispair(p) p? o+.. k? simplification
ispai?(p) ? y anv h:o+inr?d(p) ? choice
iapair(p) ? inr?d(p)?????(i???) ? cons
o+ o+ ispair(p) ? ( Yx:inj)(??inred(p)
? def eval
o+ o+ ispair(p),... ? inred(p)x??????(j?) ?
>proof omitted
o+ ispair(p).bninred(p) ?
ispair(p)?( 3 t:i?')Cp--Hpair(b.t))
o+ A ?ispair(p)?b--O ?
>proof omitted
?ispsir(p) ? o+..
>proof omitted: set h to 0
>umiqueness statement and proof omitted
-108-
liL
))it t:jaL IL ispair(p)?(3h:??(pxpair(b,t))
A ?ispair(p)?t=O
>proofs as for hd: compute ti as any t:a(unred(p)-inred(p))
I viii now discuss the second abstraction ?echanisa, tbe len-a.
which supports modular proofs. A proposition may be named and
parameterized by writing
lemma L v:VT(b:BT) --H <env> 5v.b ? Cv.b
wbere L is the lemma name, v are the variable par?eter names of types
VT. b are the constant parameter names of types 8T. tbe combined nases
of v,b are all distinct. <env> is the environment <v:vT,b:BT> aug?ented
to include type parameters. and v:VT is present only if c is a
transition specification of the form v a? ?t??v,b Subsequent to
such a (proven) l?mma, one may use the rule
emma			<env> 5			? c
v,b,?var??.e,t			v,b,tvar?,e,t
L n(e)
where 5, C are frorn the len-a definition,
n is a list of distinct variable names whose
types in <env> match vT, a is a list of s.e.
expressions whose types in <env> match ?T,
and 5?var?t5 is the composite suhstitution
re?u ?ing from maching s]l the pararetere,
-			-109-
If C is a boolean expression. the lemma is of the classical
mathematical kind. If C is a transition sp?cifi?atinn. however. the
leseta may be thought of as a procedure definition whose invocation
behaves according to the specification C with actual parameters
syntactically substituted for formal parameters. This interpretation
forces distinctness of the variable actual parameters. n. since the
resulting transition specification might be ill-formed otherwise.
This semantics for parameter passing reminds one of ALGOL 60's call
b7 name asechanism. However. since there is no way to have a variable's
location depend on another variable's value. the call by reference
machanism is adequate fur handling v. Further. since the proof of a
lemma assumes that names of v and b denote independent. distinct
variables. the implementation must handle actual parametere for b with
call by value. because a change to v must not affect the values of b
even if the actual parameters are identical variables. These details
(the creation and manipulation of justifications for lemmas) are treated
in the next chapter. It is interesting that the programmer may ignore
such subtleties; the rule for 5procedure call1 is very simple.
A' an example. the following pure logical lesma outlines a proof
that pairs uniquely determine their components.
-I10-
?e pair?uniqueneae(h:??,t:ia?.b':nLL'o+t':?)
pair(bo+t)o+pair(h'?t') ? b-b'At?t' ? def of pair(t?ice)
? b=b'At-t' ? conse?uencs
(let R abbreviste ((b);(h;t)J
and R' abbreviste ((h?);(b':t')) beiov)
R--R ? ?R'AR'ct kx
>proof omitted: use def and reasoning about
ltR'?RRA??R ? (Vs:eR)(sE?)
>proof omitted: use cdef and reasoning about
R--R'o+?R'AR'?R,( Va:sR)(scR')
b-b?At?t' ? conaequencs
? b--b? ? Vs uitb ?b) for a
? (b)-(b)V(h]-(b;t) ? Vs
o+ ? (hl-(h) ? reflexivity
(bieR' ? b--b' ? cona
o+ (b)?R' ? (b]?(b'JV(bi(b';t') ?
>proof omitted: use edef. reasoning
o+ (hi--(b')V(h)-(b1;t') ? h=b' ? Va
? h=h' ?
o+ >proof omitted
(b]--(b1;t1) ? b=b' ?
>proof omitted
R-R',RcR'AR'?R (Va?mR)(scR').b-b' ? t?t' ?
>proof omitted
h--b1.t=t' ? h-h'At-t' ? A5
? b--b' ? assumption
ho+b'o+t--t1 ? t?t' ? assumption
--HIii--H
The next few definitions introduce several notions about directed
grapbs.
let o+pair' be an abbreviation for ?(?(?)). 5seq5 be an
abbreviation for iLL(pair). 1edge5 be an abbreviation for pair. and
o+graph1 be an abbreviation for ?(edge). A sequence of integera
nl.n2.rL3nk-l.nk viii be represented by tbe set
?pair(l.nl)pair(k.nk)). A set nay be checked for representing a
sequence and the i? element of a sequence nay be selected. as follows.
def iaseq(p:?(pair)) --H
A (Y?:sp)(iapairCx)) A (hd(x) ?ot x:ap)a(l l2#p)
def select(p:seq.i:?)
tbe n:j:LL li (isseq(p)Al?? ? pair(i.n)5p)
A (?(isseq(p)Al?i?) n=O)
>proofs oaitted
A grapb is represented as a set of edges. A path in a graph C is a
sequence of nodes which are connected by edges of G. A node. n is
reachable from anotber node. r. in a graph G if there is a path from r
to n in G.
--H112--H
Aef ispath(p:seq.G:grspb) --H
iaseq(p) A (VitI ??--Hl)(psir(select(p.i).aelect(p.i+l))eC)
def reschable(nt?.r:?.G:graph)
(3p:seq)(ispsth(p.G) A select(p.l):r A aelect(p?)-r)
The following lemma outlines a procedure for coaputing e m')dea
reachable in C from a selected node r.
Iemma reach Ns:?(ia?") (r:i???.C:grsph)
?nodes(G) ? NS any S:(n:--Hnodea(G) AL reachable(n.r.C)) Ig
war examined: ju?L(1n??)
renodes(C) &r NS,exaained fly ....liL(ia?) ? iteration
>proof omitted: start with ttS.(r),examined=?.
repeatedly pick (but don't delete) a node from ?S
(the reached nodes) whicb baa not been examined.
add it to examined. and add all its aona to ?S.
until there are no more such nodea
.9 Static analysis and twne cbeckin?
Throughout this chapter. 1 have referred to rules for static
analysis; these are presented below. The refinement rules snd
extraction process are only valid when all components of proofs are
well-formed. Thus. a mechanism must be introduced to rohibit erroneous
forms from arising.
-113-
The stAtic analysis mechanism is preaented as a set of functions
that operate on syntactic ob3ects. In addition to checking well--H
formedness, the functions define the free and bound variables of
constructs, the scopes of names, and the types of expressions,
iterators. and generators. These would he included in an interactive
system in such a way that suggested refinements could be rejected as
ill--Hformed as they were initially entered.
The environment of each line in a proof is determined by the rules
of refinement, Those rules assure the validity of a proof given the
well-formednesa of each line. Thus. the goal is to define a boolean
valued function W<env>?syntactic construct? that is true exactly when
the construct is well-formed in the environment.
In order to define W, I shall introduce several auxiliary
functions. T<env>tsyntactic conatructT yields i?furmation on the
type(s) of well-formed constructs. Given W<env>Lexpj, the type of eip
in <env> is determined hy T<env>Eexpj. Similarly, T<env>Eiterj is a
sequence of types that correspond to the bound variables of iter,
7inally. T<env>(genj is the type in <env> of the (values produced by
the) generator. The types yielded by T will be strings of the grammar
for rvne presented in the last section. An environment is a set of
clauses. each of the form var:type or ?var. also as described in the
last section. In any given environment, only certain strings from the
tv?e gra=aar are meaningful. An element type is lc'?al in <env> iff its
type parameter (if any) appears in <env>, A type is leeal iff it is
hnol or a legal element type. ?titer? yields the sequence of names
bound by the iterator, ????, g???5??? yields x. F?syntactic conatruct?
-"4-
yields the set of free variable names of the construct. Lastly.
E<env>Literj provides the modification of <env> that is appropriate in
the scope of iter.
The functions manipulate names. strings. integers. sets. and
sequences. Strings and names may be compared using = and x Integers
and sets are treated much as in PRL; set expressions are sometimes
formed using generators. Sequences may be created witb sequence
brackets (...J subscripted (e.g.. s(l) is the first element of 5).
concatenated (I?). their size determined C#). and tbeir content cbecked
(?). The notation uaed is flexible; I will explain any unusual
constructions where they first appear.
Proonsit ions
W<env>Lboolexpboolexp0 ? conclusionj --H
W<env>?boolexp11 A...A W<env>Lboolexp0? A W<env>Lconcluaion?
A proposition is well-formed iff all its components are. The
other functions need not be defined for propositions.
--H115--H
Transition snacjFicati??
W<env>?x?			any iteri --H
W<env>Literj A ?titerJ=n A
(V i:l ? n)(x?--Henv A T<env>?xiJaT<env)titerJ(i))
A transition specification is well-formed iff its iterator is
well-formed. the iterator binds the proper number of names. all
the assigned variables are accessible. and the types of tbe
sasigned variables are the same as those of the iterstor. The
predicate 5nanoeenv5 is taken to ?ean that name occurs In some
name:type clause of <eny>.
iterators
For any iterator5 E<env>titerj ja the environment created by the
iterator for usa throughout its scope. For example. in
the scope of x:? is ?x and the environment is the
original one augmented by the clause a:?. F `nay be defined
using T and N without deeper examination of the form of iter.
E<env>Literj --H env - (5n:anything5 for n:aNLiter?)
? (5n:t' where n-NLiter?(i). t=T<env>Liter?(i)
i:i ??LiterJ)
Fros hare on each syntactic form will be listed followed by the text of
all functions defined on that form. The environment parameter of each
function is implicitly <env>, I shall also limit my comments to
difficult or unusual constructions. as Engliab is both less concise and
less accurate than the formalism.
-116--H
tx1			x0			genj
N --H (XltX2????tXn)
F --H FEgeoJ
T --H (T<env>tgenj for i:l ?
W --H W<env>Lgeoj A (Vi:l ? n)(I??F?genJ)
The type of the iterstor is a sequence of length n whose every
element is the type of the generator. The iterator is well-
formed only if no Xj occurs free in the generator (see section
3.2)
?iter fl boolexp?
N --H N?iter?
F --H F?iterJ ? (FLboolexpJ-N?iterJ)
T --H T<env>Literj
W --H W<env>Literj A W<E<env>Liter??boolexpJ
In the body of F, N?iterJ is undergoing implicit con?ersion fros
a sequence to a set i.e. it really sesna (n:?tIiter?3. In W.
the en?ironment for checking well?formedness of the boolean
expression is that yielded by E<er?>LiterJ.
117--H
Liter1 ?or iter2j
we
liLiter1J
FLiter2J ? (FEiter1?Ntiter2?)
T<E<env>Liter2?Liter1J
w<env>?iter2J A W<E<env>?iter2?Liter1?
A (NLiter1?Liter2J4-)
Liter1			iter2?
I --H ILiter1i II NLiter2J
I --H FEiter1) ? FLiter2?
t --H T<env>Liter1j			T<env>Liter2j
V --H W<env>Liter1j A w<env>Liter2?
A (NLiter1?Liter2J?) A CNLiter2?Liter1J?)
G?n?rtort
Ltypej
T --H type
V --H type is a legal type
LexpJ
I --H FLexpJ
I --H T<env>LexpJ
V --H V<env>LcipJ
-118-
Lexp1 ? exp2i
--H FLexp1? ? F?exp2J
T --H 1?nt
w --H W<env>?exp1J A w<env>Lexp2?
A t<env>Lezp1?T<env>?exp2?1aL
?a expj
--H FLexpi
T --H t uhere T<env>Lexpj-uL(t)
w --H w<env>Lexp?
A (3t:legai e1emen? type)(T<env>Lexp?--iL(L))
Lc exp?			U expj
--H FLexpJ
T --H T<env>Lexpj
W --H w<env>Lexp?
A (3 t:legal element type)(T<env>Lexp?-iL(t))
Literi
Y --H FLiter?
T --H T<env>Liter?(l)
W --H W<env?LiterJ A ?EiterJ-l
--H119--H
Lgen for iterj
P --H F?iterJ ?
T --H
w --H w<env>?iterJ A w<E<env>titer?tgenJ
(gen1 ; gen2j
F --H F?gen1J ? ytgen2l
T --H T<env>tgen1J
v --H w<eny>t?cn1? A wcen?>?gen2J
A T<en?>??en1?T<env>?gen2?
?o1.pn e?nressipnn
T --H
v --H
L? expj
F --H Ftexpj
T --H bool
v --H w<env>?ezpJ A t<en?>Lexp?-?
-120-
Lexp1 boolop cxp2j where boo1opu(A.v.?.?J
F --H FLexp1J ? Ftexp2j
T --H boot
w --H w<env>?exp1J A W<enw>Eexp2?
A T<eov>?exp1 J-T<env>Leip2Jkg?1
?( Viter)expj (( ? iter)expj
F --H FLiterj ? (FLexp?-tiiterJ)
T --H hoot
w --H w<env?LiterJ A w<E<en?>Liter??exp?
A T<E<en?>?iter1>LexpJ-?
T?teeer e?nresp?onp
Lconj where cona(....-2.-1.O.1.2?...)
T - jot
w --H
Leip1 intop exp2? wberc intop-(t.+.??
7 --H FLexp1? ? FLexp2?
T --H lot
w --H W<eov>Lexp1? A W<en?>Lexp2J
A T<eo?>Lexp1?-T<eov>Lezp23=i?LL
-			-121--H
L- expj
Y --H FUexp?
T --H
V --H W<env>?axpJ A T<env>LexpJe?
Lexp1?1.exp1?2			e?p1 ?l relop
relop CXP?,CIPn.m03 wbe?c each relcp.(=.?.<,?.?.?)
I --H (eF?xp. -? La jal La a. for jal La n)
1.J			I
t - bool
V --H (Vial La n)(Vj:l La
A T<anv>Leip. o+3--ja&)
Set
rnuiiae?(t)3
t --H inCa)
V --H t is a legal alcient type
--H122-
E(genjj
--H F?genJ
T --H ?(t) where t-T<env>Lgenj
W --H W<en?>?gen? A T<env>?gen) is a legal eleaent type
A gen is a.e.
gen may be shown a.e. by straightforward syntactic examination
as described in section 3.2.
?exp1 setop exp2? where setops(A.V.?)
F --H FLexp13 ? FLexp2J
T --H T<env>?exp1J
w --H w<en?>Lexp12 A W<env??exp2? A (3t:Iegai element type)
(T<env>?exp1??T<en?>Lexp2??(t))
expj
F --H FLexpJ
T --H int
W --H W<eow>?expJ
A (?t:iegai elesent type)(T<emv>?eip?-??(t))
-123--H
?exp1 a exp2J
7 --H F?exp1J ? F?exp2J
t --H
W --H W<env>Eexp1J A W<env>?exp2? A ( 3 t:legal element type)
(T<env>Eexp2J-?(t) A T<env>(exp1j-t)
exp1??1 relop
relop exp?e?Pn,m?? where re1op.(,?.c.c)
7 --H (--HFLexp. .1 ?t j:l ? ?? i:l ?
L.J			I
T --H bool
W --H ( ?t:legal ele?ent type)(Vi:l ? n)(Vj:l ?
(W<env>Lexp. .3 A T<env>texp.??(t))
1 3			1.
Otber e?nressipns
?variable3
7 --H (variable)
T --H t where `variable:t?aenv
W --H variableaenv
-124-
Let satcb(f:type.s:type) be a cospile tile
function as in section 3.St
match(f.a) --H
f=s-kQ2l ? 5succeed'
`succeed'
f--?(t)As=j?(t1) ? sstch(t.t')
f-?var ? `?va?a5
`fail'.
?D(exp where D is the nase of a definition
exp0)J
def D(b1:tb :t ) --H
7 --H (aFLexp?J for i:1 ?
T --H T<eflV?>Lexp?va?tJ
where ?var*t is the substitution forsed by cosbining
the subatitutiona yielded by aatcb(t?.T<env>Lexp??)
for i:l to n and <env?> is <b1:tb?:tn>?var?
joined with type nanes taken from <env> for any type
paranetera in t (as explained in section 3.8).
W --H ( Vi:l ? n)(W<tn?>?exp?? A exp? is a.e.
A natch(t?.T<env>Lexp?J)?'fsilS)
A ( Vi.j:l ?
(match(t?.T<env>(expi?)w?va?tas
A natch(t?,Tcenv>Lexp?J)"var?thS
3			3
tath)
125-
LD(expCXP?)1 ?here D is the natne of a definition
liL D(b1:tbn:tn) --H the iter
where ?Liter?-1
1 --H (eFLelp?J for 1:1 ?
T --H T<en?I?>?iter2va?tJ(1)
where env' and ?va?t are as above
W --H aMe as V for above fore of definition
CHAPTER 4
THE ?XTRACTIoN OF PROCRANS FRON PROOFS
4.1 Refnement loeic metatheory
There are a number of important questions that may be asked of any
system of forasi reasoning. The atudy of these questions. the
netatbeory. certainly includes three fundamental concerns: independence.
completeness. and consistency. This section discusses the meanings of
these metatheoretic properties for refinement logics. The remainder of
the chapter deaonstrates the consistency of P&L.
A set of axioms and rules of inference is said to be indenendent if
no element can be removed from the theory without decreasing the class
of theorens, i.e.. provable propositions. In this case, there is no
redundancy in the foundation of the theory.
Independence is a useful property of a logic if one's main concern
:s the corresponding metatheory. because by holding the logic to
essentials. the volume of metatheoretic analysis is minisixed. If,
ho?ever, one is interested in actual proofs in the theory then
independence is not as important as having 5 useful. easily applied
system. In PILL, where there is only a limited mechanism for introducing
derived inference rules. there are redundant rules built into the logic
(e.g. symssetry and trensitivity), but they are sufficiently conion and
-126--H
--H127-
uaeful to justify their presence. As with prograsmeing languages, the
clarity and elegance of user text is the guiding consideration; often
this leads to a clear and elegant compiler (metatheory). but this is not
the primary concern.
Comnieteness in a classical logic means that for any proposition A
(with no free variables). either A or ?A is provable. The intent is
that every true proposition he provable within the system (truth may be
defined by assigning an interpretation to all propositions of the
language). Sufficiently powerful classical logirs lack completeness.
since for any machine N either ?x halts' or "11 diverges5 is true. hut by
undecidability results. in general neither c?n he proven from any finite
set of asioms. Thus. one is forced to consider relative completeness
results of the form o+if this fragment of the theory were complete then
so would be the entire theory5. Interesting results for programming
logics can be obtained in this framework (Clarke 1979. Corelick 1975.
Ovicki 1975); in particular. with appropriate assumptions. Hoare's axiom
system is complete for simple sequential programming languages (Cook
1975).
In a constructive system. such as PRL, there is no obvious model
theory. i.e.. no definition of truth other than provahility. so the
completeness question must take a different form. A general notion
might be `whenever a formuls is provable in any `???????h??l axiom
system is it also provable in the system under study?". If the answer
is `yes5 then the system might be considered `reasonably5 complete.
Hence. Ihe i?ea of `rea?onsbly provable5 takes the place of truth. of
course. 5reasonable' axiom systems are too vaguely specifie? for fornal
-128-
study. ?owever. one migbt examine specific well-knoyn logics in place
of all `reasonable' ones. Yor example. one could establish that FltL is
complete relative to Hoare's logic by showing that any
precondition/postcondition pair that accurately describes an asserted
program in ?05???? logic can be phrased as a transition specification
and refined in FRL. That is. the specification language and refinement
rules are powerful enough to develop any asserted program that is
expressible in ??5??'5 logic. Though I have not performed such a proof.
I see 0 significant barriers to doing so (of coo?se the logic r?y have
to he extended if it turns out too weak. but I would expect only minor
technical extensions).
There is one further notion of completeness that is not
formalizsble. yet is nonetheless important. This is whether the
language of propositions is sufficiently powerful to characterize
concteely all interesting program segments and computations. Clearly.
this is not the case as such notions as input/output. abstract data
types. and ChU iterators (anong many) are not supported. In addition.
the rules for refining specifications could be extended in many ways.
Nuch work remains to develop a complete system in this informal sense.
Conaiarencv means that no formal contradictions can be derived in
the logic. Classically. this is usually shown by building a model of
the theory that provides an interpretation for each proposition and
showing that every provable foroola is true in the model. Civen that
the model assigns opposite truth values to A and ?,A C?or all
propositions A). the t?eory nost not contain contradicti?o?. or
otherwise both a proposition od its negation woold be tree in the
-129-
?odel. The proof that all proveble foraulas are true proceeds by
inducti a the length of der?vata: one shows that the axioms are
true sod the rules of inferenco preserve truth.
In ?gI? many propositions claim the constructive exiatence of
prograss. so proving consistency means showing how to extract programs
froa pcoofs. Therefore. I demonstrate consistency in this chapter by
presenc?ng an extractor (coupilor) that recursively analyres any proof
and produces an implementation for its goal. Where no implementation is
needed. I simply show why the truth of a conclusion follows from the
truth of its hypotheses. ?or example. in set theory there is no deep
constructive meaning to xsS. but it is necessary to show that the the
theory is consistent. The explicit description of an extractor proves
an essential property of the logic and justifies the view of PRL as a
language for expressing programs.
Once the notion of extraction is conceived. one must decide what
sorts of objects wilt result from its application. As was explained in
section 2.4. because PRL has a unified set of proof rules.
justifications are needed to provide the constructive content of each
proven formula. One can illagine logics for which this is not the case.
logics in wLich formulas have no constructive content and hence need no
justifications. xtractors for these logics would produce
straightforward code for each program specification. combining these
code seg?ents according to the refinement rules used. Pure logical
proofs would have no effect on the extraction process. only rules such
as composition and iterstion would build new code (and they would ignore
proofs of purely logical subgosls). This type of extraction is
130-
precisely what happens when a conventional compiler reads an asserted
program. compiling the code while ignoring assertiona. The assertions
may thua appear to the programmL'r as an unnecesasry burden.
In contraat. when one constructs a proof in a logic whose boolean
formulas have conatructive meaning. the whole text of the proof enters
into the extraction proceas. Important parts of the final program come
from proofs of diajuoctions and existentisla. The extractor may be
applied only to complete valid proofs. hence, the 5purely logical5 proof
text takes on immediate significance. as it is needed not only for
correct code, but for any code at all.
The method for extraction (presented below) developed slowly. In
my early work. I believed that justifications could be compile time
objects describing bow to combine code fragments. while final programs
would manipulate only those values and variables clearly used in proofs.
For many proofs there were 5obvious" programs that I desired the
extractor produce. Though tbe desire was justified and the belief
intuitively correct. many difficulties arose in my attempts to extract
"obvious5 programs directly.
Consider the vanalysis rule where the goal is a boolean expression:
AvB or C. Each subgoal produces a method of converting a justification
of its hypothesis into a justification of the conclusion. The overall
goal must do the same, but the justification of its conclusion depends
on whether A or B is true, which may depend on the run time result of
some test. Thus, the particular justification produced for the
conclusion, though it always has the same general form. depends on
-131--H
events occurring during execution.
Upon realizing this difficulty. I still wanted justifications to be
bandied only at compile time. I tried to develop a compile time method
for unifying the subgoal justifications of an vanalysis into a single
justification for its conclusion. This led to increasingly complex
compile time data structures for representing justifications and
similarly complex methods of extraction. When further difficulties
developed with other rules. I decided to consider the run tine
man?pulation of justifications. even though this seened to imply
i?e.'f??ient extrscted progrsea.
With this approach. the extraction process immediately became
tractable. if subtle. I was able to write the extractor as a large
recursive function. When I applied it to examples5 it was clear thst
several well ?aown code optimiration techniques could so improve the
extracted programs thst the extract-optimize combination often produced
precisely the sort of implementation thet I had intuitively believed
possible. Thus. I present below the extractor fur run time msnipulation
of justifications sad the optieizstion techniques that make this
approach feasible.
?.2 The extraction 2L aL2uA1a from nroofs
Given a proof of a proposition. BB0 ? C the ??or X
produces a procedure that maps justifications of the hypotheses into a
uatification of the conclusion. These procedures are expre?sd in a
conventional PASCAL-like progranming language. L. that is de.cribd
--H132-
below. The choice of a high level target language is to aid the reader;
an actual impleaentation of Fli would likely produce assembly or machine
code directly. Nonetheless, while L is intended to hide many ?esay
details of coapilation, it has been kept sufficiently simple that most
interesting aspects of extraction are confined to ?,
The extractor is a large recursive function from proofs to L-code.
A clause of x exists for each refinement rule describing bow to generate
code for any proof that begins with that rule in terms of the code
generated for each aohgoal, Thus, one may generate code for a large
proof tree by applying X at the leaves and successively working up the
tree using the appropriate clauses of X at each stage. Almost no other
information transfer or checking is done during extraction. huc gisen a
well formed proof, the resulting L program will he similarly well
formed.
The general form of a clause of X is
Xirefinement rulej --H rha
where refinement rule is a pattern representing a complete proof that
begins with the refinement rule and rha is either a procedure constant
of L or a choice of procedure constants bssed on information obtained
from the static analysis rules of section 3.9. The procedure constants
of the rhs often contain instances of X applied to aubgoals. These are
to be testually replaced by their values. i.e.. the procedure constants
produced by X when applied to proofs of the respective subgoals. The
rha also contains nam&s, expressions, iteratora. etc., present in the
refinement rule. These ace to be textually replaced by those actually
present in the inatance of the refinement rule being processed, Thus. X
133-
say be viewed as a complicated sort of macro definition in which
parameters are obtained from eacb refinement step by pattern matching.
At this point, the reader may wish to examine the next section for
cesaples,
L is a conventional assignment based programming language. It
includes an iL-Lh?A-LLu-li conditional statement, a
selection statement, and a ?-??? loop statement, all with standard
aemantics. Assignment is completely defined by Hoare's assignment axiom
because there are no partial variables (such as array elements), nor any
aliasing, All variables must be declared with a fixed type. Scopes are
determined atatically. L does include two unusual features requiring
detailed discussion: procedure values and recursively defined data
types.
The types of L include boolean, integer, character string,
procedure. and those that may be defined with recursive data type
definitions (Hoare 1975). Booleans and integers have conmonly available
operations. Strings are treated flexibly, but all operations could be
easily reduced to ?ubstring, concatenation, and so on. Procedure values
are explained in detail shortly: they may be formed from the text of a
procedure and an environment by the bind operator and may be applied to
actual parameters. Data type definitions allow types to be defined as a
diacriaineted union of records, for example.
LIST JulL() + PAIR(HD:VAWE, TL:LIST)
VALtt 3ooL(?h? o+ INT(I:jn) + SET(L:LIST)
134-
Given a variable R of type LIST, it must be either NULL or a PAIR. If I
is a PAIR then its second component could be selected by R.TL. A new
value of type LIST could be formed as PAIR(INT(3),R), where INT produce.
a VALUE from the integer 3. Thus. NULL, PAIR. BOOL. INT, and SET are
constructors, while ND. TL, II, I, and L are selectors. Equality testing
and assignment are defined for all types. both primitive sad defined.
A procedure constant is written
oroc			fro Ir): var decla; stmts end
where I is a list of typed parameter names that are called by reference
andY is a list of typed parameter nanes that are called by value.
Procedure constants may read and modify global variables according to
static scoping rules. A procedure constant, P, that does not modify
global variables may be converted into an asaignable value by writing
)as?(P). A bound procedure includes a copy of the environment and state
active at binding. any references to read global variables are resolved
in this fixed environment. Thus, a bound procedure is aiailar to a LISP
FUNARG; it is a pure value whose meaning remains invariant as it is
passed around the program.
The type of a procedure is written ?(types li2a types).
Variables may be declared procedure valued. They may be assigned any
bound procedure value whose parameter types equal corresponding
parameter types of the procedure variable's type.
Given a procedure constant or bound procedure, P, the invocation of
P say be written
P(vars from exps)
--H135--H
where vars is a list of distinct variable naaes accessible and
modifiable in the current environment, while expa ia a list of
expressions. The types of vars and expa must equal the types of the
procedure's corresponding formal paraneters.
For any proved proposition, ?5n ? C. the extractor will
produce a procedure of type ???(JUST ?? JUSTn) where JUST is the type
of a run ti?e structure that represent ?i?tifj?atiors. This procedure
produces a justifi??acion of C fr(m justif?cnt;??s Of 55n' If C ia
a transition specification. x atty iter , t?efl t'?e pcoccdure will
change the global variables na?ed by x and yield a justificatiun for
where
V(iter a repreaents the new values of a. The. extracted
procedures perform all the needed computation On t'?e ernIe;
juatifications paseively describe why formulas are true (tough they nay
contain bound procedures which can be invoked to perf?rm various side-
effect free coeputations).
The type JUST is defined recursively below.
JUST a NlL()
+ A???(Jl:JlST. J2:JUST)
+ oR(StfL:k?1. J:JUST)
+ 1MPL(JT:??(JUST from JUST))
+ EQUTV(JTI:iiir?(JlST from JUST). JT2:??(JUST iyi'nt JUST))
+ SOML(VALS:LlST. JI:JlST, J2:JUST)
+ ALL(JT:?(JUST from LIST.JUST))
+ TRA?S(J:JlST)
--H136--H
Each kind of formula baa an associated fors of JUST. A forsula may be
thought of as 5type5 information describing the structure of its
justification. e.g. AAB describes an AND vhose coaponents are described
by A and 5 respectively.
A given true focaula may be justified in a variety of vays. For
instance there aay be any values satisfying an existentially
?uantiffed predicate. Un order to understand tbe behavior of ? one
needs a prec SC des?riptiou of tie relationship between objects of type
JUST and the focrulas they justify. This descriptfou is provided by
J:fornula K state net of JUST. where the formula is constructively
true in the state. I shall ?ay ttat j justifies F in state s iff
j?JLij(s).
A justification is a pure value; it makes no reference to externsl
variables. Thus. once created. a justification may be passed around a
prograa without its value changing. A formula. however. does refer to
variables. so its aeaning depends at any tiwe on the state of the
coaputation at that ti?e. For essaple. the justification chosen for
x<ovx?o depends on the value of x. but the two choices. oR(??.NlL())
and Ot(jjijj?.NlL()) do not theaselves depend on x. Thus. J yields the
set of justifications that cectify a focnuls in a given state.
The definition of J is by cases. formalizing the presentation of
section 3.4. The definition ones the notation s?d?] to denote the
variation of state a in hich sariables listed in d have values listed
in x.
--H13,'--H
JLAAB?(5)
JEAvB?Cs)
?LA?3?C5)
?LA?B?(a)
(AND(J'1,32) I jl?J?A1(s). 2?JLB?(a))
= (OR(b,j) I (b??AA ja true in sAjaJLA?Cs))
v (b-?1??AB is true in sAJ'.JtBJ(s)))
tIxPL(P) I (V3')(J'aJ(Al(s) j'?JLB)(s)
where j' is the value of j'' yielded by
the invocation P(j1, fro,, j)))
since P is bound. no state need
be specified at its invocation
= (Equlv(pl,P2) I 1MpL(Pl)--HJ?A?13?(s)
A ?NPL(p2)--HJLB?A)(s))
j??B?Cs) =
JL(?iterd)B??(s) (so?(x.31.j2) I V(iterd) is true in sCd??)
A B is true in aEd???
A j1.J?V(iter )1Ca(d??))
A 32--HJ(B ?(ald'x?))
d
J?(Viterd)Bd?(s) (ALt(r) I (Vx of typ?s correuponding to d)(Vj)
(3?J??(iterd)1Cu[d?]) 3''?JtBd1(s?d=it?)
where j' is the value of j'' yielded
by the invocation F(j'' ?
since P is bound, no state need
be specified at its invocation
?n?y iterd1(s)			(TRAt's(j) ( ? v of types corresponding to d)
CV(iterd) is true in a(d=i']
A 3.JLV(iter )?sEd??]))l
J?sisp1c def refl(s) a JLinstantiated bodyl(s)
J?bool varisbls2(s) a (NIL()) . but see discussion below
of extended justifications
-138-
JLother hool expj(s) ?NIL()) . varieties enumerated in section 3?4
Given the preceding d?scription of which juatificationa certify
which formulas. one can approach the problem of establishing the
correctnesa of the extractor. I will not formally demonstrate X's
correctneas. but will sketch how it could be done and will note several
lemmas of importance in such an undertaking. This discussion should aid
the?reader in understanding the extractor.
A proposition. 5 ? F. denotes a justification transformer. A
justification transformer for 5 ? F maps a state and justifications for
5 into one of many possible final states and justifications for F. Let
N (for meaning) map propositions to the justification transformers they
denote. Thus.
N: proposition (state x jU5T*) set of (state x JUST)
N may be defined by cases:
So ? Bj(s.jl
where 5 is a boolean expression and (Vi)(jiejEsij(s)).
M?SlSn ? x anv iterd?(s.jljn)
= (<s'.j> 1 (?v of types corresponding to d)
(V(iterd) is true in std=v) A s'=str?v)
A j--HJLV(iter )?(s(d??))))
where ( Vi)(jieJLSi?(s)).
-139-
The extractor. 1. is correct iff
(Vproofs: 51Sn or y ? ...)(Vs:stste)(Vjljn:JUST)
(xrslSo ? F ? ...J is a procedure P(j' from jljn) s.t.
[(Vi)(Si true in 5 A jisJLSiJ(s))
? the invocation F(j' from jijn) in state 5
yields a state a' and a justification j' such that
<s1.j'>?M?SlSn ? F?(s.jljn)) ).
One would shov the correctneas of the extractor by induction on the
structure of proofs. Each clause of X's definition would require an
argument that correct extraction from the subgoals resulted in correct
extraction for the goal. There are two important properties needed in
such an analysis. One concerns justifications; the other concerns
justification transformers.
The first property. jLt;;t name indenendenc?, states that any
justification for a true formula B in state 5 also justifies B? in
state s(d+i?. where d is a list of names not occurring in Bx
Intuitively. this holds because has the same structure as B
Since boolean variable names are justified by any JUST (usually NlL()),
since other variable names have no justification. and since
justifications themselves do not refer to external variables. the
justifications for ? and are identical. This property may he
formally proved by induction on the structure of formulas (with much use
of the definition of J).
--H140--H
The second property. cor?ect transformation IL e?ten?ed
?stificarin?. states that an extracted procedure for Dr Fx should
map a justification of S to one for F . If x is Dot boolean
x??exp			?exp
then S and S?exp have identical justificstions. similarly for F and
I			1
F?exp Thus. in this case. the property clearly holds. If x is
boolean then a justification for Bx?exp is called an stended
juatfiration fot B . Extracted procedures correctly transform extended
justifications becauae any structure that justifies a boolean variable
in 5 is manipulated as an indivisible unit (the ?type? information of
?x prohibits any exaTnination of deeper levels of the justification).
Further. the manipulations of justifications for bonlean variables makes
Do assumption about the form of those justifications -- what goes in
comes out. This property is required to support the validity of the
substitutions used in the rules of specisli?ation and Yanalysis. amons
others. It may be established during the proof of corrtctness of the
extractor. by induction on the structure of proofs. Equivalently it
may be considered as one of the correctnese criteria for x.
This ends my discussion of properties of I. The reader will likely
find it helpful to refer back to this text while reading sections
4.3-4.6. In particular. the description of J is most useful. Before I
present the defining clauses of I. however. there are three remaining
topics to cover.
First. in order to reduce the volume of text present in the
definition of X (sections 4.3-4.6). the names H and G and all their
variations are implicitly asaumd of type JUST. while the Dane L and all
its variatious are implicitly assumed of type LIST. Ii names represent
-141-
justifications for hypotheses of propoxitions; G names represent
justifications of conclusions. The syubol H* is an abbreviation for
hi?n it represents the justifications of hypotheses for 5. as in
5 ?
Second. as discussed in section 3.4. the bypotheses of a
proposition may be freely reordered and the hypothesis of interest in a
refinement step need not occur lest in the hypothesis list. The
extractor must compensate for this freedom by reordering fornel and
actual parameters to correspond to the refinement text. I shall not
mention this further in the extractor description. but it will arise in
the examples at the end of the chapter.
Finally. the extractor1s handling of sutomatically evaluatable
expressions must be examined. Translating a.e. expressions into L is
easily achieved with conventional coapiling techniques. Integers and
booleans are directly repreaentable. Scra nay be implenented using the
LIST type with trivial 0(n2) algorithus for the set operators. Though
better representations and algorithas would undoubtedly be used in a pgL
implementation. they are not of interest here. The details of
translating a.e. expressions are similarly omitted; I assume a function
V: a.e. expression equivalent L expression.
Producing justifications for a.e. expressions. though no harder
than evaluation. is of greater interest. Define J55 : true a.e. boolean
expression L exprLssion evaluating to a justification. by cases.
?ae?AABJ
JaeLAV13i
J LA?B1
J ??Bj
AND(Jae(A1?JneLBJ)
= IL v?AJ then OR(?.Jae?A))
?Se OR(?i?JaeLB?)
= lttPL(?(?(G from ?): G ? JsetB? ?))
since given H A must be true. hence B
must be true (and s.e.). so JseLBJ iS
the desired result
= EQUIV(??(?(G from N)i G J Lg? ?)
from H): C ? JsetAT ?))
reasoning as for ?. above
JaeL?B?			=
d			d
J???(3iter ??d1 = SO??(dJaeLV(iter ?3?se?5d??
,`he?e dchooae(VLiterd3)
This means to choose any tuple of values
of iterd (assume v produces an
appropriate rcpr?sentstion). cali this
tuple d and yield the SO?? justification
`,here the inside uses of J are
evaluated in a state vith d available.
Since the 3 is true. V??ter ]
cannot be empty.
JaeL(Yiter?B?J = ALL(kjwL(?(G from L.H):
var d:VALUE;
d			elements of L;
C			J Ls
am d
Given L and justification H for V(iterd).
-lA3-
since (Viter?3? is true it ssust be
that Bd4tleaente of L is true (where
? elenents of L5 means to assign the
name of d the i??? value of L for
all i). hence JaeLBd1 yields the desired
result when evaluated in an environment
where d exists with the proper values.
J55Laisple def refj			Jse?instantiated bodyl
J55Lother bool upj
4.3 ?,traction? lpg?fa? nLlal
fech rule of section 3.5 is reproduced below together with the
associated result yielded by the extractor. Often the rhs of x is a
single procedure constant. but for some rules a condition based on
static analysis information is used to select between alternatives.
Brief explanations follow the extraction rules. where needed.
true definition
ILS ?			-
from Ha): G ? NIL() end
Given justifications Ha for S. i.e.. H1.H2the
justification for true is sinply NlL().
false definition
&c cJ --H
?(G from Ht.H): G ? NIL()
Since a justification. II for lAlu can never be produced. this
procedure cannot be invoked. Nonetheless. this rule say be used
in proofs of loop termination where no justifications need be
produced.
aicluded "dd?e
X?S ? Bv ?flJ --H
?(G li2i ut): li vLBJ rhn G ? OI(???Jae?BJ)
Alli C ? oR(jt:tttt.IIL()) li
If ? is true in the current state then yield an Ol whose 3
component justifies I otherwise yield an Ol whose 3 component
justifies ?,B (i.e.. is NlL()).
ssaumntjqn
xEs.B ? BJ			--H
?(c			Ht.H): c			ii
If B is a boolean variable with a non-trivial justification.
this rule allows the justification to pass across the ? for
aubse?uent synthesis into more complex conclusions. Passing the
justification through without modification is easential to the
validity of the cisin of the last section that extracted
procedures correctly handle esteuded justifications.
A
xLs,A1AA2 ? c ?
S,A1.A2 ? cJ --H
f?p Rt.H): xLs.A1.A2 ? c?(G from H*.H.Jl.H.J2) end
Given `1 justifying A1AA2, break it apart and produce G by
applying the procedure conatant of the subgoal to Ha and the tvo
component justificationa.
Asvntheaa
? B1AD2 ?
S ?
a ? n2J --H
ftoa Ha): var Gl.G2;
?ts ? B1?G1 from Ha);
x?s ? B2?(G2 from Ha);
G			ANn(Gl.02)
Independently compute justifications for Bi B2 and yield their
Am' combination.
-146-
Vanalygia
XLs.A1VA2 ? c ?
S.A1 &L C
S.A2 ? cJ --H
li2rn H*,li): li li.SEL the X?.A1 ? from B*.a.J)
1u X?S.A2 ? C?(c from H*,H.J) li
Test the selector and produce G from tbe appropriate eubgoal'a
3ustification transformer.
V
X?S ? B1VB2 ?
S ? B1? --H
from 11*): var
xts ? B1?CG? from ljt)
G
also
xus ? B1vB2 ?
8 ? n J --H
from H*): ili
X?S ?? B2?(G' liQi 8t);
C
-147-
?analvaii
xts.Al?? ? c ?
S ? A1
S.A1.A2 ?			--H
li21 Ht.H)s iu Cl.G2s
x?s ? A1?Cl li2i H*):
R.JT(C2 from Cl);
xts.Al.Al ? cJ(C from l;*.C15C2)
Obtain Gi justifying Al apply the bound procedure H.JT to Cl
obtaining C2 justifying A2. and uae Ht.Gl.G2 to set C. R.JT
cannot change the state so CI justifies Al throughout.
?avnrhesis
? Bl??2 It
s.Bl ? fl2J --H
?(C lini Ht)2 G ? INPL(kia?(?(C' from H):
lLs.B1 ? B2?(C' 1j;;i Ht.;;) ?)) end
C.JT is a procedure vith the values of global variables and 6f
He bound in. when it is given a justification for B1 that is
valid in the o+frozen5 state. it returns a justification for
that is similarly valid.
an' lviii
X?S, ?B ? filie ?
s ?			--H
?(G ligi H*.H)z c			ML() fl&
ivn?hei;?
xts ?
S.B ? filiel --H
?(G f? ?): G NIL()
c ?
?
li2i ilt.H): vi G1.c2?
cl			IMPL(?.JTl);
c2			LMPL(H.Jt2);
x?s?A1?A2.A2.?A1 aL CJ(c lin H*.Gl.c2)
-149
tnavn?hea is
its ? B1?B2 ?
a ? B1?%
?			--H
from at): iu G!.C2;
xLs ? B1?B2?c1 ? Ha);
its ? B2?B1?G2 f?o Ha);
G			??UIV(G1.JT5G2.JT)
V analysis
itcenv> s.( ViterX)Bx ? C ?
<any> 5 n V(iter ??exp
<eny) S.(ViterX)Bx?Bx?exp ?			--H
F? Ha.H): ?? Gl.G2;
its ? V(iter1)			J(Gl fr? Ha);
x?exp
H.JT(G2 ? vtexpl.Gl).
its.(Viter?Bx.Bx?exp ? c?(c from Ha.H,G2)
Civen a justification for the quantified formula and Cl
justifying v(iterx)?eap a justification for 5?exp can be
obtained. A subtle point concerns the use here of H.JT. The
expected inpur to H.JT is a justification of V(iterX)s but Cl
say be an extended justification (section 4.2). for it also
justifies exp (if exp ja a boolean expression). Further. tbe
desireci result Tnust justify ??????. not only Bx Ilowever.
because H.JT correctly tranaforms extended justifications (see
Vs), supplying a deeper justification to H,?T causes it to
produce a deeper result, justifying B?exp in exactly the
required asnoer.
XE<env> 3 ? (ViterX)B kX
<env,d:T) S,V(iterX)? ? B?J --H
fro 11*): c * ALL(kj?(?(G' li21 L,H):
va d:VALU;
d * elenents of L;
XLS,V(iter')??? ? B??(c' f?o,, H*,H)
The values of L nust be assigned to the nawes of d since they
way be exawined by the jeplewentation of the aubgoal. G'
justifies B??? in an environwent where d has the values of L,
thus by the free nawe independence property discussed in section
4.2, G' justifies B in an environment and state where x has the
values of L.
--H151--H
X?<env> s.( 3 iterX)Bx ? c k?
<env.d:T> S.V(iterX)?.B? ? ci --H
?(G li2i H*.H):			d:VALUE;
d elements of H.VALS;
X?S?V(iter ??d Bx? ? ci(G from H*,?.J1.?.J2)
H.Jl and H,J2 justify V(iter1) and			when x has the values of
H.VALS, so they also juatify V(iterX) and when d has tha
values of H.YALS. Since C does not refer to d G justifies C
even when d ja des?located at procedure exit.
?synthesis
IL<env> S ? (?iter')B1 kz
<env.y:T> S ? y any iter1 li B1i --H
from B*): war
var y:VALU?;
xLs ? y * Aax iter1 ? B1i(G' from 11*);
SoME(y.G?.J.J1.G'.J.J2)
G' is an AND justification since it justifies VCiter1 ? B ).
The components justify V(iter1) and B respectively. in a state
where I has the values of y.
--H152--H
X?<env> 8 ? C ?
<env> 8 ? 81
<env> 8.81 ? 82
<env> S.B8n-1 ? 8n
<e?v> 8.8
? o+8? ? cJ --H
from H*): var Gl,G2Cn;
? 81JCc1 from ?t)g
xrs.81 ? 82?G2 from 8*.Gl):
xLs.83fl-I ? 80J(Gn Lr2i B?.C1
xLs.B? CJ(G from fl*?cjCn)
soecialitarign
XL<eov> 8			? c			?
?exp ?exp
<eov.x:T> S ? c ? --H
x			x
LrQm			var i:VALUK;
x VEexpi;
xE81 ?r CxJ(G from ?*)
Since ??5x ? Cx] has the property of correctly tranaforaing
extended justifications. it produces the desir?d result when
given Ha justifying S??? (a. discussed in aection 4.2).
ref1e??vi?v
X?S ? exp-exp] --H
li T<env>Lexp]--? th?
f,o Ha): G EQUIv(kj??(??(G' from u): 0' * li ?),
from H): 0' * H ??) end
from 11*): 0 * NIL() end
If the expression is boolean, say A. then build an Qulv with
two procedures for A?A. Otherwise. the expression requires
only the trivial justification.
avr'?trv
? exp2-exp1 ?
5 ? exp1?exp2] --H
li T<env>Lexp1J-? jllcIl
?:`(c froa Ha):
jtAt 0';
xLs ? exp1-exp2j(0' liLs Ht)t
0 * EQUIv(G'.JT2.0'.JTl)
f?cr? Ha); 0 * NIL() end
?Ls ? cxpj--4xp3 ?
s ?? ??1- ??2
s ? exp2uxp3i --H
li T<env>Lexp1??? then
fro 11*):
var Gl,G2;
Dr exp1?exp2J(C1 f?pm ut);
xLs ? exp2=exp3l(C2 frp? 11*);
G #			from ii):
c1.JTl(G'' f?om H);
G2.?T1(G' fro c'?)
from II):
G2.JT2(GIw fro? H);
Gl.JT2(G' from 0'').
lie
?CG fro B*)? 0 ? NIL() e?
-155-
snbati?nriqa
The rule 0 substitution is. by far. tba most difficult from
vbicb to extract. When an expreslion of a formula is replaced
by another expreasion of completely different form the
justification of the original formula must be internally
restructured to justify the new formula. This is accomplished
by replacing justifications of all occurrences of the original
expression by justifications of the new expreasion. A recursive
L procedure named SUB is used to perform this replacement at run
time. However because the recursion ia on the structure of
formulas. every invocation of SUB could be expanded in-line at
compile time. given appropriate concern for parameter passing
and local names.
-136--H
tL<env> s			? c
?exp1			?exp1
<any>			? exp1eIp2
<any> S			? c			J --H
?exp2			?exp2
li T<any>?exp1J--k?1 then
liQm
var GIGn.G'.G'';
XLS?exp1 ? exp1--exp2j(G1 fr? HI
Lli i;1 ? n ?
SUB(Gi fro S?x?Hi?G??JT1?G??J%)
)crs			? c			J(G'' fro SI			cn):
?exp2			x?exp2
sUB(c from Cx?G'#?GI?JT2?GI?JT1)
1Lgm Ha): XtS?eip2 ? C?+?axp2J(G fro? Ha) ?a
where SUB(C from F.J.JTl.JT2) takes a (boolean or
transition) formula 7 with free occurrences of I,
a justification J of F?j JTl mapping
justifications of el to justifications of e2.
JT2 performing the inverse mapping. and sets G to
a justification of 7?e2 (for any ei.e2).
If exp1 is not boolean then the aubgoal performs the desired
transformation. If e1p1 is boolean then ezp1e1p2 provides a
pair of justification transformers which are uaed to turn each
Hi into a justification Ci ni Si and G (?u?tifying
x?exp2
-157-
c			)			n justification of C			Tb p?ocodur? ua,
x??apI
o+?ti?fyin? a?ove stated properties. is defined 55 follows.
SUB --H			1iui Y.7.JTl.JT2):
li 7 doesn't contain x free then
c?J
L1a uu I
I			JTt(c f? J)
? SUB(Gl -? A.J.Jl,JTl,JT2);
SUS(C2 fro B.J.J2,JTl.JT2);
c AND(GI.c2)
AvB ? li J.SEL ??
SUB(Gi from A.J.J.JTl,JT2);
SUsCcl i?tQ? B.J.J.JTl.JT2);
G			oR(J.SL,fi)
A?B			? G			1MFL(??(?(G' ?r?
var Gl,C2;
SUSCcl li? A.H.JT2.JTl);
J.JT(G2 f?oa G?);
SUli(G' fro B.G2,JTl.JT2)
c ? zqulv(??(?(G' irms
var Gl,G2;
SUB(Gi f?om A.H,JT2.JTl);
J.JTl(c2 f?n GI);
1)8
su?(c' fro B.c2,JTl.JT2)
from ?)z
var Gl.G2;
suB(c1 from B,H.JT2.JTl);
J.JT2(G2 from cl);
sUH(G' fro A.G2.JTi.JT2)
(3 iter?)Ba ? sUB(Gl from V(iter ).J.Jl,JTl,JT2);
sUB(G2 f?o Ba.J.J2.JTI.JT2);
c ? soNE(J.vALs.G1.G2)
(Viter?? ? c ? ?L(?(?(G' fro L.H):
var G1.G2;
suB(c1 from v(iter?),N.JT2.JT1);
J.JT(c2 from L.Gl);
sUB(G' from Ba?G2?JT1?JT2)
a?? iterb sUB(c1 from V(itcr6).J.J.JTl.JT2)
G TRA?s(G1)
? G NIL()
else
eod case
li
--H139--H
4,4 ?traction? i?teeera and aeta
The generaL rule of arithmetic allow. any valid reaaoning about
aisple arithmetic relations, Since these relations have no constructive
meaning, the CItraction rule for arithmetic is trivial.
arith
xLS.B1Be ?			--H
?CG ?twa Ht): G ? NIL() end
The other rules of arithmetic have marginally more interesting
eatractiona.
tr?chqtomv
xLs ? exp<O v (expo v exp>O)? --H
?(c from He): c ? li vtexpj<O
then oR(?,NlL())
oR(li1a?.oR(vtezpJ-O.NIL())) end
I?S.ezp1?exp2 ? exp1<exp2 v eip1'exp2j --H
li2i H*,H): c oR(v?exp1?v?exp2J.Nlt()) end
XtS.ezp1?ezp2 ? exp1;exp2 V exp1>exp2? --H
?rom H*.H): G OR(VLexp1?-VUexp2J.NIL()) end
-160-
Consider. now a model for set theory in wbicb sets are represented
as non-repeating LISTs of VALUEs. The null set of any type is
represented by the list lULL(). xsS is tested by searching the
representation of 5 for an element that equals I (where two sets are
considered equal iff every element of one equals some element of tbe
otber, end vice versa). The set forming notation. (generator). can be
implenenred by describing how each form of s.e. generator produces an
object of type LIST, Finally. all set operations can be described in
terms of operations on LIST representations. In tl?ia aodel. it is easy
to extract from the set refinement rules.
a
xLS ? xsaii??(T)			?A1i?? --H
?(G from Ha): C EQulY(
liLLd(?(c5 liai H)r C' ? ?IL() ??.
?(??(c' fros 1): G' ?IL() ng))
Since xe???(T) cannot be true in tbs ssodsl. the
justification produced for false will ne?er be used. Sililarly.
no justification can ever be supplied for false so that
produced for xo??(T) will not be used.
-161-
?def
Ifs ? xs(genl			?(x:gen)? --H
1L? lg*): c ? EQtlv(??(?(G' ii):
JaeL?(x:gen)J ?).
liQm
? NlL() end ))
Given a complete description of the LIST representation for
(gen). one can show that V properly characterizes the elements
in the representation. Thus. in the model. x--H(gen) is
equivalent to V(x:gen). Given H justifying xc(gen). one can
conclude the truth of V(x:gen) hence Jae?V(x:gen)J produces the
desired justification. In the other direction H justifies
V(x:gen), thus xa(gen) is true. Recall (from section 4.2) that
its justification is altaply ?IL().
The remsining set axioms are clearly true in the suggested model.
Further since all set expressions are a.e. extractors for the
remaining set axioms say he constructed as shown above. using ?se to
produce justifications as needed. I leave this construction to the
reader.
4.5			R?t?a?tinn			snec.fcar,nns
The procedures extracted from transition specifications modify
their environient in addition to producing justifications. Recall that
-162-
the justification produced for x Snv iter5 is TRANS(J) where J
justifies V(iter5) in an environment and state in which a ja the new
value of x and x is the old value.
X?<env> s ? ?Xn ? anv a1texpan:expn2 --H
Ha):
G ? TlLANs(AND( .. AxD(Jae?s1expiJ.JaeLs2exp2J)....
JseUsnexpnj)).
Xn			VUexp1JVFexpnJ
The procedure evaluates the n expressions and aasigns them to
global variablexn. The justification produced is for
?(a1:expan:expn). that is. for Sl=CXPIA???Asn=expn which
Is associated left to right. For each non-boolean expression,
the corresponding coaponent of G is NIL(). For the boclean
expressions. s?exp? is treated as a??exp? and an appropriate
justification produced. G is computed before the new values of
x are assigned. since the components of G may reference the
original values of I.
-163-
X?env? 5 ? x * any ateexp ?
<env? 5 ? ex??(T)? --H
from H*):
I * V?exp3.HD.
G * Tws(NLL())
Once the subgoal is established. exp is known non-empty. i.e.
VLetpJ is not NULL(). Thus. the HD component exists and mey be
asaisned to x. The justification for V(a:eexp) is NIL() since
V(a:eexp)?aeezp.
Xt<env> 5 ? I * any iter5 ly
<eny> 5 ? V(iter5)????? --H
?(C liQi H*):
irs ? V(iter5)5?J(G' from Ha);
G			Tws(G')
Since G1 justifies V(iter5)5?1 by free name independence. 0'
justifies V(iter5) in any state where a has the same value as x.
Therefore. since the new value of x equals the old value of x
01 justifies V(iter5) in a state where a is th? n velo, of a
and a is the old value.
-16?
ajanlif,catjpn
X?env? S ? x * fly itera ?
<env>			S ?			sny iterib
<env.b:T> S.V(iterlb) IL V(iter5)??J --H
?(G f?o+ Ha):
var Gl.G2;
var I'.h:VAUIE;
I'
I?s IL I * 5'v iterlbj(Sl frog Ha),-
b
I *
X?S.?(iterlb) IL V(iter5)?J(G2 igise
G			TWs(s2)
Cl justifies V(iterlb) in a state Ihere b is the 0ev value of I
and I is the old value. that La, in tbe state active vhen the
second subgoal's procedure is invoked. C' justifies
V(i?er5)a*? or again by free nage independence, V(iter5) vhen a
has the same value as b (vhich is the 0ev value of i) and I has
its current value (vhich is the old value of i). Thus, after
reaturing tlie n?? value to I, C is the desired result.
?L<env> S ? z			any itera bt
ili yst
<eov.7:T) S ? i.y any iter?.b:T? --H
li2i Bt)
1u y:VALUE;
x?s ? x.y ? ? iter?.b:T?(G? from Ha);
c G'.J.Jl
e?A
G' is a TRM?s(&ND(-.?)) whose J.Jl co?ponent justifies V(iter5)
in the appropriate state. The declaration of y is accessed
according to conventionaL static scopiog rules from the interior
atracted procedure.
cpm?pa??pn
xL<env> s ? any it?ra ky
<eny> S ? q11
<eny> ?1 ? x any iterlal
<env.a1?T> s.v(iterl'1) ? ?2?ai
<eny> Q21 ? x ? any iter2?2
<env.ai:Tan-1:T> S.v(iterlal).v(iter2?)?a1
an-i
o+...V(itern-i			??an-2 ? Qn?an?i
<eny>			Qn1 ? X			AiLX iternan
al			a2
<env.ai:Tan:T> s.v(iteri ).V(iter2
? VCi?er )			J --H
....vitern??)?an-1			a a?an
feom Ha):
yar Gi.GI?Gn.Gn?.C?;
ia aO.alan:VALU?;
aO
xLs ? Qi1J(Gi frpa Ha);
xLqi1 nr I any iterial
?ci' fron GI);
al I; x
XES.V(iterial) ? ?2??ai??? fro Ha.Gl'.J);
I al;
xLq21 ? I any iter2a2?G2t f,nm G2);
a2			x;			I ? aC;
an ?			I ? aC;
--H167--H
X?S.V(iterl51).V(iter252)?51
..?V(itern50)?an?1 ? ?(iter5)?an?
li2i ?*.Gl'.J.G2'.JCn'.J);
x an;
c Tws(G')
Bach ai records the value of x after executing the extracted
procedure for Qi1 ? I 5?? iteriSi. The original (old) value
of x is aO. The first aubgoal produces Cl justifying Q11. The
second aubgoal produces Cl' with Cl'.J justifying V(iterl51) in
a state where al baa the new value of x and x has its original
value. The next two assignments create this state so that C2
juatifies Q2?al After the next assignment. by free name
independence. C2 justifies Q2x and C2' is created with G2'.J
justifying V(iter252) in the appropriate state. This process
continues until C' is produced justifying V(iter5)a?an The
final assignments set I and C to the desired results. By free
name independence. G.J justifies V(iter5) when a equals an (the
new value of x) and x has its original value. in programs
extracted fro. real proofs. adequate information on the
intermediate values of x is often supplied by the Gi
justifications alone. so the inte?nediate ai variables are never
accessed. in these cases msny of the variables and assignments
introduced by this rule may he eliminated using the
optimizations described in section 4.7.
-168-
X?<env> 8 ? x ?			itera b:
x ? an' iter? AL tj+ while
<env> S ? anv iteri
<env.i:T? S,V(iter1) ? BiY?Bi
<env.i:T> S.V(iteri).3i ?
<env> ? AlLX ittr2b
<env,i:T.h:T> S.V(iter?)?Bi.V(iter2h)?j
V(iter1)i?? A ti?<ti
<env.iT> S.V(iter?)?tisO ?
<env,i:T> S.V(iter').?B ? V(iter?) .J --H
I			a*i
fig Ha):
ALL Ci,Gi'.Ch,Gteat.fq.C';
ALL xo.i.biVAWE;
xc *
xLs ? x * anv iterLj(Ci liq Ha);
Ci Gi.J;
i *
x * xC;
? /a invprlpnr V(iter?) La :uatified by Gi in the preaent
state, i has the new valiie of x, and z has it.
originni value t?
XLS.V(iter ) ? Biv?BiJ(Gteat fig,, Ht,Ci);
e?it IL ?,CLeat.SEL;
x(s.V(iter1
)?Bi ? (Yi??? li2i Ha.Ci.Gtest.?);
XLQx ? I * B?? iter2h?(Ch frgn Cq);
169-
b ?
I iC;
I?S,V(iterL),8i,V(jter2b)???? ? V(iter?) At <t J
i?b i?b i
(Gi' fro ?*,Ci.Ctest,J,Cb.J);
Ci Ci1.Jl;
i?b
tTS?V(iter1)??Bi ? ?(iter?)a?i?(C# frn,, H*,Ci,Gtest,J);
I ?
C ? TRANS(C')
end
The original value of x is kept in xO. After the initialization
transition and subsequent three assignments, i has the current
value of x and I has its original value; thus, Ci justifies
V(iter?) and the in?arjant holds initially. The body of the
loop produces Gtest which tells whether B or ?,1. is true and
the loop is exited if ???i' Otherwise Oq justifying ???? is
created. I is restored to its 5current5 value, and with Cq now
justifying Q1 (by free name independence) Cb is produced with J
component justifying V(iter2 ) in a state where h is the new
value of x, This state is achieved by the next two assignments.
Then Ci' is rreated snd Ci is set to the part justifying
V(iter?) in a state where i has the value of b, i,e., the newest
iteration result. The last assignment creates this state so the
invariant holds again, When the loop is finished, ?B? is
justified by Cteat,' and i,x have the new,original values of I,
--H170-
respectively. C' justifies V(iter5) thus after x ? i I has
the desired final value and G.J justifies V(iter5) in a state
where a has the new value of x (i.e.. i) and I baa the old
value. Note that the proof of termination is necessary to
insure that the extracted loop terminates, but it does not enter
into the extracted code.
4.6 Extraction-. definitions Iii leiiiiaa
Extraction for abstractions is heavily based on the ideas used in
the rules of specialization and substitution. Since all actual
parameters of abstraction invocation, are a.e., their binding to formal
parameters is similar to the binding that occurs in the specialization
rule.
Consider an instance of the simple form of definitions:
def D(b:T) --H SXPb
If e?p is a.e. then any iuvocation, 0(e). is also a.e.. In this case. v
and J must be extended to cover this form of a.e. expression. ?0(e)J
is defined as V?eSPb.?va?e.tJ and Jae?0(e)J is defined as
JasEexPh.1va?e.t1 where `?var?t5 is the composite substitution
resulting from parameter matching (described in section 3.8). If sIp is
not a.e. then no invocation of 0 will ever be directly evaluated.
rather. proofs involving 0(e) will reduce the calculation to a
combination of a.e. calculations (just as with other non-a.e.
expressions). However, justifications of 0(e) may be manipulated
whether 0(e) is a.e. or not; as 0(e) is considered an abbreviation of
55?b.?va?e,t' the justification of 0(e) is identical to that of
-171-
CXPb.?var+e.t Thui the extraction rule for siaple definition
reference is trivial.
XES?D(e) 2L C?D(e) It
?xph.?var+?e t
Lt:s Ha):
c			-
?xpb.?var+?e.t
XUS?xph.?var+?e.t ?			J(G li21 Ha)
end			X+?eXPh.?var+?e.t
Next. consider an instance of the more complex form of definitions:
def D(b:T) --H the iterX
<y:TI.envr>			? 7 ? AILX iter?X
<s:T??y:TI????I> V(iter?).V(iterx)
h			b ?y ? x-y
Since this definition provides a means of computing the result for all
inYncations it is always s.e.. In addition to providing the value
satisfying the iterator the definition must yield a justification
supporting that claim. This justification is provided hy the first
proof of the definition hody. Thus. for each complex definition.
construct an L function DL as follows:
--H172--H
liA D?(b:vALuE) eet,,rns (VAL:vALuE.JtJtisT):
var y:VALUE;
Y			ilf iterbx?(G li?;
return
The value function V may be extended to complex definitions: V?D(e)J
means D?(v?e2).vAL. The J component of DL is used in the definition
reference rules presented shortly.
An invocation of a complex definition is not an abbreviation for
the substituted body. The justification for D(e) is simply ?lL() This
difference between simple and complex definitions arises because all
needed justifications are provided in full by tbe latter. while the
former (not necessarily being a.e.) rely on juatifications of D(e)
provided by the user of the definition reference rule.
The rules of definition reference for complex definitions are abovi
below.
definition evaluation
xLS ? V(iterbX)x.b.?vsceD(e)se.tJ --H
liQin Hs):
G DL(VLei).J
Since c juetiiies V(iter?X)? by free name indcp?ndence (as
iJ.3--H
used in specialization) and the observation that type names
never affect the code -titracted from a proof. C also justifies
V(iterXb)x.b,?var?(e),e.t
?efr,o+?,rip uni
It C?D(e) ?
S?D(e) It V(iter5)
b s.b.?var*exp.e,t
e			It C			J --H
?exp			?eip
li T<env>LD(e)J--iu??1
from HIHn):
v?r GiGn.Ca.Gb,Gc.Gd;
lIt b.x.y:VALUE;
It V(itSr'b)x.b.tvar?exp.estJ
(Ga fro" HIHo);
b * vEeJ;
x V?expJ;
y ? D?(VLe1)?VAL;
Gb			D?(VLe?).J;
x?v(iter?)?V(iter?X)? It xyJ(Gc fro Ca,Gb);
lIt i:I ? n ?
St?y(Gi from S?y.Hi.Gc.JT2.Gc.JTI)
ii;
1?S?exp It C J(Gd from GiGn);
?e?p
SL'By(G from C ,Gd,Gc.JTl .Gc.JT2)
?It(G li2i Ha):
-174-
x?s			? c			?C fron Na)
y?exp			?exp
Thia extractor is very siaiiar to that for substitution; there
are two asin differences. First SUBy is a version of tUB that
looks for occurrencea of y rather than x. Second. producing Cc
juatifying exp=D(e) requires more work as fcllows. The first
aubgoal is uaed to create Ca justifying
v(iterhx)x.b.?var?exp.e.t Then Cb is created justifying
V(itechX)x.b.?va?D(e).e.t Finally. a buiit?in use of
specialization produces Cc from the definition?s uniqueness
suhproof (the second one). by creating a state where b is a x
is exp. and y is D(e).
Extraction for lemmas is a good bit simpler than for definitions.
For each leuna
lin:ig L v:VT(b:BT) --H s ? c
v.b v.b
a L procedure is created:
--H gL1l(C.v:VALUE from 11*.b:vALUE)t
ur C ?C from H*)
This is the only instance of a procedure in which the variables of v
might be both referenced and assigned to by the body. The procedure is
used as in specialization. in the following extractor for lesasa
references.
17,--H
xts			kx
v.b.?var??,e,t ? v.b.?varsn.e.t
L n(e)J --H
LLQi
li2rn
Since the invocation of is call by reference on n and call by
value on VLeJ. the lemma body (computing from inside LL) can
treat v. b as variables and fixed values, respectively. as it
assumes it can. As mentioned earlier, the substitution ?va?t
is of no consequence since type names have no effect on the code
extracted fros proofs.
4.7 ?xamnle eitracrions and onti?jzat;on
T?ro example extractions are presented below together with the
application of several code optimization techniques to the extracted
procedures. (See (Ah? and UlIman l973J for an overview of code
optimiLation techniques.) Unfortunately, the extreme tedium of
extracting by hand (and reading extractions) has forced me to severly
restrict the size and number of examples considered. Though most of the
extraction rules are not demonstrated. this section is still quite long.
As I have mentioned previously. PRL can only be feasible wit') machine
support; it is not designed for paper reafioning. ?xtraction is an area
where this is most apparent.
-176--H
The need for optisi?ation is notivated by the first exaiple. a
simple proof in pure logic.
Example 1: ( 3x:i?P??Q ? (Vx:?)(Px?Q)
This is a refinement schema vbere P and Q are arbitrary boolean
expressions. Each proposition of the refinement is labeled for
reference from the extraction.
I)
2)
3)
4)
5)
6)
7)
8)
9)
10)
II)
12)
( 3x:?)Px?Q ? ( Vx:?)(P??q) Ig Vs
? ?d?? ?
( 3x:li?)Px?Q???P? ? Q ? ?a reordered
( 3x:????)Px?Q?inls??P? ? ( 3x:in?)rx ? 3s
(3X:?)Px?Q?li1??P? ? y lax x:liL AL ?x ? cons
( 3 x:?)Px?Q??L??P? ? Y lax b:d			It ae
( 3 x??)Px?Q???P??b=d It It&tAPb			It As
(3x:ii??)Px?Q?liw??Pd?bd It r??e It true def
(3x:?)P ?Q?P
x			d.bd It ?b It subst
3 x:?)Fx?Q??.P?.bd It b--d			It assum
3 x:?)Fx?Q????P??bd It ?d			It assus reord
( 3x:?)P??Q.?.P?.( 3x:?)??.Q It Q It assum
The extracted procedure is displayed with each line annotated witb
the labels of refinemet-ta of ?hich it is a part. Thia information is
similar to the nestin? level nunbers provided by some compilers.
--H177--H
I shall not pro?ide a step by 6tep description of the extraction
process, but the sotivated reader `aill see t?at it is a purely
sechanical application of the extracti?n rnt?n.
I			?(c li2i Hi): G			ALL(?(?(G' LQiL
1			? d:VAU;E;
I			d
1 2			?(C from Hl.H2):			G ThFL(ki?(?(G' fr?'s II):
1 2 3 fro H,Hl,112):
1 2 3			vsr Gl,G2;
1 2 3 4			frrom			Hl.H2,a3):
I 2 3 4			vsr
1 2 3 4 UL y:vALuE;
I 2 3 4 3			fro Hl.H2.H3):
I 2 3 4 3			?ar			Cl.G2;
1 2 3 4 3			??			y',b:VALUE;
1 2 3 4 5			y'
I 2 3 4 3 ? ?:t:i(G fro Hl.?.R3):
123456			G TR&Ns(NIL());
123436			y*d
1 2 3 4 3 6
1 2 3 4 3			(Gi from lil?H2,H3):
I 2 3 4 3			b
1 2 3 4 3			y ?
1 2			3 4			3 7			?(G from Hl,?f2.H3.H4):
1 2			3 4			3 7			var Gl.C2;
1 2			3 4			3 7			8			?(G			H1.H2,R3,H4):
-178-
1234578
1234578
123437
1234579
1 2 3 4 5 7 9 11
1 2 3 4 5 7 9 ii
1 2 3 4 5 7 9 11
1234379
1234579
123457
123457
123457
12343
12345
12345
12345
1234
1234
1234
123
123
1 2 3 12
1 2 3 12
1 2 3 12
123
123
12
G NIL()
end
from N1.?2,H3.H4).o+
from Hl.H2.)i3.U4):
liaa HJ.H2.H.R3):
C?B
e?d
li2a 81.ll2,83.U4)
(G2 from
G AND(Gl.G2)
end
(G2 from Hl.B2.1I3.Cl.J);
y ?
G ? TRANS(G2)
end
(G1 from N1.U2,H3);
G SOME(y,G'.J.J1,G?,J.J2)
end
(Gl ? H,H1.H2)
1I.JT(G2 from Cl);
from li1,B2.H3.H4,8)?
C?H
end
li21 1i.H1.H2.G1.C2)
end
from Hl.h2.H)
-179-
I 2			end ))
I 2			end
I			CG' li2i )?11,u)
clearly. the above procedure is subject to massive improvement the
most obvious suggestion is to expand procedure invocations in-line with
suitable renaming of variables to avoid conflicts. This optimization
results in the following code.
f-nm R1)?
c * ALL(kin?(
?(G? f-? L.H):
? d:vAUJE;
d * L.HD:
?(c'a lini 1):
ili cl.G21
vAg G'b;
var y:vALU?;
var Gla.G2at
var y .b:VALU?;
Cia * TRA)?s(NlL())I
y *
b
480-
y ? yf;
v?r Glb.G2b;
Gib			NlL();
C2b
G2a			AND(Glb.G2b)?
C'b TRANS(G2a);
GI soME(y.G'b.J.J1.C?b.J.J2)?
Hl.JT(G2 wi Gl)?
G?a			G2;
Yrom this it is apparent that elisinating chain assignments,
propagating ?nown expressions. removing dead variables. and removing
dead code could substantially 1sprove the extracted procedure. These
optimizations yield the text below.
?(G from HI):
G *
?(G' liai L.H):
G'
from Ha):
?pr GI;
HI.JT(C'n			Gl)
-181--H
This procedure nicely captures the senantics of the original
formula. ( 3x:??Px?q ? ( Vx:i??k)(P1?Q). providing a justification
of the conclusion in a clean. direct aanner. This is the sort of
5obvious5 extracted code I ap??e of in section 4.1. It seems that the
code produced by the extractor is so einple and highly structured that
these basic optili:ationa are extremely effective.
The second example is the proof of a specification for an absolute
value program. It demonstrates the extraction of procedures that change
global variables.
Exanpie 2: ? x ? any a:abs(x)
1)			?			x anv s:aba(x)			bg cons
2)			? x<Ov(x-Ovx>O)			by trichotony
3)			i<ov(x-ovx>o) ?			x anv a:aba(x) by Va
A) x<? ? a any a:aha(x)			by cons
3)			x<O ? a			any b:-x			by SC
6)			a<O.b--a			? b-ahs(x)			by arith
7)			xaovx>O ? a			? any s:ahs(x) by null
8) xOvx>O ? xaahs(x)			by va
9) xaO ? a-o+abs(a)			by arith
10) x>O ? x-abs(x)			by aritb
-182-
Tbis proof yields tbe following extracted code (again. by
?ecbanical application of tbe extraction rules).
1			var
1 2
1 2			G li x<O then oR(?.NIL())
1 2			nAa
12
13
13
134
134
134
134
1345
1345
1345
1345
134
1 3 4			b			x;
1 3 4			x
I 3 4			6			?(c from H1.H2):
I 3 4			6			G ? NIL()
1 3 4			6			ena
I 3 4			(G2 li2i H1.CI.J);
end
(Gl liQm)
from H):
li H.SEL then
?(c from 81):
vAt C1.G2;
vAt x'.b:VALUE;
li2a 81)1
c			TRANs(NIL()):
(G1			Hi);
-183-
134
134
134
13
13
137
137
1378
1378
13789
13789
13789
1378
1378
1 3 7 8 10
1 3 7 8 10
1 3 7 8 10
1378
1378
1378
137
137
137
`3
13
`3
z ?
c TRANs(c2)
end
(c li2l H.J)
liQrn H1)i
var G';
from H):
li H.sEL then
fro? u1)?
G NIL()
end
lial
f?om HI):
G NlL()
end
H.J)
li
end
fro. HI);
C Tws((;')
end
H.J)
li
end
ligi cl)
-184-
Expanding procedure invocations in-line:
?(c li?):
var CIt
Cl li x<O ?hen OR(???.NIL())
A1u OR(li1i?.oB(x-O.NIL()))t
li Gl.sEL ?hem
var Cla,C2a;
? x'.b:VALUf;
x1
CIa TRANS(NIL());
x -I;
x I';
C2a
x *
C ? TwS(C2a)
jL Cl.J.S?L?
NlL()
elee
li;
G			TRANs(C')
-183
luaiaating cbain assig?ents, Propogating known expressions,
reloving dead variables. and reeoving dead code:
?(G li??):
IA' Cl;
Cl			li x<O then ORC?.NIL())
el.e
li C1.s?L then
C			Tws(RIL())
111
IA' C';
li CI.J.sEL th,
li
NIL()
li;
C ? Tws(c1)
?ly:ing the IL stateaents with fundamental data flow analysis
techniques, this can be reduced furthers
-186-
?(G ?):
li x<O ?hen
X ? -x
lit
C ? TRANs(NIL())
Thus optimizing the extracted procedure is again extremely
worthwhile and yields the 5obvious5 implementstion for the originsi
specificstion.
CRAPTgR 5
CONCLUSION
5.1 Summarv
There are three areas in which ?gL?? conceptual foundation
crucially differs from those of conventional programming languages and
logics. Firat, the logic supports reasoning about specifications5 not
programs. Second. complex texts are structured as formal hierarchies.
maintained and manipulated with machine aid. Third. program
specifications and logical formulas are uniformly treated according to a
constructive interpretation. These ideas form a base to which I have
often returned during the development of PR?. They are the essence of
this work to be retained and contemplated prior to any technical
detail. I expect this triad to drive further work on refinement logics;
therefore. each constituent shall be summarized in some depth.
Computer scientists in the areas of programming languages and
systems have long believed that their raison d5etre is to cause machines
to exhibit specific behaviors. This view. though partly true. is highly
misleading. When accepted uncritically5 as almost always occurs5 it
leads to the belief that executable code is the programmer's prime
concern. Programming languages are considered notations for commanding
action in the nachine's vocabulary. hence the programmer5s main task is
-187-
-188-
termed 5coding5, The entire yield of tbe programming process is tbe
completed executable program.
In reality. the executable program is a relatively minor by-product
of the creative effort and complex reasoning typicall7 involved in
solving programming problems. The vast bulk of effort is expended in
understanding the problem, investigating possible solutions, determining
the solution of choice. and developing the details of the solution in a
comprehensible fashion. This spectrum of reasoning takes place most
conveniently at varying levels of detail in the world of specifications.
Since this reasoning constitutes the major effort of program
development. our prime concern should be to facilitate its correct and
timely completion. Concentrating instead on executable text ia a
critical blunder.
It should not be inferred from the above that conventional
programming languages are totally miadirected. Some situations do
require direct access to machine facilities; further, there are people
who justifiably study concrete algorithms, asking questions like o+what
happens if I change this line of code?". Nost programmers, however. are
engaged in converting specifications to machine behavior, These
individuals need a logic for clearly and naturally reasoning about
specifications, not prograns.
I am arguing that programming should be viewed as a particular
variety of applied logic. A logic that leads not to asserted programs,
but to th constructive, hierarchical proofs about specifications
ea.mpliticd by FRL. Tht validity of this view is subject to debate, yet
189
I believe the arguments in its favor are f snifirient merit to warrant
considerable further explorati?9 of its ?nus??uencca. Even now. one
inuediate consequence seems not?wortiy. since we should not be
constructing purely executable texts. neither should we be verifying
thai. Observation of work toward practical verification of large
prograuas scais in accord with this conclusion.
The second conceptual foundation of PRL is the interactive
development of formal. hierarchically structured proofs. It has been
noted that complex objects are most easily constructed as a hierarchy of
stable components lAlexander 1967]. Refinement logics embrace this
observation in its entirety (perhaps a bit too warmly) by organizing
proofs as trees with all intermediate goals fully specified. Unlike
conventional progranmiog langua?es. the refinement logic notation
superbly supports top down development and testing (for aptneas) of
proofs. Even the novice progranmer would understand the utility of
these methods if trained using refinement logica.
The highly structured proofs of PRL are in marked contrast to the
linear proofs of mo?t existing logics. When a system of reasoning is
designed. the decision merely to write and manipulate proofs on paper
exerts considerable pressure to mold the logic around the linear. static
nature of the medium. Otherwise. the system will be impractical. Until
recently. of course. there was no alternative, but the advent of
Inexpensive. interactive. personal computing systems liberates logicians
to consider methods of symbol manipulation not feasible on paper. It is
vital to realize that interactive computing systems are as much a part
of these logics as paper is of conventional logics.
-191-
These new prograeming logics and their supporting ?ystems may bring
(computer aided) correct-program technoingy to the real world. Clearly.
this depends on constructing habitable facilities for the experienced
user. PRL is my first attempt to build a logic from the new
foundations. I would compare it to FORTRAN. or some lesser known early
high level language. in that it is unlikely to be a prime example of it.
genre. PASCAL is so superior to FORTRAN because the designer had the
experience and conviction to ignore many of the considerations that
influenced FORTRAN's design. while concentrating on other aspects whose
importance had become known. I have little doubt that my programler's
background has retarded my progress in developing PRL; too many
assumptions had to be forgotten. However. I have a correspondingly deep
conviction that. with the requisite practical experience. a truly ?sable
logic and support system can be developed from PRL'a basic ideas. The
significance of interactive systems as a new medium for proofs is worth
serious thought.
The final conceptual foundation of PRL is the use of constructive
reasoning to unify the treatment of program refinements and logical
proofs. This is perhaps the most radical of the three fundaments.
Further, it is the one of which I am least sure.
With conventional logic.. verificatiom text is physically and
conceptually dis3oint from executable text (even if they are
interleaved). This encourages the programmer to view verification text
as of doubtful utility. even as some sort of parasite that accompanies
the construction of correct programs. This attitude is reflected in
attempts to minimire the ratio of proof to program apparent in recent
-191-
work on autonatic verificati<,n. Sucb effort (for its own sake) is
misguided because it ignores the actuality that the proof. rather than
the program. is the significant product of development.
Supplanting a programmer's 5praise the code5 attitude with one of
concern for the lucid expreasion of developmental reasoning requires a
unified logic of correct program development. There must be no
distinction between program and verification; no portion of the text may
be branded ineasential. This ensures that creative effort takes place
within a single conceptual framework. the framework of vslid proof
construction. The machine is left the task of deriving executable code.
the programmer is able to concentrate on building the clearest possible
proofs. and the refinement logic designer is freed to aid the programmer
by examining a broad domain of proof styles far beyond the scope of
programming languages intended solely for execution.
Adopting a constructive interpretation of formulas naturally leads
to a unified logic. As chapter 4 demonstrates. the operational content
of PILL proofs is widely distributed throughout their texts. yet it may
be extracted and optimixed into efficient conventional code. Whether
the constructive approach is feasible for real users. or whether some
more palatable means must be uncovered to achieve similar results. can
be determined only by practical experience. There is no doubt. however.
that constructive reasoning unifies the logic admirably. As with the
two preceding basic concepts. this one should be the subject of
additional inquiry.
-192-
In concluding. I should mention tbe importance of the logic
developed in chapter 3. PRL is a useful case study. It concretely
illustrates the ideas of refinement logics. demonstrates by construction
that they exist. and provides a wealth of technical detail about a
particular logic. Nost significantly. it is lacking in a wonderful
diveraity of ways. pointing to a co?ensurate range of topics for
further research.
5.2 Ideas for future research
Ny ideas for future research roughly fall into four categories.
There are those pertaining to the specification language. the reasoning
system. extraction. and the implementation of an interactive program
development system. I shall address each in turn.
The majority of this thesis concentrated on the formalization of
the refinement concept. The notation for specifying program segments
was developed just enough to allow formulation of an interesting logic.
In a practical system. the perepicuity and succinctness of
specifications is a major concern. for their readability directly
determines one's confidence in their aptness.
The obvious extensions to the specification language include
additional types. recursive abstractions, and a more powerful set
theory. Earley has described powerful imperative and applicative
facilities based on sequences. mappings. tuples. and sets together with
iterators and reduction o?erstors (like +? in APL) Etar?ey 19?4a]
These mechanisms allow him to express a complete Lk(l) p??? t?ble
193--H
generator as a relatively straigbtforward applicative e?preasion (Earley
1974b1. ?is ideas have been directed toward creation of a very high
level language; while valuable. auch additional thought is needed to
integrate thee into a logic. Constable has made progress toward
developing a constructive set theory (Constable 1979]. but here. too.
such vork reeains.
The power of isperative pTogramming languages is due. in large
part. to the idea of wsr?bles and assignment statements. These permit
a single name to represent different values at different times with no
change of environment. It is precisely this power that complicates
logics of assignment beyond pure logics (such as the predicate
cslculus). These complications appear in PltL as the multiple
substitutions that are prominent in the rules for refining transition
specifications, I see these substitutions as exceedingly unpleasant and
have two ideas for developing logics where no name represents both old
and new values of a variable.
The first idea is to revert to a pure constructive logic without
assignment. E?preaaions denote values. predicates characterize values.
and existentislly quantified formulas are values packaged for later use.
Since unique names must be introduced with each 3analysis. this logic
is equ?valeot to a single assignment language. i.e.. one in which each
variable is assigned only once EKing 1976. Ashcroft and Wadge 1973).
This idea has been considered before (Constable 1971]. but mostly by
logicians with little knowledge of code optimization. Given such
knowledge. the extractor might be made sufficiently smart to re-use
variables when possible. e.g.. in loops. thus yielding acceptably
-194-
efficient programs. The extraction process for PRI already introduces
and subsequently removes so many variables that adopting this extreme
approach may hardly affect the final code. yet it considerably
simplifies the proof system.
Ny second thought concerns an extension. rsther than a restriction,
of the specification language. It would be veil if specifications could
be reasoned shout directly, without first using V to translate to the
predicate calculus. Perhaps the specification language could be forsed
as an algebra with operators for combining specifications and axioms
relating specifications. For example, consider the following
specification for a sorting program.
(swap(A.i.j) where lSi?j?)a n ordered(A)
This is a generalized regular expression describing the legal sequences
of operations that may be performed on A. It might be thought of as a
variant of a predicate path expression (Andler 1979), Also, it may be
considered as locally defining an abstract data type. say, `sortable
sequence5. Any legal refinement of this specification may perform only
swap operations on A, other operations may be forbidden by automated
syntactic examination. Thus, the user simply proves that the parasetera
to swap are always acceptable and A becomes ordered. Because the
permutation concept is captured in the sequence of legal operations. no
reference need be made to the old value of A.
I do not know the details of this specification language. I do not
know when reference to old values can be eliminated by this technique,
nor do I even have a good semantics for specifications (e.g., are
sequences of operations equivalent to swap acceptable in refinements?).
-195-
Nonetheless. I find this example sufficiently intriguing to justify
further examination. Reflection on the relationship between this idea
and Pratt5a factIheuristic dichotomy might well be valuable tpratt
1977).
The second category of ideas for further research concerns the
reasoning system. Again. several obvious extensions come to mind.
Clearly. a method for handling computation errors. such as division by
zero. ia needed. This is really the proble? of partial operators that
arises in logic. I spent 4uite a while trylog to develop a theory of
non-deterministic expressions. e.g.. any i:l ? 0 ? AEi]-x. with
limited success. Such a theory could incorporate erroneous expressions
by declaring partial operators to be defined. hot maximally non-
deterministic. where they would otherwise be undefined. For example.
a'b is deterministic unless b=O in which case it may yield any value
(of the appropriate numeric type). This technique avoids introducing an
undefined value by limiting what can he snown St proof time about the
values of expressions; if any echitrary result is not acceptable then
one must prove the operation well-defined. Also. it leads to efficient
extracted programs (roughly. the code is allowed to return "whatever is
in the register5).
A second ohvioua extension would permit the refinement of
constructs other then transition specifications. Expressins. types.
and iterators are all subject to hierarchical development. An
expression might be refined as a program segment (with no global
assigoneots) followed by a return statement. Types sy he tef Lued in
accordance with the latest theories on abstract data types. Iterat?rs
-196-
could be used as specifications for the coroutins-liks iterators of CW
(Liskov et.al. 1977).
The choice of transition specification refinement rules for PIL was
based on a well known result of BoIm and Jacopini that any control
structure can be formed as a composition of sequencing. selection. and
unbounded iteration IBohas and Jacopini 1966). This is sufficient to
assure theoretical completeness of the refinement system. but leaves the
question of naturalness i.e.5 practical completeness. open.
Progra?ers often choose refinements based on aquired knowledge of
techniques for programming specific problems. These techniques. such as
binary search heapsort. and dynamic programming. are seldom expressed
ahstractly. yet they certainly?form a powerful set of refinements for
decomposing specifications in a natural way. A good logic should
facilitate reasoning on this level to the greatest extent possible.
while continuing to assure the reasoningvs correctness. Thus. means for
achieving this should be explored. It is possible that an effective
mechanism for introducing derived rules would allow development of a
refinement rule library capturing useful programming devices.
My final thought on the reasoning system deals with methods of
increasing one 5 confidence in the sptness of specifications. ?srlier
I wrote that the latter was ultimately dependent on their readability.
Though this is fundamentally true. higher level reasoning showing5 say.
the equival of two independently formulated specifications. can
substantially rai? ne 5 confidcnce that a specification correctly
capI int itt i?n. Therefort the re?son?og system
should `,tvidu for pto'???L proptrties of specifications. `ther tlian
-197-
refinement properties. Presently. I have no ?ugg?atinns in this domain;
however, Cartwright's work ?n typ?d LiSP may prove quite applicable
(Cartwright 1976).
The third category of ideas for further reaearch concerns
extraction. ?xtraction is a variant of compilation that has not been
widely studied. Though intuitinnist logicians have certainly been
concerned with techniques for deriving mechanisms from proofs. the
economy of those techniques sod of the resultant mechanisms has had
little importance. Compiler designers. of course, evince the utmost
concern for compile time and run time efficiency. Thus, extraction of
programs from proofs, incorporating ideas from both disciplines, may be
a fertile area for joint research by theoretical and applied computer
scientists.
The simple optimization methods applied in section 4.7 seem
remarkahly effective. I believe that an interesting optimization
theoren might be established of the forn 5if a proof makes no `nasty'
use of old state information then extraction with optimizations A. B,
and C yields `good' code'. I would take `good5 to mean that the code
uses only variables specifically declared (in some instance of the var
rule) in the proof. The set of optimizations together with the precise
meaning of 5nasty' remain to be determined. Such a theorem would
formalize the belief expressed in chapter 4. that 5good5 code should he
derivable for sany proofs. in any case. I would expect the study of
optimizing extractors to be both interesting and valuable.
-l98-
The final category of idras for future research concerns the
implementation of an interactive program development eystem (lPDS) for
FRL. As I have argued, such a system is essential for practical use of
tbe logic. However, a conventional, hacker-designed system (using
5designed5 loosely) could easily render PEL more cumbersome tban it is
on paper. The high volume of text being manipulated truly necessitates
a properly human engineered interactive facility.
Environments and pre-conditions often flow down many levels of
proof trees without change. Since this is a trivial manipulation of
much text, it is important that the IPDS handle these flows
automatically. In addition, since the user is generally aware of this
information. it should not be displayed unless specifically requested.
Automatically flowing and selectively displaying environments and pre-
conditions is a simple, yet significant, activity of an lPDS.
Automatic and semi-automatic reasoning is a broader area cf lPDS
research, Though a fully detailed proof should be available to the
reader of a development, the writer may benefit by leaving obvious
inferences to the system, Some minimum degree of system competence is
probably required for practical development (e.g., arithmetic reasoning,
handling of equality), Much existing work on automatic programming,
theorem proving, etc,, undoubtedly could be employed here.
Semi-automatic reasoning, as supplied by the LCF metalanguage
(Gordon et,al, l977a], lets the user write proof finding procedures.
called tactics. These tactics examine goals (i.e., specifications) for
occurrences of various patterns, then suggest usa of appropriate
-199--H
refinement rules to generate new suhgosls. Tactics asy be composed via
tsCrics?s into complex heuristic provers. The LCF group reports some
interesting successes witb their approach. A metalanguage of this sort
might be appropriate in a refinement logic IPDS.
These concepts may be useful for automating some of the work of
proof development: certainly. the programmer will appreciate any
available aid. ?owever for the immediate future. the progrsmmer will
be performing the creati?e work. not the machine. The programmer must
he trained in methods of constructing solutions to complex problems.
with tbe requisite understanding of the limits of human ability and the
attendant implications. The machine must he able to see the
programmer's reasoning unfold and assure its validity. People and
machines continue to have complementary strengths. Refinement logics
together with their vitalizing interactive program development systems
are an attempt to mold the computer's strengths to human needs.
BIBLl0;WRT
(Abo and Ullian 1973)
Aho. A.V., and J.D. OIlman; The Theo?v ? pars;ns
Translation 111 Comni1?ng Volume li ?; Prentic?
Nail. Inc.. Englewood Cliffs. N.J.
(Alexander 19673
Alesander. C.; Notes ill rhe Synthesis ? ?; Harvard
University Press. Cambridge. Massachusetts.
(Andler 1979]
Andler. 5.; 5Predicate Path Expressions5. CoefRecord ?
liii Sisth Annual Svmnosium on Princioles ? Proea?'ne
Laneuaees (January 1979) pp. 226-236.
(Asbcroft and Wadge 1975)
Ashcroft. E.A. end W.W. Wadge; Demy?tifvin Proeram Provine.
An mL?np? ? i?i&ifl; Research Beport CS-7?-02.
Department of Computer Science. University of Waterloo.
Waterloo Canada (June 1975).
(Baker 1972a]
Baker. F.T.; 5Chief Prograrmer Team Management of Production
Prograsming5; ]1lM Svsrems Journal 11.1 (1972) pp.56-73.
(Baker l972b)
Baker. F.T.; 5System Quality through Structured Programming5;
Proceedines ? Joint Comnurer Confe?ence AFIPS, Volume
Al. Part I (1972) pp.339-343.
(Balter et.al. 1974)
Balzer. R., N. Greenfeld. M. Kay. W. Mann. W. Ry?er. D.
Wilczynski. and A. Zobrist; 5Domain-Independent Automatic
Programming5; P?oceedines ? TFlP Coneress 14 North-Nolland
Publishing Company. Amsterdam. The Netherlands.
(Balter et.al. 1976]
Balzer. R.. N. Goldman. and D. Wile; 5On the Tranaformational
Implementation Approach to Progra?ing5; Proceedipes ? the
Second International Conference 2n Softwa?e Fnerlue IfEE
Computer Society (October 1976).
(Barnard 1977]
Barnatd. 0.; An Annotar?d Biblioers?hv on Comnuter Prn?esm
iR&2?''?; Tecinical Report CSRC-oO. Univer?ity of Toronto.
Tnrunto, Canada (May 1977).
-200-
(Bbandsrkar and Juliussen 1978)
Ihandarkar D.P.. and j?g Juliussen; ?Semiconductor
Tecbnology: Trends and Implications"; ?? A?iLLLiii?
??, SlCARCR 7.1 (August 1978) pp.4-14.
(Bledsoe and 8ruell 1976)
Eledsoe, W.W.. and P. ?ruell; "A Nan-Machine Theorem Proving
System"; Artificial Intellieence 5.1 (Spring 1974) pp.51--H72.
(lobs and Ja?opini 1966)
Bohm. C.. and G. Jacopini; "Flow Diagrams. Turing Machines,
and Languages with Only Two Formation RuleaW; Com'munications
the AtM 9,5 (Nay 1966) pp.366-371.
(3urstall and Darlington 1975)
Rurstall, R.N.. and J. Darlington; "Some Transformations for
Developing Recursive ProgramsW; Proccedines ? International
Cc?'erence on Reliable Software, SICPl?N Notices 10.6 (June
1975) pp.465-472.
(Cartwrigbt 1976)
Cartwrigbt. R.; 5User-Defined Data Types as an Aid to
Verifying LISP Programs"; Proceedin?s ? the Third
International Coilpaulum i2? Auromata. Lan?ua?es. and
Pro?ra?,n?, Edinburgh Press, Edinburgh. Scotland.
(Cban 1978)
Chan, T.; ? Al.orirhm for Checkins PiJCv Arithneric
In?erence,; Technical Report 77-326. Department of Computer
Science. Cornell University. Ithaca. New York (1978).
(Clarke 19791
Clarke. E.N. Jr.; `Programming Language Constructs for which
it is Impossible to Obtain Good Noace Aaioa Systems"; Journal
aiM 26,1 (January 1979) pp. 129-147.
(Clint and Noare 19?2)
Clint. N., and C.A.R. Hoare; 5Program Proving: Jumps and
Functions'; Acra Informatica 1 (1972) pp.214-224.
(Clint 1973)
Clint. N.; `Program Proving: Coroutinee'; Acta Infora,atica 2
(1973) pp.50-63.
(Constable 1971)
Constable. R.L.; `Constructive Nathenatics and Automatic
Progra? Writers"; Proccedines ? Conaresa 21. North-
Rolland Publishing Company. Amsterdam, The Netherlands.
-202
(Constable 1978]
Constable R.L.; L!1 Proof ??????; informal document.
Departnent of Computer Science. Cornell University. Ithaca.
New York.
(Constable 19793
Constable. R.L.; personal communication.
(Constable and Johnson 19793
Constable. R.L.. and 5. Johnson; 5A PLICY Precis5; Confe-ence
3ihc Sixth &? Svssnosium ? Priacioles ? Proeramming
Ianeua?es (Jarnary 1979) pp.7-20.
(Constable and O5Donnell 1978]
Conetable R.L.. and M.J. O5Donnell; ? Proeranmo. lose;
Winthrop Publishers. Inc.. Cambridge. Massachusetts.
(Conway and Cries 1979]
Conway. 8. and D. Cries; ? Introduction ? Proeranmine;
Second ltdition Winthrop Publishers5 Inc.5 Cambridge.
Massachusetts.
(Cook 19753
Cook. S.A.; A,iomati and Interoretive 2Anl&1C]il]tl for An A1&21
Fratment; Technical Report s;D9. Department of Computer
Science. University of Toronto. Toronto. Canada.
(Demers and Donahue 1979]
Demers A.. and J. Donahue; ilenort ? the Proera=ing Lao?ua?e
?-?11; Technical Report TR79-37l. Department of Computer
Science. Coroell University. Ithaca Me? York (Narch 1979).
(Deutach 1973]
Deutach L.P.; 7tl ? Ver?f.er; Ph.D. Thesis5
Department of Computer Science University of California5
Berkeley. California.
(Dijkstra 1968a]
Dijkatra. E.W.; 5GOTO Statement Considered Harmful5;
Communications ? ACM 11.3 (March 1968) pp.147-148.
(Dijkstra 1968b]
Diikstra E W "A Constructive Approach to the Probless of
Program Correetness"; All 8.3. pp.174-186.
(Dijkstra 1975a]
Dijkstra E.W.; 5Guarded Commands. Nondeterminacy. and a
Calculus for the Derivation of Programs"; Proceedines ? the
International Conference 2LL ?eliahla Software SICP1? Notices
10.6 (June 1975) pp.2.1-2.13.
-203
(Dijkstra 1975b)
Dijkstra. K.W.; "Correctness Concerns snd Among Other Things.
?by they are Resented"; Proceedines ? Tnrernsrlnnal
Conference on ReI?able Sofrware SlCPLAN Notices 10.6 (June
1975) pp.546-SlO.
tDijkstra 1976)
Dijkstra, g.W. ? Disciolne ? Proera?ina; Prentice-Nall.
Inc.. Englewood Cliffs. N.J.
(Dneasett 1977]
Dummect. N.; Eleatents ? Intnition'sm; Clarendon Press. Oxford
University. OjLford. England.
(Earley 1973]
Earley. J.; 5Relatinnal Level Data Structures for Prograssing
Lar?goages5; ? Info?matica 2 (1973) pp.293-3O9.
(Esrley l974a]
Earley. J.; "High Level Operations in Automatic Programming";
Proceedin?s ? )1ti1iil ?ApO11? )itAX liii ]ii]oil( Lan?ua?es
SIGP1?N Notices 9.4 (April 1974) pp.34-42.
(Earley 1974b]
Earley. J.; Nieb tevel Iterators AAA A 1ffi)1lA for
Auto?ticatlv Desienine Data Structure Reoresenratlons; Nemo
No. lRL-M425. Electronics Research Laboratory. University of
California. Berkeley. California (February 1974).
(Elspas et.al. 1972]
Elapas. B. R.N. Levitt. R.J. Waldinger. and A. Wakaman; "An
Assesmeet of Techniques for Proving Program Correctness5;
4.2 (June 1972) pp.97-l47.
(glapas 1974)
Elspss. 8.; The Semiautomatic Generation 2 Induct?ve
Ataertions jilt Provine Proeram Correctness; Stanford Research
Institute Project 2686. Stanford. California (July 1974).
(Floyd 1967]
Floyd. R.W.; 5Assigning Meaning to Programs5; Proceedines ? A
Sv=?osiun in Aunlied Mathematics. American Mathematical
Society. pp.19-32.
(Floyd 1971]
Floyd. R.W.; "Toward Interactive Design of Correct Programs5;
2 IPIP Coneress ii. North-Holland Publishing
Company. Amsterdam. The Netherlands.
.:oA-
(Gerbart 1973a)
Gerhart. S.L.; "Correctness Preserving Program
Traneformationset ContRecord 2L the Second ArM
Synnosium ??fl Prjnc;nles ? Proeraseans t?nsuaaes (January
1975) pp.54-66.
(Gerbart l975b]
Gerhart. S.L.; "Knowledge about Progrsas: A Model and a Case
Study"; Proceedines ? ?nternatona1 Conference 111 Reliable
??? SlCPlAN Notices 10.6 (June 1975) pp.88-93.
(German and We?breit 1975]
C?ncdn. S.M.. and 8. Wegbreit; `A Synthesizer of lnd.ctive
Assertions"; IFFE Tra5 2fl Software En?ineerine 5K-I .1
(March 1975) pp.&8-75.
(Good 1970]
Cood. D.I.; Jo? ? Man-Machine System ?: Provina Pro?ram
ior?; ih.D. Thrais. Departwent of Co?puter Science.
University of Wisconsin, Madison. Wiaconain.
(Good et.al. 1975]
Good, 0.1.. R.L. london. and W.W. Bledsoe; 5An Interactive
Progran Verification System"; Proceedines it International
Conference it; Reliable Software, SIGPLAN Notices 10.6 (June
1975) pp.?82-492.
(Gordon et.al. 1977a]
Cordon. M., R. Milner. L. Norris. N. Newey. snd C. Uadawortb;
A Metalaneusee li Interactive Proof in 1&?; Internal Report
CSg-l6-77. University of Edinburgh. Edinburgh. Scotland
(Septeeher 1977)
(Gordon et.al. 1977b]
Gordon. N.. R. Milner. and G. Wadswortb; ??inb'.reb 1u;
Internal Report CSR-ll-77 (Parts I and 2). University of
Edinburgh. Edinburgh. Scotland (September 1977).
(Gorelici 1973]
Gorelick. G.A.; A Conolere Asionatir System jli Provin?
?Q? about Recuraive 1114 ?on-l1ecuraive Proaracs:
Technical Report #75. Department of Conputer Science.
Univer?ity of Toronto. Toronto. Canada (January 1975).
(Green 1976]
Gr?en, C.; "The Design of the PSI Progran 5ynt1?csis Systen';
Proceedinas i( Second International 1iit;?? it; ?i1JtiJGi
lIfE Coeputer Society (October 1976) pp.4-18.
(Creenspan an? lorning 1977]
C??enspan. 5.. and J.J. Norning; ???roju?in? hetiwfl? ?
liklin?1y f?r i? ?Qt?bt (jiO?* ZJ; Technical
Report CING-RI, University of To??nt?, Tcronto, Canada (Nay
1977).
(Cries 1976]
Cries. D.; "An Illustration of Current Ideas on the Derivation
of Correctness Proofs and Correct Programae; iLU Transactions
Ill Software ?n2ineerins SE-2,4 (December 1976) pp.238-243.
(?on Hefle and Luckham 1975]
von Renke, F.W.. and D.C. Luckbam; "A Methodology for
Verifying Programs"'. Proceed,n;s ? International Conference
i;;i Reliable Software, SICPLAN Notices 10,6 (June 1975)
pp.156-163.
(Hoare 1969]
Noare, C.A.R.; "An Axiomatic Baais for Computer Programming";
Co=unications ? the ArM 12.10 (October 1969) pp.576-580.
(Roare 1972a]
Boare, C.A.R.; "A Note on the FOR Statement"; lii 12 (1972)
pp.334-341.
(Hoare l972b]
Noare, C.A.R.; "Proof of Correctnesa of Data Representationa";
ALIB Informatica I (1972) pp.271--H281.
(Hoare 1973]
Hoare, C.A.R.; "Hints on Pcograi?ing Language Design"; Invited
address at the first SICACT/SICPIAN Sy???4,ln ?; Pr?ncinlea ?
Pro?ra=ini Lan?ua?es (October 1973). Al?o Technical Report
STAN-CS-73-403, Computer Science Departuent, Stanford
Cuiveraity, Stanford, California.
(Roars 1975]
Noare, C.A.p.; "Recursive Data Structures'; International
Jn?rna1 li Connuter and Svatem Sciences 4.2. pp.105-132.
(Hoare and ?irth 1973]
Noare, C.A.R., and N. Wirth; "An Axiomatic Definition of the
Prograrcing Language lASCAL"; ALLa Inforniatica 2 (1973)
pp.335-355,
(Igarasbi et.al. 1973]
Igarashi, 5.. R.L. k?ndon, and D.C. Luckham; Automatic Pro?raa
Verif?catin? li A Io2ical Basis and its Imnienienration;
Artificial Intelligence Laboratory Memo AIN-200. Stanford
University, Stanford, California (May 1973).
-206-
(Katz and Manna 1976]
Katz, 5., and ?. Manna; 5Logical Analysis of Programs';
?Q?UiLL?1L1otti A ?h? ACM 19.4 (April 1976) pp.188-206.
(Kay and Goldberg 1977]
Kay. A., end A. Goldberg; 5Personal Dynamic Media'; TFKK
Comouter Ma?azjne 10,3 (March 1977) pp.31-41.
(Kleens 1932]
Kleene, S.C.; Introduction ? Netamathematics; Van Nostrand
Publishing Company, Princeton, N.J.
(King 1969]
King. J.C.; A ?cL? Vg;iLgct; Ph.D. Thesis, Department of
Computer Science, Carnegie-Mellon University. Pittsburgh5
Penneylvania,
(King 1976]
King. J.C.; 5On Generating Verification Conditions for
Correctness Proofs5; IQ?rarnmierenracheo. edited by H.J,
Srhneider and M. Nag1, Informarik?Fachbericbre. Springe?
Verlag. Nerlin (1976).
(Liakow 1972]
Liekov, E.H.; 5A Dcsign Nethodology for Reliable Software
5yetons5; ????? A ?i Joint Co?nute Confere?ce.
AFIPS, Volume 41, Pert 1 (1972) pp.191-199.
(Liskov et.al. 1977]
Liekov, B.N., A. Snyder, R. Atkinson, and C. Schaffert;
5Abstraction ?!ccbanisns in CLU5; 1tti? A ? Aii1
iitiulitlic? ? Lanroaze D? jli Keliable ?LL1s?. 5'GPLAM
Notices 12.3 (Narch 1977) pp.166-178.
(London 1972]
London, lt.L.; 5The Current State of Proving Programs Correct';
Proccedin?s Q A(1l Aicl1lLi Conference liii. pp.39-46.
(London 1973]
London, R.L.; 5A View of Program Verification'; Proceedines ?
International Confeccnce on ?eliab1e Software SlGPLAM Noticca
10,6 (June 1973) pp.334-343.
(Long 1977]
Long. W.J.; A Proera ](1i1tzili; Ph.D. Thesis, Laboratory for
Computer Science, MIT5 Cambridge, Naaaachuaetta (November
1977).
-207-
(Nanna and Waldinaer 1977)
Nanna, Z.. and R. Waldingert 5The Automatic Synthesis of
Recursive Progran?s"1 Procecd,o+n?s li ?hc S'm?nosi, on
Artificial Intellja,nce and P?o?ramm?ne Yaneusees, SIGPLAN
Notices 12.8 (August 3977) pp.29-36.
(Nanna and Waldinger 1978)
Nanna, Z.. and R, Waldinger; "The Synthesis of Structure
Changing Prograns"; I??Jt? ? Third International
Conference on Software Ee?jne,rine, lEhE Computer Society (Nay
1978) pp.175-187.
(Nilla 1971)
Nilis. It.; 5Top Down Prograaaing in Large Systems5; in Rustin
(ed.) Dehueejne Th???i?i i? ?aree ???, Prentice- Itall,
Inc,, Englewond Cliffa. N.J.
(Nills 1975]
NilIs. It,; "Ilow to Write Correct Pro?r a and hoow It";
froceedines ? ILt?et?Ii.otici C?????? ?n Reliable ]igf???,
SICILAN Notices 10.6 (June 1975) pp,363?37O.
(Nilner 1977]
Nilner, R.; ? Theoev ? Tvpe ?1?mw1?]ctt ?
Report CSR-9-77, Departeent of Cuaputer Science. University of
Edinburgh, Fdinburgh, Scotland.
(Noriconi 1977]
Muricuni, M.S.; A Svstem ]uj Desienine and
Verifrvin? Pro?rams; Ph.D. Thesis, Departuent of Computer
Science, University of Texas, Austin, Texas CDecember 1977).
(Naur 1966]
Naur, P,; 5Proof of Programs by Cenecal Snapshots"; MI 6,4.
fItelson 1974]
Nelson, T, , ? ?Ile?; Itugo's Book Service. Box 2622,
Chicago, Illinois.
(Owicki 1975)
Owicki, 5,; Axineatic Proof Techniques for Pa,?llel liQwM;
Ph,D. Thesis, Department of Coaputer Science, Cornell
L?iveraity, Ithaca, New York (July 1973).
(Cwicki and Cries 1973]
Owirki, 5,, and D. Cries; "An Axiornatic Proof Technique for
Parallel Programs"; Act, Informatica 6 (1976) pp,319-340,
-208-
(Pratt 19773
Pratt, V.fl.: "The Coinpetence/Perfor?nce Dichotosy in
ProRra-ning"; ConfRecord 2L the ?n?.rth ArM Sv=nnaius on
Principles i;( Protra?.ne taneugees (January 1977) pp.194-200.
(Prawitt 1965]
Prawitz, 0.; Natural fleduction; Almquist and Wiksell,
Storkbnla, Sweden.
(Randall and Naur 1968]
Randoll, B. and P. Naur (eds.); Confe'ence An ?oftw??e
?1iie?)rtit; Scientific Affairs Division. NATO. Eruasels
8el?uie,
(Rich and Shrobe 1978]
Rich, C.. and N.8. Shrohe; "Initial Report on a LISP
Prograu?mer's Apprentice"; IFFF ??1ii;ii An Software
ne SE-4.6 (Nover?er 1978) pp.4?5-466
(Schwartz 1975]
Schwartz, J.T.; ? Proe?airnnine, An ??li? Renort An
Proiect; Second Edition. Coaputer Science Deparccent, Courant
inatitute of Mathetnatical Sciences, New York University. New
York. New York.
(Schwart? 1977]
Schwartz, J.T.; "On Correct ProRraa Technology5; Correct
2co?? ?c1a?? L E?tenaihiljtv i( muilitit. Computer
Scicoce Department Rtport #12, Courant Iostit?t, of
Mathematical Sciences. New York University, New York, ?ev York
(September 1977) pp.1-119.
[Shaw et.sl. 1976]
Shaw, M,, W.A. Wulf, and R.L. London; "AESThACTICN and
VERIFICATION in ALPNARO: Designing and Specifying Iteration
and Cenerators5; Proceedines w( An ,d1i1 Con?erence An `?ngu?ee
flesien ? ???? Software, S1GFLAN Notices 12.3 (March
1977) pp.153-165.
(Siewiorek et. al. 1978]
Siewiorek. D.P.. 0.8 Thomas, and D.L. Scharfetter; 5The Use
of lii Modulca in Computer Structures: Trend, and
Limitation,"; lEER Comourer Marazine 11.7 (July 1978)
pp.16-25.
(Standish et.aI. 1976]
Standish. T., D. Narriman, 0. Rihler, and J. Neighbors; The
Irvine 7r??? 1???n??? Catalorue; Departme0t of
Information and Cooputer Science, University of California,
Irvine, California (January 1976).
-209-
Essabo 1969]
Stabo. M.?.; The ???1b??? ?a? of ?eclrr? Centzen; North-
Holland Publishing Company Ai?gtecdam The Netherlands.
(Waldinger and Levitt 1974)
aldicger. R.J.. and X.N. Levitt; 5N?asoning About Progransa';
??tit? Record pi ACN ??? pI Princj?lea pi
Laneuqees (October 1973) pp.169-182.
Eweebreit 1976]
Wegbreit. B.; `Goal Directed Program Transformation1;
Conference Record pi the Third AC? Svmnosium pI Princinles ?
Pro?ra?ina Laneuanea (January 1976) pp.153-170.
(Wirtb 1971)
Wirtb, N.; `Program Development by Stepwise Refinement';
Co=?unications pi ]]it ACN 14.4 (April 1911) pp.22l-227.
(Wirth 1973]
Wirtb. N.; Svatenatic ??? A;l Introduction; Prentice-
Hall Inc., Englevood Cliffs. N.J.
(wirtb 1974]
Wirtb N.; `On the Design of Programming Languages';
Proceedines pi I?IP fo? ?, North-Holland Publishing
Company. Amsterdam. The Netherlands.
Ewnlf 1978]
Wulf. W.A. (ad.); ? Info?pl ?? pi AIPNAs0; Technical
Report CS-78-105. Department of Computer Science. Carnegie-
Ilellon University. Pittsburgh. Pennsylvania.
COLLECTED CONCEFTS, DE?tNlTlONS, AND SYNTAX
As an aid to the reader. I have collected below most of the words
and phrases whose meanings are defined in this thesis. The terms.
listed alphabetically. are briefly explained, with section and page
numbers refering to more detailed definitions in the body of the thesis.
The syntactic constructs of the specification langusge are included in
this list.
s.e., see automatically evalustahle.
analysis rule. a refinement rule whose aubgoals are derived from the
hypotheses [2.4(39)).
augmented environment. the environment of an abstraction body. It is
derived from the parameter list (3.8(101)).
automatically evaluatable, a syntactic construct is automatically
evsluatahle iff it contains no occurrence of the generator
Wtypes [3.2(61)].
constructive interpretation, a semantics for boolean formulas in which
proofs must supply more informsstion than the formula's
(classical) truth [2.4(42,44)).
deep constructive meaning. true of a formula iff it carries more
information than its (classical) truth, i.e.. iff its
justification is not NlL() (3.4(67)),
-210-
-211-
definition. a named. psrsmeteri?ed ob?ect vhose invocation yields a
value (3.8(9?)).
V (del), a msp from (extended) iterators to boolean expressions
cbaracterizing them (3.2(?9))
environment. a list of the nanes accessible to a proposition along vith
their types (3.4(66). 3.8(100). 2.3(38)).
expression. a value yielding conatruct of statically determined. fixed
type (3.1(49). 3.8(9?)].
int-exp			decimal nu?ber			variable name
I definition t?ference I int-exp t int-exp
I int-exp + int-exp I int-exp - int-exp
I - int-exp I # set-exp
set-Cxp + ?li1tit(type)			I ( generator )
variable name			I definition reference
I set-exp A set-sip I set-exp ? set-exp
I set-Cip - set-exp
bool-exp + true			I false
I variable name I definition reference
I int-exp-list relation int-exp-list
relation int-exp-list where relationo+(=.?.<.?.>.?)
I set-exp-list relation set-exp-iist
relation set-exp-list where relationo+(a.?.?.c)
I exp a set-exp I exp ,i set-exp
I ?, bool-exp
I bool-exp A bool-exp I bool-exp v bool-exp
I bool-exp ? hool-exp I bool-exp = bool-exp
I (3 iterx)hool?expx I ( V iterx)bool?expx
--H212--H
extended justification. a justification that provides sore information
than called for by the justified formula. In particular.
boolean variables occurring in the formula have non-trivial
justifications (4.2(140)3.
axtraction. the 5compiling5 process that produces executable code fros
constructive proofs (2.2(28). 2.4(41)3. For FILL. X is an
extractor function that maps proofs to justification
trenstormers expressed in L-code (4.2-4.6).
free name independence. the property that juatific?tions for a fo?ula
do not depend on the free names of the formula (?ecauae
justifications are pure values) (4.2(139)].
generator. a construct that yields a collection of values (2.3(34).
3.2(55)).
gen type I exp I exp ? exp
I a exp c exp I  exp
I iterx I gen1 for iterX I gem gem
iterstor. a construct that yields both a tuple of names (to be used over
a contextually determined scope) and a collection of tuples of
values for the names (to be used in a conteatuslly determined
way). An iterator. iter? yields the names listed in x
(2.3(35). 3.2(55)).
iter1			x : gem I iter1 IL			I iter1 for ?????
I . iterZ where x is y concatenated with
t			-213-
I a sap from a.e. boolean expressions to justifications for them
(6.2(141). 4.6(170)].
JUST, the data type representing juatiticatiuns during execution of
extracted code. (4.2(135)].
justification. an object carrying the cnnstruct?va meaning of a formula.
Conatructive proofs accept justifications for hypotheses and
yield justifications to certify their conclusion (2.4(46).
3.6(66). 4.1. 4.2].
justification transformer. usually a procedure (extracted from a proof)
that maps justifications of hypotheses into a justification for
a conclusion. In general. a map from justifications to
justifications (2.4(46). 3.4(66). 4.2].
L. the conventional programming language used for describing extracted
code (4.2(131)).
legal type. a type name which is well-defined in a given environnent
(all its type paraneter?, i.e.. var ty?ee. occur in the
environment) (3.8(101). 3.9(114)).
l?asa, a named. parameterized proposition and its proof (3.8(108)].
parameter matching. the process by which actual parameters of an
invocation are shown type compatible with formal parameters of a
definition or lemma. The process yields a substitution of types
for type names that unifies the parameter types (3.8(102).
3.9(124)).
-			4
-214-
polymorphic abatraction. a definition or lemma that can accept
paremetera of different types at different invocations
(3.8(99)).
proof. a complete argument demonatrating the constructive truth of a
proposition (2.2(25)). A well-formed refinement using the rules
of PR1? (2.2(28)].
proposition. a atatement to be proved. either purely logical or a
tranaition apecification (2.2(25). 2.3(37). 3.4(65)).
refinement rule. a rule by which a goal propoaition may be broken down
into simpler aubgoala. Solutiona to the aubgoala may be
combined to yield a anlution to the goal (2.2(24)). The Index
of Refinement Rulee providea page referencea for each rule.
state. a map from variable namea to vsluea. At any given time. it
completely deacribea the entire computation (2.3(32)).
static analysia. an examination of a propoaition to detennine its veil--H
formedacee. derive type information. etc. 3.9).
aubatitution. a ayntactic replacement. A???e is the formula A with all
free occurrencex of a rhanged to a. No capture may result from
a aubatitution (3(49)].
ayntheaia rule. a refinement rule whose aubgoals are derived from the
conclusion (2.4(39)).
transition apecification. a characterization of the state changing
properties of a program aegment (2.3(32.36). 3.3(63)).
trans--Hspec var-list anv iterX
varlist anv gem-list
varlist * nv Refl?li5tx for iter'
type. a group of values subject to a particular set of operators
(3.1(49). 3.8(100)).
type			k221			element-type
element-type ? jill' I set ( element-type ) I ?var
V a map from a.e. expressions to tbeir equivalent L-expressions
[4.2(141). 4.6(170)).
well-formed. a property of propoaitions and their components; true iff
all operators have corr?ctly typed arguments. only names in the
environment are referenced, etc. Well-fornedne.s is determined
by static analysis [3?9].
INDEX OF WINillltNT RULES
Each refinement rule of PRL ii listed below with the psge numbers
of its definition in chapter 3 and its extraction clause in chapter 4.
The rules are ordered alphabetically by the English spellings of their
names.
all analysis
all synthesis
end analysis
and synthesis
arith
assumption
choice
conposition
consequence
definition
definition evaluation
definition uniqueness
difference definition
elenunt of definition
equal d?finition
equivaltuce analysis
equival			synthesis
xclnd?! ejddle
exists analysis
an			88
v			a			73
v			74
A a			70
A a			70
arith			81
assumption			76
choice			88
composition			91
consequence			77
definition			103
definition evaluation			104
definition uniqueness			105
- def			85
a def			83
def			85
a			72
cs a			73
excluded middle			76
3 a			74
-216-
162
149
150
145
145
159
144
163
166
152
171
172
174
161
160
161
148
149
144
151
217
cijats synthesis			9 5
false definition			false def
greater than or			? def
equal definition
isplication analysis			--H a
laplication synthesis			5
intersection definition			def
iteration			iteration
leuma			lerna
less than or			? def
equal definition
not analysis			? a
not eleuent of definition			1' def
not equal definition			? def
not synthesis			? a
null			rull
or analysis			V a
or synthesis			V 5
reflexivity			reflexivity
sirplification			sirplification
size definition			? def
specialization			specialization
subset definition			c def
subset or equal definition			 def
subatitution			substitution
syT-etry			synnetry
transitivity			transitivity
75			151
76			144
82			159
71			147
71			147
85			161
94			168
108			176
82			159
72			148
85			161
76			161
72			148
8d			163
71			146
71			146
79			133
89			164
85			161
77			152
85			161
85			161
79			155
79			153
79			154
-2? 8
t?ichotoay
Lrue def
def
trichotomy
true definition
union definition
82			159
76			143
85			161
90			165