Front Cover

Readings in Artificial Intelligence and Software Engineering

Copyright Page

Table of Contents

ACKNOWLEDGMENTS

INTRODUCTION

Part I: Deductive Synthesis

Chapter 1. A Deductive Approach to Program Synthesis

MOTIVATION

BASIC STRUCTURE

SPLITTING RULES

TRANSFORMATION RULES

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

REFERENCES

Chapter 2. Top-Down Synthesis of Divide-and-Conquer Algorithms

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

REFERENCES

Part II: Program Verification

Chapter 3. Mechanical proofs about computer programs

1. INTRODUCTION

2. A MATHEMATICAL APPROACH

3. THE GYPSY ENVIRONMENT

4. AN EXAMPLE

5. TRIAL APPLICATIONS

6. CONCLUSION

APPENDIX A. FORMAL PROOF OF LEMMA extend_separation

APPENDIX B. FORMAL PROOF OF VERIFICATION CONDITION

REFERENCES

Chapter 4. PROOF CHECKING THE RSA PUBLIC KEY ENCRYPTION ALGORITHM

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

References

Part Ill: Transformational Approaches

Chapter 5. An Experimental Program Transformation and Synthesis System

1. Introduction

2. Languages and Formalism Used

3. System Structure

4. Synthesis

5. Generalisation and Sub-function Synthesis

6. Eureka Elimination

7. Conclusion

ACKNOWLEDGMENTS

REFERENCES

Chapter 6. Program Development as a Formal Activity

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

REFERENCES

Chapter 7. An Experiment in Knowledge-based Automatic Programming

1. Introduction

2. Overview of the Knowledge Base

3. Sample Programs

4. A Detailed Example

5. Implementation

6. Discussion

7. Approaches to Automatic Programming

8. Assessment

ACKNOWLEDGEMENTS

REFERENCES

Chapter 8. On the Efficient Synthesis of Efficient Programs

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

12. Conclusions

ACKNOWLEDGMENT

REFERENCES

Chapter 9. Reusability Through Program Transformations

I. INTRODUCTION

II. ABSTRACT PROGRAMS

III. REFINEMENT OF ABSTRACT PROGRAMS TO CONCRETE PROGRAMS

IV. SOME EXPERIENCE WITH REUSING ABSTRACT PROGRAMS

V. THE PROGRAMMING SUPPORT ENVIRONMENT

REFERENCES

Chapter 10. Program Developments:Formal Explanations of Implementations

1. INTRODUCTION: TRANSFORMATIONAL IMPLEMENTATION

2. DEVELOPMENT LANGUAGE PROPERTIES

3. THE DEVELOPMENT LANGUAGE

4. THE DEVELOPMENT PROCESS

5. REPLAY OF DEVELOPMENTS

6. THE UNDERLYING PROGRAM MANIPULATION SYSTEM: POPART

7. STRUCTURES EXPRESSED IN THE PADDLE LANGUAGE

8. PROBLEMS AND FUTURE RESEARCH

REFERENCES

Part IV: Natural Language Specifications

Chapter 11. Automatic Programming Through Natural Language Dialogue: A Survey

Introduction

Comparison

Research issues

Acknowledgments

References and notes

Chapter 12. Protosystem I—An automatic programming system prototype

INTRODUCTION

A MODEL OF THE PROGRAM WRITING PROCESS

EFFICIENCY ENHANCEMENT IN SYSTEM DEVELOPMENT

THE DEVELOPMENT OF PROTOSYSTEM

THE PROTOSYSTEM I DATA PROCESSING SYSTEM MODEL AND THE SYSTEM SPECIFICATION LANGUAGE

THE TRANSLATOR AND THE DATA SET LANGUAGE

THE DESIGN CRITERION AND THE JOB COST ESTIMATOR

THE OPTIMIZING DESIGNER

CONCLUSION

ACKNOWLEDGMENTS

BIBLIOGRAPHY

Chapter 13. Informality in Program Specifications

I. INTRODUCTION

II. ATTRIBUTES OF SUITABLE PROCESS-ORIENTED SPECIFICATION LANGUAGES

III. WHY OPERATIONAL SPECIFICATIONS ARE HARD TO CONSTRUCT

IV. SEMANTIC CONSTRUCTS IN NATURAL LANGUAGE SPECIFICATION

V. DESIRABILITY OF INFORMALITY

VI. RESULTS

VII. DESCRIPTION OF THE PROTOTYPE SYSTEM

REFERENCES

Part V: Very High Level Languages

Chapter 14. An Automatic Technique for Selection of Data Representations in SETL Programs

1. INTRODUCTION

2. THE SETL LANGUAGE AND ITS BASING SYSTEM

3. AN AUTOMATIC DATA REPRESENTATION SELECTION ALGORITHM

4. CONCLUSION

ACKNOWLEDGMENTS

REFERENCES

Chapter 15. Automating the Selection of Implementation Structures

I. INTRODUCTION

II. FORMALISMS

III. ALTERNATIVE IMPLEMENTATION-STRUCTURE GENERATION

IV. SUMMARY AND CONCLUSIONS

APPENDIX

ACKNOWLEDGMENT

REFERENCES

Chapter 16. KNOWLEDGE-BASED PROGRAMMING SELF APPLIED

ABSTRACT

1. Introduction

2. Specification of the Rule Compiler

3. Extensions to the Rule Compiler

Acknowledgements

References

Chapter 17. IMPLEMENTING SPECIFICATION FREEDOMS

1. Introduction

2. Specification in Gist

3. Mappings

4. Concrete examples of Gist

5. Case study

6. Related work

7. Conclusions

Acknowledgment

References

Part VI: Programming by Example

Chapter 18. A Methodology for LISP Program Construction from Examples

1. Introduction

2. A Sample Synthesis

3. Synthesis Theorems

4. Variable Addition

5. Two Additional Examples

6. System Capabilities and Limitations

7. Conclusion

REFERENCES

Chapter 19. Programming by Examples

1. Introduction

2. A Computation Description Language

3. The Synthesis Algorithm

4. Concluding Remarks

Appendix I

ACKNOWLEDGMENTS

REFERENCES

Part VII: Intelligent Assistants

Chapter 20. TOWARD INTERACTIVE DESIGN OF CORRECT PROGRAMS

CONCLUSION

APPENDIX

REFERENCES

Chapter 21. A Designer/Verifier's Assistant

I. INTRODUCTION

II. BRIEF SCENARIO

III. SUGGESTING WHAT TO DO NEXT

IV. PREVIEWING THE EFFECTS OF CHANGES

V. REASONING ABOUT CHANGES

VI. CONCLUSION

APPENDIX A. RELATIONS IN A MODEL

APPENDIX B. ASAMPLE MODEL

ACKNOWLEDGMENT

REFERENCES

Chapter 22. The Programmer's Apprentice: A Session with KBEmacs

I. INTRODUCTION

II. SCENARIO

III. EVALUATION

IV. CAPABILITIES

V. IMPLEMENTATION

VI. RELATED WORK

VII. FUTURE DIRECTIONS

ACKNOWLEDGMENT

REFERENCES

Chapter 23. REPORT ON A KNOWLEDGE-BASED SOFTWARE ASSISTANT

ABSTRACT

1. EXECUTIVE SUMMARY

2. PROBLEMS AND SOLUTIONS

3. KBSA INTERNAL STRUCTURE

4. SUPPORTING TECHNOLOGY AREAS

5. ACKNOWLEDGMENTS

6. REFERENCES

Part VIII: Programming Tutors

Chapter 24. Intelligent Program Analysis

1. Introduction

2. Finding the Plan

3. Program Synthesis

4. Program Generation Models

5. Analysis Policy

6. The Analysis Process

7. Value Equivalence

8. Construct Equivalence

9. Error Analysis

10. Expression Errors

11. Conditional Clause Reversal

12. Predicate Errors

13. Loop Iteration Errors

14. The Missing EXIT Statement

15. An Example

16. Experience

17. Applications

Appendix. A Simple Programming Language Model

REFERENCES

Chapter 25. PROUST: Knowledge-Based Program Understanding

I. INTRODUCTION: MOTIVATION AND GOALS

II. THE ROLE OF PLANS IN PROGRAM UNDERSTANDING

III. ATYPICAL PROBLEM IN PROUST's DOMAIN

IV. RELATING GOALS TO CODE VIA PLANS

V. THE UNDERSTANDING PROCESS: AN EXAMPLE OF PROUST IN ACTION

VI. PERFORMANCE: PRELIMINARY RESULTS

VII. CONCLUDING REMARKS

REFERENCES

IX: Programming Knowledge

Chapter 26. On Program Synthesis Knowledge

1. Introduction

2. Overview of Programming Knowledge

3. The Divide-and-conquer or Partitioning Paradigm

4. Internal Representation of Sets

5. Singleton Split

6. Refinement Diagram for Sorting Programs

7. In-place Sorting

8. Equal-size Split

9. Conclusions

10. Appendix

REFERENCES

Chapter 27. Program Abstraction and Instantiation

1. INTRODUCTION

2. OVERVIEW

3. A DETAILED EXAMPLE

4. PROGRAM TRANSFORMATIONS

5. DISCUSSION

ACKNOWLEDGMENTS

REFERENCES

Chapter 28. A Formal Representation For PlansIn The Programmer's Apprentice

1. Introduction

2. The Plan Calculus

3. A Situational Calculus

4. Plans

5. Relations Between Plans

6. Final Remarks

References

Chapter 29. Empirical Studies of Programming Knowledge

I. INTRODUCTION: MOTIVATION AND GOALS

II. BRIEF DESCRIPTION OF BOTH EXPERIMENTAL TECHNIQUES

III. GENERATING PLAN-LIKE AND UNPLAN-LIKE PROGRAMS

IV. DETAILED DESCRIPTION OF STUDY I: FILL-IN-THE-BLANK

V. DETAILED DESCRIPTION OF STUDY II: RECALL

VI. CONCLUDING REMARKS

ACKNOWLEDGMENTS

REFERENCES

Part X: Domain Knowledge

Chapter 30. The Draco Approach to Constructing Software from Reusable Components

I. INTRODUCTION

II. THE ORGANIZATIONAL CONTEXT OF DRACO

III. WHAT COMPRISES A DOMAIN DESCRIPTION?

IV. DIFFERENCES IN DEFINITION FROM OTHER APPROACHES

V. AN EXAMPLE DOMAIN ORGANIZATION

VI. SOFTWARE COMPONENTS AND THE REFINEMENT PROCESS

VII. DOMAIN SPECIFIC SOURCE-TO-SOURCE PROGRAM TRANSFORMATIONS

VIII. WHAT CAN BE SAID ABOUT THE POWER OF THE DRACO METHOD

IX. CONCLUSIONS

APPENDIX

REFERENCES

Chapter 31. A Perspective on Automatic Programming

Abstract

The Task Domain: Quantitative Log Interpretation

The Role of Domain Knowledge

An Experimental Approach

Summary

References

Chapter 32. Knowledge Representation as the Basis for Requirements Specifications

Requirements specifications should talk about the "what"rather than the "how" of a software system; specifications dealing with the world must be more powerful and extensive than those dealing with target systems

It is necessary to combine several kinds of modeling faculties into one language; a good modeling language should allow the designer to describe discourse entities andevents in the real world

Successive RML refinements introduce and describe smaller and smaller subclasses that model more and more specialized concepts: here inheritance allows the modeler to limit specifications to how the subclass differs from the superclass at each step

Time is inextricably involved in every fact we state: RML captures therich variety of time references in everday discourse and builds complex temporal descriptions within its object-oriented framework

The chief difficulty of theinitial stages of requirements engineering is deciding what concepts and phenomena arerelevant

AI research on non-monotonic logics may provide insight on how to make final specification logically consistent

References

Part XI: Artificial Intelligence Programming

Chapter 33. POWER TOOLS FOR PROGRAMMERS

The implementation disasters of the 1960s are slowly being succeeded by the design disasters of the 1980s

Redundancy protects the design from unintentional change—but it's equally well protected against intentional change

Conventional programming technology restrains the programmer; exploratory systems amplify him

The programming languages used in exploratory systems minimize and defer constraints on the programmer

Chapter 34. Perspectives on Artificial Intelligence Programming

Programming Styles

Use of Multiple Paradigms

Programming Environments

Narrow Knowledge-Based Systems

Directions and Themes Revisited

REFERENCES AND NOTES

BIBLIOGRAPHY

INDEX