Blick ins Buch

On the Refinement Calculus

Carroll Morgan, Trevor Vickers (Herausgeber)

Buch | Softcover

XI, 159 Seiten

1994
Springer Berlin (Verlag)
978-3-540-19931-1 (ISBN)

Lese- und Medienproben

Inhaltsverzeichnis (PDF)

Artikel merken

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

Erscheint lt. Verlag	13.12.1994
Reihe/Serie	Formal Approaches to Computing and Information Technology (FACIT)
Zusatzinfo	XI, 159 p.
Verlagsort	London
Sprache	englisch
Maße	155 x 235 mm
Gewicht	280 g
Themenwelt	Mathematik / Informatik ► Informatik ► Programmiersprachen / -werkzeuge
	Mathematik / Informatik ► Informatik ► Theorie / Studium
	Mathematik / Informatik ► Mathematik ► Analysis
Schlagworte	algorithms • Calculus • Distribution • programming • Programming language
ISBN-10	3-540-19931-4 / 3540199314
ISBN-13	978-3-540-19931-1 / 9783540199311
Zustand	Neuware