Data Refinement - Model-Oriented Proof Methods and Their Comparison

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.

Détails du produit

• Auteurs: Willem-Paul de Roever, Willem-Paul (Christian-Albrechts Univer De Roever, Willem-Paul Engelhardt De Roever, Kai Engelhardt, Willem-Paul Engelhardt Roever
• Edition: Cambridge University Press ELT
• Langues: Anglais
• Format d'édition: Livre de poche
• Sortie: 18.12.2008
• EAN: 9780521103503
• ISBN: 978-0-521-10350-3
• Pages: 436
• Thème: Cambridge Tracts in Theoretica
• Catégorie: Sciences naturelles, médecine, informatique, technique > Informatique, ordinateurs > Informatique