The Evolution of Programs-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. |
Contents
| 15 | |
Program Modification and Debugging | 49 |
Program Abstraction and Instantiation | 87 |
Program Synthesis and Extension | 131 |
Program Annotation and Analysis | 195 |
General Discussion | 243 |
Global Transformations | 251 |
Synthesis Rules | 267 |
Annotation Rules | 273 |
Implementation | 289 |
References | 319 |
| 353 | |
Other editions - View all
Common terms and phrases
abstraction mapping ADD1 Y1 analogy Artificial Intelligence Aſk ASSERT AND LTQ assert q assignment rule begin begin comment c/d 3 q+ candidate Chapter compute conditional statement conditional test Conf control rules correct program debugging derived DIV2 DIVIDE C D division program element example execution exit test expression FORALL function given program global invariant goal achieve gram heuristic hold IEEE Trans imply initialization input specification input variables instantiation integer square-root program invariant assert inverse loop assert loop invariant loop L5 loop-body LTQ CONTENTS A Z modification nonnegative integer oſiſ oſs oſtſ output invariants output specification output variable pos(A,b preconditions problem Proc program synthesis program transformations program variable protecting q sē c/d real-division program recursion schema relation repeat assert replaced rule assert satisfy schemata SETO Software Engineering specification assert structured programming subgoal achieve termination tion transformed program universally quantified verification condition well-founded set yields
Bibliographic information
| Title | The Evolution of Programs Volume 5 of Progress in Computer Science and Applied Logic |
| Author | DERSHOWITZ |
| Edition | illustrated |
| Publisher | Springer Science & Business Media, 2013 |
| ISBN | 1461256216, 9781461256212 |
| Length | 359 pages |
| Subjects | › › Computers / Computer Science Computers / Data Science / General Computers / General Computers / History Mathematics / Discrete Mathematics Science / History |
| Export Citation | BiBTeX EndNote RefMan |