Data Refinement - Model-Oriented Proof Methods and Their Comparison

Klappentext Graduate text in formal methods in computer science. Zusammenfassung Graduate text in formal methods in computer science. Inhaltsverzeichnis 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; Part II. Applications: 11. Reynolds' method; 12. VDM; 13. Z, Hehner's method and Back's refinement calculus; 14. Refinement methods due to Abadi & Lamport and Lynch. 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.

Product details

• Authors: Willem-Paul de Roever, Willem-Paul (Christian-Albrechts Univer De Roever, W. Deroever, Kai Engelhardt, Kai Englehardt, W. -P De Roever, W.-P. De Engelhardt Roever, W-.P.de Engelhardt Roever
• Publisher: Cambridge University Press ELT
• Languages: English
• Product format: Hardback
• Released: 03.12.1998
• EAN: 9780521641708
• ISBN: 978-0-521-64170-8
• No. of pages: 436
• Series: Cambridge Tracts in Theoretica
• Subject: Natural sciences, medicine, IT, technology > IT, data processing > IT