A Theory and Practice of Program Development

by Derek J. Andrews

Overview

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.

Product Details

ISBN-13:	9783540761624
Publisher:	Springer London
Publication date:	08/08/1997
Series:	Formal Approaches to Computing and Information Technology (FACIT)
Edition description:	1st Edition.
Pages:	405
Product dimensions:	6.10(w) x 9.25(h) x 0.04(d)

Table of Contents

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.