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.

Contenu

1. Introduction.- 2. General Overview.- 2.1. Introduction.- 2.2. The Problem.- 2.3. Annotation.- 2.4. Debugging.- 2.5. Modification.- 2.6. Abstraction.- 2.7. Instantiation.- 2.8. Synthesis.- 2.9. Discussion.- 3. Program Modification and Debugging.- 3.1. Introduction.- 3.2. Overview.- 3.2.1. Basic Method: Analogy.- 3.2.2. Special Case: Debugging.- 3.2.3. Correctness Considerations.- 3.2.4. Completing an Analogy.- 3.3. Examples.- 3.3.1. Real Division.- 3.3.1.1. First Correction.- 3.3.1.2. Second Correction.- 3.3.2. Integer Division.- 3.3.2.1. Modification.- 3.3.2.2. Extension.- 3.3.3. Array Search.- 3.3.3.1. Modification.- 3.3.3.2. Transformation.- 3.4. Discussion.- 3.4.1. Pre-modification Phase.- 3.4.2. Modification Phase.- 3.4.3. Post-modification Phase.- 4. Program Abstraction and Instantiation.- 4.1. Introduction.- 4.2. Overview.- 4.2.1. Basic Method: Analogy.- 4.2.2. Correctness Considerations.- 4.2.3. Instantiation.- 4.2.4. Special Case: Program Transformations.- 4.3. Examples.- 4.3.1. Extremum.- 4.3.2. Binary Search.- 4.3.3. Associative Recursion.- 4.4. Discussion.- 5. Program Synthesis and Extension.- 5.1. Introduction.- 5.2. Overview.- 5.2.1. Strengthening.- 5.2.2. Splitting.- 5.2.2.1. Disjoint Goals.- 5.2.2.2. Protection.- 5.2.2.3. Preservation.- 5.2.3. Assignments.- 5.2.4. Conditionals.- 5.2.5. Loops.- 5.2.5.1. Forward Iterative Loops.- 5.2.5.2. Backward Iterative Loops.- 5.2.5.3. Termination.- 5.2.5.4. Recursive Loops.- 5.2.6. Extension.- 5.3. Examples.- 5.3.1. Array Minimum.- 5.3.1.1. Goal Splitting.- 5.3.1.2. Loop Formation.- 5.3.1.3. Conditional Formation.- 5.3.1.4. Extension.- 5.3.2. Integer Square-Root.- 5.3.2.1. Goal Splitting.- 5.3.2.2. Loop Formation.- 5.3.2.3. Alternatives.- 5.3.2.4. Extension.- 5.3.2.5. Binary Integer Square-Root.- 5.3.3. Associative Recursion.- 5.3.3.1. Recursive Solution.- 5.3.3.2. Iterative Solution.- 5.3.4. Partition.- 5.3.4.1. First Solution.- 5.3.4.2. Second Solution.- 5.4. Discussion.- 6. Program Annotation and Analysis.- 6.1. Introduction.- 6.2. Overview.- 6.2.1. Notation and Terminology.- 6.2.2. Assignment Rules.- 6.2.3. Control Rules.- 6.2.4. Schematic Rules.- 6.2.5. Heuristic Rules.- 6.2.6. Counters.- 6.3. Examples.- 6.3.1. Real Division.- 6.3.1.1. Assignment Rules.- 6.3.1.2. Control Rules.- 6.3.1.3. Heuristic Rules.- 6.3.1.4. Analysis.- 6.3.2. Array Minimum.- 6.3.2.1. Assignment Rules.- 6.3.2.2. Control Rules.- 6.3.2.3. Generalization Heuristic.- 6.3.2.4. Analysis.- 6.3.3. Selection Sort.- 6.3.3.1. Algorithmic Rules.- 6.3.3.2. Heuristics.- 6.3.3.3. Analysis.- 6.4. Discussion.- 7. General Discussion.- Appendix 1: Global Transformations.- Appendix 2: Program Schemata.- Appendix 3: Synthesis Rules.- Appendix 4: Annotation Rules.- 4.1. Assignment Rules.- 4.1.1. Range Rules.- 4.1.2. Set Assignment Rules.- 4.1.3. Counter Relation Rules.- 4.1.4. Basic Relation Rules.- 4.1.5. Assorted Relation Rules.- 4.2. Control Rules.- 4.2.1. Control Axioms.- 4.2.2. Assignment Control Rules.- 4.2.3. Conditional Control Rules.- 4.2.4. Loop Control Rules.- 4.2.5. Value Rules.- 4.3. Heuristic Rules.- 4.3.1. Control Heuristics.- 4.3.2. Dangerous Heuristics.- Appendix 5: Implementation.- 5.1. Introduction.- 5.2. Modification.- 5.3. Synthesis.- 5.4. Annotation.- References.- Name Index.