General Discussion
Nachum Dershowitz · Birkhäuser Boston eBooks · 1983
Programming is a complex human activity, requiring skill and expertise of its practitioners. The idea of designing an interactive programming system in which a human programmer is assisted by a semiautomatic verifier/debugger was first suggested in [Floyd71]; more recently, the need for assorted “intelligent” programming aids has been expressed in many quarters. In our view, it is important to incorporate—as an integral part of such programming environments— methods for transforming programs in ways that do not necessarily preserve their semantics, in addition to correctness-preserving transformations. Our purpose in the chapters that preceded was to contribute to that goal by describing a unified approach to formal program manipulation based upon invariant assertions. (For a survey of various logic- based approaches to the different aspects of programming, see [Manna- Waldinger78].) We believe that the kinds of evolutionary processes that we have formalized play an important role in programming.