## Specification and Transformation of Programs: A Formal Approach to Software Development"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. |

### What people are saying - Write a review

User Review - Flag as inappropriate

waste waste

### Contents

1 Introduction | 1 |

12 The Problematics of Software Development | 4 |

13 Formal Specification and Program Transformation | 6 |

14 Our Particular View of Transformational Programming | 11 |

15 Relation to Other Approaches to Programming Methodology | 12 |

16 An Introductory Example | 15 |

2 Requirements Engineering | 19 |

211 Basic Notions | 20 |

551 Sorting | 240 |

552 Recognition of ContextFree Grammars | 241 |

553 Coding Problem | 247 |

554 Cycles in a Graph | 249 |

555 Hammings Problem | 251 |

556 Unification of Terms | 252 |

557 The Pack Problem | 256 |

56 Exercises | 259 |

212 Essential Criteria for Good Requirements Definitions | 23 |

213 The Particular Role of Formality | 25 |

22 Some Formalisms Used in Requirements Engineering | 27 |

222 Flowcharts | 28 |

223 Decision Tables | 29 |

224 Formal Languages and Grammars | 30 |

225 Finite State Mechanisms | 31 |

226 Petri Nets | 32 |

227 SASADT | 34 |

228 PSLPSA | 37 |

229 RSLREVS | 40 |

2210 EPOS | 44 |

2211 Gist | 49 |

2212 Summary | 52 |

3 Formal Problem Specification | 56 |

32 The Process of Formalization | 60 |

322 Problem Description | 63 |

323 Analysis of the Problem Description | 64 |

33 Definition of Object Classes and Their Basic Operations | 65 |

332 Further Examples of Basic Algebraic Types | 77 |

333 Extensions of Basic Types | 81 |

334 Formulation of Concepts as Algebraic Types | 84 |

335 Modes | 95 |

34 Additional Language Constructs for Formal Specifications | 98 |

341 Applicative Language Constructs | 100 |

342 Quantified Expressions | 107 |

343 Choice and Description | 109 |

344 Set Comprehension | 113 |

345 Computation Structures | 115 |

35 Structuring and Modularization | 117 |

36 Examples | 119 |

361 Recognizing Palindromes | 120 |

362 A Simple Number Problem | 121 |

363 A Simple Bank Account System | 122 |

364 Hammings Problem | 125 |

365 Longest Ascending Subsequence Longest Upsequence | 127 |

366 Recognition and Parsing of ContextFree Grammars | 128 |

367 Reachability and Cycles in Graphs | 129 |

368 A Coding Problem | 132 |

369 Unification of Terms | 134 |

3610 The Pack Problem | 136 |

3611 The Bounded Buffer | 138 |

3612 Paraffins | 139 |

37 Exercises | 142 |

4 Basic Transformation Techniques | 149 |

42 Notational Conventions | 154 |

422 Transformation Rules | 156 |

423 Program Developments | 158 |

43 The UnfoldFold System | 159 |

44 Further Basic Transformation Rules | 163 |

441 Axiomatic Rules of the Language Definition | 164 |

442 Rules About Predicates | 166 |

443 Basic Set Theoretic Rules | 167 |

444 Rules from Axioms of the Underlying Data Types | 168 |

45 Sample Developments with Basic Rules | 178 |

452 Palindromes | 180 |

454 Floating Point Representation of the Dual Logarithm of the Factorial | 184 |

46 Exercises | 185 |

5 From Descriptive Specifications to Operational Ones | 189 |

51 Transforming Specifications | 191 |

52 Embedding | 195 |

53 Development of Recursive Solutions from Problem Descriptions | 200 |

532 Compact Rules for Particular Specification Constructs | 211 |

533 Compact Rules for Particular Data Types | 220 |

534 Developing Partial Functions from their Domain Restriction | 225 |

54 Elimination of Descriptive Constructs in Applicative Programs | 232 |

541 Use of Sets | 233 |

542 Classical Backtracking | 236 |

543 Finite LookAhead | 237 |

55 Examples | 239 |

6 Modification of Applicative Programs3311 Types | 263 |

61 Merging of Computations | 264 |

612 Function Combination | 267 |

613 Free Merging | 273 |

62 Inverting the Flow of Computation | 275 |

63 Storing of Values Instead of Recomputation | 280 |

632 Tabulation | 282 |

64 Computation in Advance | 286 |

641 Relocation | 287 |

642 Precomputation | 288 |

643 Partial evaluation | 290 |

644 Differencing | 292 |

651 From Linear Recursion to Tail Recursion | 297 |

652 From NonLinear Recursion to Tail Recursion | 303 |

653 From Systems of Recursive Functions to Single Recursive Functions | 306 |

66 Examples | 310 |

662 The Algorithm by Cocke Kasami and Younger | 312 |

664 Hammings Problem | 319 |

67 Exercises | 322 |

7 Transformation of Procedural Programs | 326 |

711 while Loops | 328 |

712 Jumps and Labels | 332 |

713 Further Loop Constructs | 335 |

72 Simplification of Imperative Programs | 336 |

722 Elimination of Superfluous Assignments and Variables | 337 |

723 Rearrangement of Statements | 339 |

724 Procedures | 341 |

73 Examples | 343 |

731 Hammings Problem | 344 |

732 Cycles in a Graph | 345 |

74 Exercises | 347 |

8 Transformation of Data Structures | 349 |

81 Implementation of Types in Terms of Other Types | 350 |

811 Theoretical Foundations | 351 |

812 Proving the Correctness of an Algebraic Implementation | 355 |

82 Implementation of Types for Specific Environments | 359 |

822 Implementations in Terms of Modes | 361 |

823 Implementations in Terms of Pointers and Arrays | 370 |

824 Procedural Implementations | 373 |

83 Libraries of Implementations | 375 |

831 ReadyMade Implementations | 376 |

832 Complexity and Efficiency | 379 |

84 Transformation of Type Systems | 381 |

85 Joint Development | 386 |

851 Changing the Arguments of Functions | 387 |

852 Attribution | 391 |

853 Compositions | 394 |

854 Transition to Procedural Constructs for Particular Data Types | 395 |

Cycles in a Graph | 398 |

87 Exercises | 401 |

9 Complete Examples3311 Types | 404 |

91 Warshalls Algorithm | 405 |

913 Operational Improvements | 407 |

914 Transition to an Imperative Program | 408 |

92 The Majority Problem | 410 |

922 Development of an Algorithm for the Simple Problem | 411 |

923 Development of an Algorithm for the Generalized Problem | 414 |

93 Fast Pattern Matching According to Boyer and Moore | 417 |

931 Formal Specification | 418 |

933 Deriving an Operational Version of 8 | 423 |

934 Final Version of the Function occurs | 425 |

935 Remarks on Further Development | 426 |

94 A Text Editor | 427 |

941 Formal Specification | 429 |

942 Transformational Development | 445 |

943 Concluding Remarks | 454 |

References | 456 |

475 | |

### Other editions - View all

### Common terms and phrases

abstract algebraic types algorithm amount(firstt applicability conditions arbitrary arguments assertion axioms based on BOOL basic Bauer binary tree bintree buffer cleartext clist command constructs data structures data types defined definedness definition denotes derive directed graphs dummy elem element elsf embedding emptyq endoftype example expression false finite folding formal specification funct funct h function function composition further given graph G hib(a imperative program implementation input instantiation introduced isdef(b language lob(a mmap mode mset natmap natsequ natural numbers node nodemap nodesequ nodeset object kinds Obviously oldbal operations particular Petri net pqueue predicate preds(x priority queues properties requirements engineering respective Sect semantic sequ sequence simplification sort step strategy string subst Syntactic constraints tail recursion technique termstring transformation rules transformational programming transition true h tuple type scheme unfold unfold/fold universal quantification variant yields