On the Refinement Calculus

Häftad, Engelska, 1994

Del i serien Formal Approaches to Computing and Information Technology (FACIT)

559 kr

Beställningsvara. Skickas inom 10-15 vardagar. Fri frakt över 249 kr.

Beskrivning

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.

Produktinformation

Utgivningsdatum:1994-12-13
Mått:155 x 235 x 10 mm
Vikt:277 g
Format:Häftad
Språk:Engelska
Serie:Formal Approaches to Computing and Information Technology (FACIT)
Antal sidor:159
Upplaga:1992
Förlag:Springer-Verlag Berlin and Heidelberg GmbH & Co. KG
ISBN:9783540199311

Utforska kategorier

Systemvetenskap och AI inom Data och IT
Programspråk inom Data och IT

Innehållsförteckning

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.