Specification and Transformation of Programs: A Formal Approach to Software Development

Front Cover
Springer Science & Business Media, Jul 5, 1990 - Computers - 493 pages
"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
Index
475
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information