Verification of Object-Oriented Software. The KeY Approach Foreword by K. Rustan M. Leino /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Beckert, Bernhard (Επιμελητής έκδοσης), Hähnle, Reiner (Επιμελητής έκδοσης), Schmitt, Peter H. (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2007.
• Σειρά: Lecture Notes in Computer Science, 4334
• Θέματα: Computer science.; Software engineering.; Programming languages (Electronic computers).; Computer logic.; Mathematical logic.; Artificial intelligence.; Computer Science.; Artificial Intelligence (incl. Robotics).; Logics and Meanings of Programs.; Mathematical Logic and Formal Languages.; Programming Languages, Compilers, Interpreters.; Software Engineering.

Long gone are the days when program veri?cation was a task carried out merely by hand with paper and pen. For one, we are increasingly interested in proving actual program artifacts, not just abstractions thereof or core algorithms. The programs we want to verify today are thus longer, including who...

Πίνακας περιεχομένων:

• A New Look at Formal Methods for Software Construction
• A New Look at Formal Methods for Software Construction
• I: Foundations
• First-Order Logic
• Dynamic Logic
• Construction of Proofs
• II: Expressing and Formalising Requirements
• Formal Specification
• Pattern-Driven Formal Specification
• Natural Language Specifications
• Proof Obligations
• From Sequential Java to Java Card
• III: Using the KeY System
• Using KeY
• Proving by Induction
• Java Integers
• Proof Reuse
• IV: Case Studies
• The Demoney Case Study
• The Schorr-Waite-Algorithm
• Appendices
• Predefined Operators in Java Card DL
• The KeY Syntax.