Specification and Transformation of Programs

"Specification and transformation of programs" is short for a methodology of software development where, from a formal specification of a problem to be solved, programs correctly solving that problem are constructed by stepwise application of formal, semantics-preserving transformation rules. The approach considers programming as a formal activity. Consequently, it requires some mathematical maturity and, above all, the will to try something new. A somewhat experienced programmer or a third- or fourth-year student in computer science should be able to master most of this material - at least, this is the level I have aimed at. This book is primarily intended as a general introductory textbook on transformational methodology. As with any methodology, reading and understanding is necessary but not sufficient. Therefore, most of the chapters contain a set of exercises for practising as homework. Solutions to these exercises exist and can, in principle, be obtained at nominal cost from the author upon request on appropriate letterhead. In addition, the book also can be seen as a comprehensive account of the particular transformational methodology developed within the Munich CIP project.

1. Introduction.- 1.1 Software Engineering.- 1.2 The Problematics of Software Development.- 1.3 Formal Specification and Program Transformation.- 1.4 Our Particular View of Transformational Programming.- 1.5 Relation to Other Approaches to Programming Methodology.- 1.6 An Introductory Example.- 2. Requirements Engineering.- 2.1 Introduction.- 2.1.1 Basic Notions.- 2.1.2 Essential Criteria for Good Requirements Definitions.- 2.1.3 The Particular Role of Formality.- 2.2 Some Formalisms Used in Requirements Engineering.- 2.2.1 A Common Basis for Comparison.- 2.2.2 Flowcharts.- 2.2.3 Decision Tables.- 2.2.4 Formal Languages and Grammars.- 2.2.5 Finite State Mechanisms.- 2.2.6 Petri Nets.- 2.2.7 SA/SADT.- 2.2.8 PSL/PSA.- 2.2.9 RSL/REVS.- 2.2.10 EPOS.- 2.2.11 Gist.- 2.2.12 Summary.- 3. Formal Problem Specification.- 3.1 Specification and Formal Specification.- 3.2 The Process of Formalization.- 3.2.1 Problem Identification.- 3.2.2 Problem Description.- 3.2.3 Analysis of the Problem Description.- 3.3 Definition of Object Classes and Their Basic Operations.- 3.3.1 Algebraic Types.- 3.3.2 Further Examples of Basic Algebraic Types.- 3.3.3 Extensions of Basic Types.- 3.3.4 Formulation of Concepts as Algebraic Types.- 3.3.5 Modes.- 3.4 Additional Language Constructs for Formal Specifications.- 3.4.1 Applicative Language Constructs.- 3.4.2 Quantified Expressions.- 3.4.3 Choice and Description.- 3.4.4 Set Comprehension.- 3.4.5 Computation Structures.- 3.5 Structuring and Modularization.- 3.6 Examples.- 3.6.1 Recognizing Palindromes.- 3.6.2 A Simple Number Problem.- 3.6.3 A Simple Bank Account System.- 3.6.4 Hamming’s Problem.- 3.6.5 Longest Ascending Subsequence (“Longest Upsequence”).- 3.6.6 Recognition and Parsing of Context-Free Grammars.- 3.6.7 Reachability and Cycles in Graphs.- 3.6.8 A Coding Problem.- 3.6.9 Unification of Terms.- 3.6.10 The “Pack Problem”.- 3.6.11 The Bounded Buffer.- 3.6.12 Paraffins.- 3.7 Exercises.- 4. Basic Transformation Techniques.- 4.1 Semantic Foundations.- 4.2 Notational Conventions.- 4.2.1 Program Schemes.- 4.2.2 Transformation Rules.- 4.2.3 Program Developments.- 4.3 The Unfold/Fold System.- 4.4 Further Basic Transformation Rules.- 4.4.1 Axiomatic Rules of the Language Definition.- 4.4.2 Rules About Predicates.- 4.4.3 Basic Set Theoretic Rules.- 4.4.4 Rules from the Axioms of the Underlying Data Types.- 4.4.5 Derived Basic Transformation Rules.- 4.5 Sample Developments with Basic Rules.- 4.5.1 Simple Number Problem.- 4.5.2 Palindromes.- 4.5.3 The Simple Bank Account Problem Continued.- 4.5.4 Floating Point Representation of. the Dual Logarithm of the Factorial.- 4.6 Exercises.- 5. From Descriptive Specifications to Operational Ones.- 5.1 Transforming Specifications.- 5.2 Embedding.- 5.3 Development of Recursive Solutions from Problem Descriptions.- 5.3.1 A General Strategy.- 5.3.2 Compact Rules for Particular Specification Constructs.- 5.3.3 Compact Rules for Particular Data Types.- 5.3.4 Developing Partial Functions from their Domain Restriction.- 5.4 Elimination of Descriptive Constructs in Applicative Programs.- 5.4.1 Use of Sets.- 5.4.2 Classical Backtracking.- 5.4.3 Finite Look-Ahead.- 5.5 Examples.- 5.5.1 Sorting.- 5.5.2 Recognition of Context-Free Grammars.- 5.5.3 Coding Problem.- 5.5.4 Cycles in a Graph.- 5.5.5 Hamming’s Problem.- 5.5.6 Unification of Terms.- 5.5.7 The “Pack Problem”.- 5.6 Exercises.- 6. Modification of Applicative Programs.- 6.1 Merging of Computations.- 6.1.1 Function Composition.- 6.1.2 Function Combination.- 6.1.3 “Free Merging”.- 6.2 Inverting the Flow of Computation.- 6.3 Storing of Values Instead of Recomputation.- 6.3.1 Memo-ization.- 6.3.2 Tabulation.- 6.4 Computation in Advance.- 6.4.1 Relocation.- 6.4.2 Precomputation.- 6.4.3 Partial Evaluation.- 6.4.4 Differencing.- 6.5 Simplification of Recursion.- 6.5.1 From Linear Recursion to Tail Recursion.- 6.5.2 From Non-Linear Recursion to Tail Recursion.- 6.5.3 From Systems of Recursive Functions to Single Recursive Functions.- 6.6 Examples.- 6.6.1 Bottom-up Recognition of Context-Free Grammars.- 6.6.2 The Algorithm by Cocke, Kasami and Younger.- 6.6.3 Cycles in a Graph.- 6.6.4 Hamming’s Problem.- 6.7 Exercises.- 7. Transformation of Procedural Programs.- 7.1 From Tail Recursion to Iteration.- 7.1.1 while Loops.- 7.1.2 Jumps and Labels.- 7.1.3 Further Loop Constructs.- 7.2 Simplification of Imperative Programs.- 7.2.1 Sequentialization.- 7.2.2 Elimination of Superfluous Assignments and Variables.- 7.2.3 Rearrangement of Statements.- 7.2.4 Procedures.- 7.3 Examples.- 7.3.1 Hamming’s Problem.- 7.3.2 Cycles in a Graph.- 7.4 Exercises.- 8. Transformation of Data Structures.- 8.1 Implementation of Types in Terms of Other Types.- 8.1.1 Theoretical Foundations.- 8.1.2 Proving the Correctness of an Algebraic Implementation.- 8.2 Implementations of Types for Specific Environments.- 8.2.1 Implementations by Computation Structures.- 8.2.2 Implementations in Terms of Modes.- 8.2.3 Implementations in Terms of Pointers and Arrays.- 8.2.3 Procedural Implementations.- 8.3 Libraries of Implementations.- 8.3.1 “Ready-Made” Implementations.- 8.3.2 Complexity and Efficiency.- 8.4 Transformation of Type Systems.- 8.5 Joint Development.- 8.5.1 Changing the Arguments of Functions.- 8.5.2 “Attribution”.- 8.5.3 Compositions.- 8.5.4 Transition to Procedural Constructs for Particular Data Types.- 8.6 An Example: Cycles in a Graph.- 8.7 Exercises.- 9. Complete Examples.- 9.1 Warshall’s Algorithm.- 9.1.1 Formal Problem Specification.- 9.1.2 Derivation of an Operational Specification.- 9.1.3 Operational Improvements.- 9.1.4 Transition to an Imperative Program.- 9.2 The Majority Problem.- 9.2.1 Formal Specification.- 9.2.2 Development of an Algorithm for the Simple Problem.- 9.2.3 Development of an Algorithm for the Generalized Problem.- 9.3 Fast Pattern Matching According to Boyer and Moore.- 9.3.1 Formal Specification.- 9.3.2 Development of the Function occurs.- 9.3.3 Deriving an Operational Version of ?.- 9.3.4 Final Version of the Function occurs.- 9.3.5 Remarks on Further Development.- 9.3.6 Concluding Remarks.- 9.4 A Text Editor.- 9.4.1 Formal Specification.- 9.4.2 Transformational Development.- 9.4.3 Concluding Remarks.- References.