+612 9045 4394
Specification and Transformation of Programs : A Formal Approach to Software Development - Helmut A. Partsch

Specification and Transformation of Programs

A Formal Approach to Software Development

Hardcover Published: 5th July 1990
ISBN: 9783540523567
Number Of Pages: 493

Share This Book:


RRP $228.99
or 4 easy payments of $39.63 with Learn more
Ships in 7 to 10 business days

Other Available Editions (Hide)

Specification and Transformation of Programs is short for a methodology of software development where, from a formal specification of a problem, programs correctly solving that problem are constructed by stepwise application of formal, semantics-preserving transformation rules. This book is primarily intended as a general introductory textbook. It can also be seen as a comprehensive account of the transformational methodology developed within the Munich CIP project. The contents of the book reflect the essential steps in a sequential process of software development from an informally stated problem, via a formal problem specification, to a final, efficient program. Aspects considered include linguistic means for describing the various intermediate stages in the process, individual techniques for the transition between these stages, and strategies for applying these techniques. All aspects are illustrated by representative examples.

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.

ISBN: 9783540523567
ISBN-10: 3540523561
Series: Monographs in Computer Science
Audience: Professional
Format: Hardcover
Language: English
Number Of Pages: 493
Published: 5th July 1990
Country of Publication: DE
Dimensions (cm): 25.4 x 17.78  x 2.87
Weight (kg): 1.11