A Theory and Practice of Program Development
1st Edition
Published on 4. July 1997
Book
Paperback/Softback
XVII, 405 pages
978-3-540-76162-4 (ISBN)
Description
A Theory and Practice of Program Development
provides a comprehensive introduction to a software development method based on VDM-SL. Each development step is rigorously justified, and the strategies and transformations used are justified and explained ma thematically. The approach provides the formal semantics of a simple, but powerful, wide-spectrum programming language and gives a formal definition of both algorithmic and data refinement. Unlike other texts, it covers both the theory and practice of program development. Although based on VDM-SL, no knowledge of this language is assumed, thus making it widely accessible.
A Theory and Practice of Program Development
is intended for 3rd/4th year undergraduate and postgraduate students taking formal methods and software engineering; software developers involved in the production of provably correct computer systems and reusa ble design and the problems of reusable code.
More details
Series
Edition
1st Edition.
Language
English
Place of publication
London
United Kingdom
Publishing group
Springer Berlin
Target group
Professional and scholarly
Research
Illustrations
2 s/w Abbildungen
XVII, 405 p. 2 illus.
Dimensions
Height: 235 mm
Width: 155 mm
Thickness: 23 mm
Weight
639 gr
ISBN-13
978-3-540-76162-4 (9783540761624)
DOI
10.1007/978-1-4471-0987-7
Schweitzer Classification
Content
1. Writing Correct Programs.- 1.1 Satisfying Specifications.- 1.2 An Alternative Approach.- 1.3 Summary.- 2. A Small Programming Language.- 2.1 Satisfying Specifications.- 2.2 Specifications and Programs.- 2.3 The Semantics of Commands.- 2.4 Non-determinism and Partial Commands.- 2.5 The Concepts of Predicate Transformers.- 2.6 Substitution.- 2.7 The Formal Semantics of the Kernel Language.- 2.8 The Weakest Liberal Pre-conditions, Termination, and Relations.- 2.9 Executable Programs.- 2.10 Summary.- 3. Concepts and Properties.- 3.1 More Commands.- 3.2 The Domain of a Command.- 3.3 Some Properties of Commands.- 3.4 A Normal Form.- 3.5 Some Further Properties.- 3.6 The Primitive Commands Revisited.- 3.7 Initial Values.- 3.8 A Compiler for the Small Language.- 3.9 Summary.- 4. Building New Commands from Old.- 4.1 Defining Commands.- 4.2 An Approach to Recursion.- 4.3 Sequences of Predicates and their Limit.- 4.4 Limits of Predicate Transformers.- 4.5 Limits of Commands.- 4.6 Tidying the Loose Ends.- 4.7 Epilogue.- 5. Program Refinement.- 5.1 Stepwise Refinement.- 5.2 Replacing Specifications.- 5.3 Conventions.- 5.4 Refinement Classes.- 5.5 Alternative Views of Refinement.- 5.6 Other Refinement Relations.- 5.7 Summary.- 6. The Basic Commands.- 6.1 The Constant Commands.- 6.2 Assertions.- 6.3 Assignment.- 6.4 Summary.- 7. Declarations and Blocks.- 7.1 The Declaration Command.- 7.2 Some Interactions Between Commands.- 7.3 The Definitional Commands.- 7.4 Refining Definitional Commands.- 7.5 Defining Constant Values.- 7.6 Logical Constants.- 7.7 Summary.- 8. Command Sequences.- 8.1 Solve a Part and then the Whole.- 8.2 Summary.- 9. The Alternative Command.- 9.1 Divide and Conquer.- 9.2 The Partition.- 9.3 Reassembly.- 9.4 Alternatives - The If Command.- 9.5 RefiningSpecifications.- 9.6 Summary.- 10. The Iterative Command.- 10.1 Another Approach.- 10.2 The Generalized Loop and Refinement.- 10.3 The General Variant Theorem.- 10.4 An Application.- 10.5 Loops.- 10.6 Iteration - The Do Command.- 10.7 Practical Do Commands.- 10.8 The Refinement of Loop Bodies.- 10.9 Summary.- 11. Functions and Procedures.- 11.1 Proper Procedures and their Calls.- 11.2 Function Procedures and their Calls.- 11.3 Function Calls in Expressions.- 11.4 An Alternative Approach to Parameters and Arguments.- 11.5 Postscript.- 11.6 Summary.- 12. An Example of Refinement at Work.- 12.1 The Problem - Integer Multiplication.- 12.2 Logical Constants Revisited.- 12.3 Summary.- 13. On Refinement and Loops.- 13.1 The Factorial Problem.- 13.2 Finding Guards and Invariants.- 13.3 Identifying the Loop Type Incorrectly.- 14. Functions and Procedures in Refinement.- 14.1 Factorial.- 14.2 Multiply.- 14.3 Summary.- 15. Refinement and Performance.- 15.1 A Second Approach to Multiplication.- 15.2 Fast Division.- 15.3 Summary.- 16. Searching and Sorting.- 16.1 A Diversion - the Array Data Type.- 16.2 Linear Search.- 16.3 Binary Search.- 16.4 A Simple Sort Algorithm.- 16.5 Summary.- 17. Data refinement.- 17.1 The Refinement Strategy.- 17.2 The Refinement to Executable Code.- 17.3 The Next Step.- 17.4 The Refinement of the Operations.- 17.5 The First Refinement Step.- 17.6 The Next Refinement Step.- 17.7 A Summary of the Approach.- 17.8 Summary.- 18. A Theory of Data Refinement.- 18.1 An Approach to Data Refinement.- 18.2 Data Refinement in Practice.- 18.3 Another View of Data Refinement.- 18.4 Functional Refinement.- 18.5 An Alternative Data Refinement of Assignments.- 18.6 Summary.- 19. An Alternative Refinement of the Security System.- 19.1 A Data Refinement.- 19.2Another Approach to the Refinement.- 19.3 Summary.- 20. Stacks and Queues.- 20.1 A Finite Stack.- 20.2 A stack of Boolean Values.- 20.3 A Finite Queue.- 20.4 An Efficient Queue.- 21. Dynamic Data Structures.- 21.1 Simulating a Linked List.- 21.2 Explicit Pointers.- 21.3 The Stack Using Explicit Pointers.- 21.4 Summary.- 22. Binary Trees.- 22.1 The Specification.- 22.2 The Refinement.- 22.3 The Refinement of the in Operation.- 22.4 The Refinement of the insert Operation.- 22.5 The Refinement of the delete Operation.- 22.6 An In-order Traversal.- 22.7 Summary.- 23. Epilogue.- 23.1 An Approach to Loose Patterns and Functions.- A. Program Refinement Rules.- A.1 Replace Specification.- A.2 Assume Pre-condition in Post-condition.- A.3 Introduce Assignment.- A.4 Introduce Command-semicolon.- A.5 Introduce Semicolon-command.- A.6 Introduce Leading Assignment.- A.7 Introduce Following Assignment.- A.8 Introduce Alternatives.- A.9 Introduce Iteration.- A.10 Introduce Proper Procedure Body.- A.11 Introduce Proper Procedure Call.- A.12 Introduce Function Procedure Body.- A.13 Introduce Function Procedure Call.- A.14 Add Variable.- A.15 Realize Quantifier.- A.16 Remove Scope.- A.17 Expand Frame.- A.18 Contract Frame.- A.19 Introduce Logical Constant.- A.20 Remove Logical Constant.- A.21 Refine Block.- A.22 Introduce Skip.