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.

Dettagli sul prodotto

• Autori: Willem-Paul de Roever, Willem-Paul (Christian-Albrechts Univer De Roever, Willem-Paul Engelhardt De Roever, Kai Engelhardt, Willem-Paul Engelhardt Roever
• Editore: Cambridge University Press ELT
• Lingue: Inglese
• Formato: Tascabile
• Pubblicazione: 18.12.2008
• EAN: 9780521103503
• ISBN: 978-0-521-10350-3
• Pagine: 436
• Serie: Cambridge Tracts in Theoretica
• Categoria: Scienze naturali, medicina, informatica, tecnica > Informatica, EDP > Informatica