-Ecclesiastes 12:12 Programs are invariably subjected to many rorms or
transrormation. After an initial version of a program has been designed
and developed, it undergoes debugging and certification. In addition,
most long-lived pro- grams have a liCe-cycle that includes modifications
to meet amended specifications and extensions for expanded capabilities.
Such evolution- ary aspects of programming are the topic of this
monograph. We present rormal methods for manipulating programs and
illustrate their applica- tion with numerous examples. Such methods
could be incorporated in semi-automated programming environments, where
they would serve to ease the burden on the programmer. We begin by
describing a method whereby a given program that achieves one goal can
be modified to achieve a different goal or a pro- gram that computes
wrong results can be debugged to achieve the 2 Preface intended results.
The abstraction of a set of cognate programs to obtain a program schema,
and the instantiation of abstract schemata to solve concrete problems,
are approached from the same perspective. In addition, we describe
synthesis rules for generating code from specifications and annotation
rules for making assertions about code. The synthesis rules may be used
when a program is first being developed, or when, in the course of
modifying a program, the need arises to rewrite a program segment.
Annotation rules may be used for the purpose of determining what an
incorrect program really does before attempting to debug it or how a
correct program works before attempting to modify it.
