Modular Specification and Verification of Object-Oriented Programs

• Main Author: Müller, Peter (Author, http://id.loc.gov/vocabulary/relators/aut)
• Corporate Author: SpringerLink (Online service)
• Format: Electronic eBook
• Language: English
• Published: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2002.
• Edition: 1st ed. 2002.
• Series: Lecture Notes in Computer Science, 2262
• Subjects: Computer programming.; Programming languages (Electronic computers).; Software engineering.; Computer logic.; Programming Techniques.; Programming Languages, Compilers, Interpreters.; Software Engineering/Programming and Operating Systems.; Software Engineering.; Logics and Meanings of Programs.

Software systems play an increasingly important role in modern societies. Smart cards for personal identi?cation, e-banking, software-controlled me- cal tools, airbags in cars, and autopilots for aircraft control are only some examples that illustrate how everyday life depends on the good behavior o...

Table of Contents:

• Mojave and the Universe Type System
• The Semantics of Mojave
• Modular Specification and Verification of Functional Behavior
• Modular Specification and Verification of Frame Properties
• Modular Specification and Verification of Type Invariants
• Conclusion
• Formal Background and Notations
• Predefined Type Declarations
• Examples
• Auxiliary Lemmas, Proofs, and Models.