Cover image; Title page; Table of Contents; Copyright; ACKNOWLEDGMENTS; INTRODUCTION; I: Deductive Synthesis; Chapter 1: Introduction to Deductive Synthesis; Chapter 2: A Deductive Approach to Program Synthesis; Publisher Summary; MOTIVATION; SPECIFICATION; BASIC STRUCTURE; SPLITTING RULES; TRANSFORMATION RULES; RESOLUTION; THE RESOLUTION RULES; THE POLARITY STRATEGY; MATHEMATICAL INDUCTION AND THE FORMATION OF RECURSIVE CALLS; A COMPLETE EXAMPLE: FINDING THE QUOTIENT OF TWO INTEGERS; THE FORMATION OF AUXILIARY PROCEDURES; GENERALIZATION; COMPARISON WITH THE PURE TRANSFORMATION-RULE APPROACH

ACKNOWLEDGMENTSChapter 3: Top-Down Synthesis of Divide-and-Conquer Algorithms; ABSTRACT; 1 Introduction; 2 A Simple Example; 3 Derived Antecedents; 4 SPECIFICATIONS; 5 Design Strategies for Simple Algorithms; 6 The Form and Function of Divide-and-Conquer Algorithms; 7 Design Strategies for Divide-and-Conquer Algorithms; 8 Concluding remarks; Appendix A; ACKNOWLEDGMENT; II: Program Verification; Chapter 4: Introduction to Program Verification; Chapter 5: Mechanical proofs about computer programs; Publisher Summary; 1 INTRODUCTION; 2 A MATHEMATICAL APPROACH; 3 THE GYPSY ENVIRONMENT

4 AN EXAMPLE5 TRIAL APPLICATIONS; 6 CONCLUSION; Appendix A. Formal proof of lemma extend_separation; Appendix B. Formal proof of verification conditionseparator#3; Discussion; Chapter 6: PROOF CHECKING THE RSA PUBLIC KEY ENCRYPTION ALGORITHM; Publisher Summary; 1 Introduction; 2 A Sketch of the Theorem-Prover; 3 Correctness of CRYPT; 4 Fermat's Theorem; 5 Invertibility of CRYPT; 6 Sample Input to the Theorem-Prover; 7 Conclusion; III: Transformational Approaches; Chapter 7: Introduction to Transformational Approaches; Chapter 8: An Experimental Program Transformation and Synthesis System

ABSTRACT1 Introduction; 2 Languages and Formalism Used; 3 System Structure; 4 Synthesis; 5 Generalisation and Sub-function Synthesis; 6 Eureka Elimination; 7 Conclusion; ACKNOWLEDGMENTS; Chapter 9: Program Development as a Formal Activity; Abstract; I INTRODUCTION; II TRANSFORMATION RULES; III CORRECTNESS OF TRANSFORMATIONS; IV TRANSFORMATIONAL SEMANTICS; V THE ROLE OF ABSTRACT DATA TYPES; VI THE ROLE OF ASSERTIONS; VII AN EXTENDED EXAMPLE: THE WARSHALL ALGORITHM; VIII CONCLUDING REMARKS; ACKNOWLEDGMENT; Chapter 10: An Experiment in Knowledge-based Automatic Programming; ABSTRACT

1 Introduction2 Overview of the Knowledge Base; 3 Sample Programs; 4 A Detailed Example; 5 Implementation; 6 Discussion; 7 Approaches to Automatic Programming; 8 Assessment; ACKNOWLEDGEMENTS; Chapter 11: On the Efficient Synthesis of Efficient Programs; ABSTRACT; 1 Introduction; 2 Background; 3 A Framework for Efficient Program Synthesis; 4 An Overview of the LIBRA Implementation; 5 An Example of LIBRA in Operation; 6 Methods for Controlling Search in Program Refinement; 7 Prototypes; 8 Estimating Execution Costs; 9 Adding New Efficiency Knowledge; 10 Results; 11 Related Research