Introduction / 1: |
Motivation / 1.1: |
Specification and Verification Technique / 1.2: |
The Problem / 1.3: |
Modular Correctness / 1.3.1: |
The Frame Problem / 1.3.2: |
Modular Verification of Type Invariants / 1.3.3: |
The Extended State Problem / 1.3.4: |
Alias Control / 1.3.5: |
Modularity Aspects of Programs, Specifications, and Proofs / 1.4: |
Modularity of Programs / 1.4.1: |
Modularity of Universal Specifications / 1.4.2: |
Modularity of Interface Specifications / 1.4.3: |
Modularity of Correctness Proofs / 1.4.4: |
Approach, Outline, and Contributions / 1.5: |
Approach / 1.5.1: |
Outline / 1.5.2: |
Contributions / 1.5.3: |
Related Work / 1.6: |
Specification Techniques / 1.6.1: |
Verification and Analysis Techniques / 1.6.2: |
Mojave and the Universe Type System / 2: |
Mojave: The Language / 2.1: |
The Language Core / 2.1.1: |
Modularity / 2.1.2: |
Universes: A Type System for Flexible Alias Control / 2.2: |
The Ownership Model / 2.2.1: |
The Universe Programming Model / 2.2.2: |
Programming with Universes / 2.2.3: |
Examples / 2.2.4: |
Formalization of the Universe Type System / 2.2.5: |
Discussion / 2.2.6: |
The Semantics of Mojave / 2.3: |
Programming Logic / 3.1: |
Formal Data and State Model / 3.1.1: |
Axiomatic Semantics / 3.1.2: |
Language Properties / 3.1.3: |
Type Safety / 3.2.1: |
Liveness Properties / 3.2.2: |
Properties of Readonly Methods / 3.2.3: |
Correctness / 3.3: |
Correctness of Closed Programs / 3.3.1: |
Correctness of Open Programs: Modular Correctness / 3.3.2: |
Modular Soundness / 3.3.3: |
Composition of Modular Correct Open Programs / 3.3.4: |
Modular Specification and Verification of Functional Behavior / 3.4: |
Foundations of Interface Specifications / 4.1: |
Specification of Functional Behavior / 4.2: |
Abstract Fields / 4.2.1: |
Pre-post-specifications / 4.2.2: |
Verification of Functional Behavior / 4.3: |
Verification of Method Bodies / 4.3.1: |
Proofs for Virtual Methods / 4.3.2: |
Example / 4.3.3: |
Modular Specification and Verification of Frame Properties / 4.4: |
Meaning of Modifies-Clauses / 5.1: |
Explicit Dependencies / 5.1.2: |
Modularity Rules / 5.1.3: |
Formalization of Explicit Dependencies / 5.2: |
Declaration of Dependencies / 5.2.1: |
Axiomatization of the Depends-Relation / 5.2.2: |
Consistency with Representation / 5.2.3: |
Formalization of the Modularity Rules / 5.2.4: |
Axiomatization of the Notdepends-Relation / 5.2.5: |
Formalization of Modifies-Clauses / 5.2.6: |
Verification of Frame Properties / 5.4: |
Local Update Property / 5.4.1: |
Accessibility Properties / 5.4.3: |
Modularity Theorem for Frame Properties / 5.4.4: |
Leino's and Nelson's Work on Dependencies / 5.4.5: |
Other Work on the Frame Problem / 5.5.2: |
Modular Specification and Verification of Type Invariants / 6: |
Motivation and Approach / 6.1: |
Invariant Semantics for Nonmodular Programs / 6.1.1: |
Problems for Modular Verification of Invariants / 6.1.2: |
Specification of Type Invariants / 6.1.3: |
Declaration of Type Invariants / 6.2.1: |
Formal Meaning of Invariants / 6.2.2: |
Verification of Type Invariants / 6.3: |
Verification Methodology / 6.3.1: |
Module Invariants / 6.3.2: |
History Constraints / 6.4.2: |
Conclusion / 6.5: |
Summary and Contributions / 7.1: |
The Lopex Project / 7.2: |
Tool Support / 7.3: |
Directions for Future Work / 7.4: |
Formal Background and Notations / A: |
Formal Background / A.1: |
Notations / A.2: |
Predefined Type Declarations / B: |
Doubly Linked List / C: |
Property Editor / C.2: |
Auxiliary Lemmas, Proofs, and Models / D: |
Auxiliary Lemmas and Proofs from Chapter 3 / D.1: |
Auxiliary Lemmas and Proofs from Chapter 5 / D.2: |
Auxiliary Lemmas and Proofs from Chapter 6 / D.3: |
A Model for the Axiomatization of the Depends-Relation / D.4: |
Bibliography |
List of Figures |
Index |
Introduction / 1: |
Motivation / 1.1: |
Specification and Verification Technique / 1.2: |