Title	On the Refinement Calculus [electronic resource] / edited by Carroll Morgan, Trevor Vickers
Imprint	London : Springer London, 1992
Connect to	http://dx.doi.org/10.1007/978-1-4471-3273-8
Descript	XI, 159 p. online resource

On the Refinement Calculus gives one view of the development of the refinement calculus and its attempt to bring together - among other things - Z specifications and Dijkstra's programming language. It is an excellent source of reference material for all those seeking the background and mathematical underpinnings of the refinement calculus

The Specification Statement -- 1 Introduction -- 2 Specification statements -- 3 The implementation ordering -- 4 Suitability of the definitions -- 5 Using specification statements -- 6 Miracles -- 7 Guarded commands are miracles -- 8 Positive applications of miracles -- 9 Conclusion -- 10 Acknowledgements -- Specification Statements and Refinement -- 1 Introduction -- 2 The refinement theorems -- 3 The refinement calculus -- 4 An example: square root -- 5 Derivation of laws -- 6 Conclusion -- 7 Acknowledgements -- Procedures, Parameters, and Abstraction: Separate Concerns -- 1 Introduction -- 2 Procedure call -- 3 Procedural abstraction -- 4 Parameters -- 5 Conclusion -- 6 Acknowledgements -- Data Refinement by Miracles -- 1 Introduction -- 2 An abstract program -- 3 A difficult data refinement -- 4 Miraculous programs -- 5 Eliminating miracles -- 6 Conclusion -- 7 Acknowledgements -- Auxiliary Variables in Data Refinement -- 1 Introduction -- 2 The direct technique -- 3 The auxiliary variable technique -- 4 The correspondence -- 5 Conclusion -- 6 Acknowledgements -- Data Refinement of Predicate Transformers -- 1 Introduction -- 2 Predicate transformers -- 3 Algorithmic refinement of predicate transformers -- 4 Data refinement of predicate transformers -- 5 The programming language -- 6 Distribution of data refinement -- 7 Data refinement of specifications -- 8 Data refinement in practice -- 9 Conclusions -- 10 Acknowledgements -- Data Refinement by Calculation -- 1 Introduction -- 2 Refinement -- 3 Language extensions -- 4 Data refinement calculators -- 5 Example of refinement: the โ{128}{156}meanโ{128}{157} module -- 6 Specialized techniques -- 7 Conclusions -- 8 Acknowledgements -- 9 Appendix: refinement laws -- A Single Complete Rule for Data Refinement -- 1 Introduction -- 2 Data refinement -- 3 Predicate transformers -- 4 Completeness -- 5 Soundness -- 6 Partial programs -- 7 An example -- 8 Conclusion -- 9 Acknowledgements -- Types and Invariants in the Refinement Calculus -- 1 Introduction -- 2 Invariant semantics -- 3 The refinement calculus -- 4 A development method -- 5 Laws for local invariants -- 6 Eliminating local invariants -- 7 Type-checking -- 8 Recursion -- 9 Examples -- 10 A discussion of motives -- 11 Related work -- 12 Conclusions -- A Additional refinement laws -- References -- Authorsโ{128}{153} Addresses