A Theory and Practice of Program Development

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.

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.3.1 Some Primitive Commands.- 2.3.2 A Basic Command.- 2.3.3 New Commands from Old — Operators.- 2.4 Non-determinism and Partial Commands.- 2.5 The Concepts of Predicate Transformers.- 2.6 Substitution.- 2.6.1 Rules for Substitution.- 2.7 The Formal Semantics of the Kernel Language.- 2.7.1 The Bounded Commands.- 2.7.2 The Unbounded Commands.- 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.3.1 Sequence.- 3.3.2 Bounded Non-deterministic Choice.- 3.3.3 Guarded Commands.- 3.3.4 Unbounded Non-deterministic Choice.- 3.3.5 Assertions.- 3.4 A Normal Form.- 3.5 Some Further Properties.- 3.5.1 Setting and Testing Variables.- 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.3.1 A Skeptical Result.- 4.3.2 A Credulous Result.- 4.4 Limits of Predicate Transformers.- 4.4.1 The Two Approaches.- 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.6.1 Weak Refinement.- 5.6.2 Partial Refinement.- 5.6.3 Full Refinement.- 5.6.4 Strong Refinement.- 5.6.5 Refinement by Simulation.- 5.7 Summary.- 6. The Basic Commands.- 6.1 The Constant Commands.- 6.2 Assertions.- 6.3 Assignment.- 6.3.1 Implementation Issues.- 6.4 Summary.- 7. Declarations and Blocks.- 7.1 The Declaration Command.- 7.2 Some Interactions Between Commands.- 7.3 The Definitional Commands.- 7.3.1 Declarations.- 7.3.2 The Let Command.- 7.3.3 The Def Command.- 7.3.4 The Def and Let Commands Compared.- 7.4 Refining Definitional Commands.- 7.5 Defining Constant Values.- 7.5.1 Refining Functions and Constants.- 7.6 Logical Constants.- 7.7 Summary.- 8. Command Sequences.- 8.1 Solve a Part and then the Whole.- 8.1.1 Choosing the First Step.- 8.1.2 Choosing the Second Step.- 8.1.3 Choosing Both Steps.- 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 Refining Specifications.- 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.8.1 Decreasing Variants.- 10.8.2 Increasing Variants.- 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.1.1 Getting Started.- 12.1.2 The Refinement Strategy Continued.- 12.1.3 The Next Step.- 12.2 Logical Constants Revisited.- 12.3 Summary.- 13. On Refinement and Loops.- 13.1 The Factorial Problem.- 13.1.1 The First Solution.- 13.1.2 A Second Solution.- 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.4.1 The First Attempt.- 16.4.2 The Other Approach.- 16.5 Summary.- 17. Data refinement.- 17.1 The Refinement Strategy.- 17.1.1 The Problem.- 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.6.1 The check Operation.- 17.6.2 Putting it all Together.- 17.6.3 Further Development.- 17.6.4 The Final 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.1.1 The Data Refinement of Declarations.- 18.1.2 Refinement and Specifications.- 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.2 Another Approach to the Refinement.- 19.3 Summary.- 20. Stacks and Queues.- 20.1 A Finite Stack.- 20.1.1 The Refinement.- 20.1.2 Reorganizing the Operations.- 20.2 A stack of Boolean Values.- 20.2.1 Some Lemmas about the Representation.- 20.2.2 The empty-stack Operation.- 20.2.3 The push Operation.- 20.2.4 The pop Operation.- 20.2.5 The read Operation.- 20.2.6 The is-empty Operation.- 20.2.7 The is-full Operation.- 20.2.8 The Code.- 20.2.9 Some Lessons.- 20.3 A Finite Queue.- 20.3.1 A Refinement of the Queue.- 20.3.2 Some Theorems.- 20.3.3 The Operations Transformed.- 20.3.4 An Extension to the System.- 20.4 An Efficient Queue.- 20.4.1 Some Properties.- 20.4.2 Lessons.- 21. Dynamic Data Structures.- 21.1 Simulating a Linked List.- 21.1.1 Some Theorems.- 21.1.2 The Operations Transformed.- 21.2 Explicit Pointers.- 21.3 The Stack Using Explicit Pointers.- 21.3.1 Standard Stack Specification to 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.