Cover Image
Read Now

On the Refinement Calculus

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 mathema...

Full description

Bibliographic Details
Other Authors: Morgan, Carroll (Editor), Vickers, Trevor (Editor)
Format: eBook
Language:English
Published: London Springer London 1992, 1992
Edition:1st ed. 1992
Series:Formal Approaches to Computing and Information Technology (FACIT)
Subjects:
Computer Science
Mathematical Analysis
Analysis
Online Access:
Collection: Springer Book Archives -2004 - Collection details see MPG.ReNa
Table of Contents:
  • 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
  • 5Soundness
  • 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’ Addresses
  • 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

Similar Items