On the Refinement Calculus
Published on 9. December 1993
Book
Hardback
XI, 159 pages
978-3-540-19809-3 (ISBN)
Description
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.
More details
Series
Edition
1992
Language
English
Place of publication
London
United Kingdom
Publishing group
Springer Berlin
Target group
College/higher education
Professional and scholarly
Illustrations
biography
Dimensions
Height: 23.5 cm
Width: 15.5 cm
Weight
425 gr
ISBN-13
978-3-540-19809-3 (9783540198093)
DOI
10.1007/978-1-4471-3273-8
Schweitzer Classification
Other editions
Additional editions
Carroll Morgan | Trevor Vickers
On the Refinement Calculus
Book
12/1994
Springer
€53.49
Shipment within 10-15 days
Content
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 "mean" 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.- Acknowledgements.- A Additional refinement laws.- References.- Authors' Addresses.