Book contents
- Frontmatter
- Contents
- Preface
- Part I Theory
- 1 Introduction to Data Refinement
- 2 Simulation as a Proof Method for Data Refinement
- 3 Relations and Recursion
- 4 Properties of Simulation
- 5 Notation and Semantics
- 6 A Hoare Logic
- 7 Simulation and Hoare Logic
- 8 An Extension to Total Correctness
- 9 Simulation and Total Correctness
- 10 Refinement Calculus
- Picture Gallery
- Part II Applications
- Appendix A An Introduction to Hoare Logic
- Appendix B A Primer on Ordinals and Transfinite Induction
- Appendix C Notational Convention
- Appendix D Precedences
- Bibliography
- Index
7 - Simulation and Hoare Logic
Published online by Cambridge University Press: 03 May 2010
- Frontmatter
- Contents
- Preface
- Part I Theory
- 1 Introduction to Data Refinement
- 2 Simulation as a Proof Method for Data Refinement
- 3 Relations and Recursion
- 4 Properties of Simulation
- 5 Notation and Semantics
- 6 A Hoare Logic
- 7 Simulation and Hoare Logic
- 8 An Extension to Total Correctness
- 9 Simulation and Total Correctness
- 10 Refinement Calculus
- Picture Gallery
- Part II Applications
- Appendix A An Introduction to Hoare Logic
- Appendix B A Primer on Ordinals and Transfinite Induction
- Appendix C Notational Convention
- Appendix D Precedences
- Bibliography
- Index
Summary

- Type
- Chapter
- Information
- Data RefinementModel-Oriented Proof Methods and their Comparison, pp. 132 - 145Publisher: Cambridge University PressPrint publication year: 1998