Modular Specification and Verification of Object-Oriented Programs面向对象程序的模块规范与验证

1.Introduction
　1.1　Motivation
　1.2　Specification and Verification Technique
　1.3　The Problem
　　1.3.1　Modular Correctness
　　1.3.2　The Frame Problem
　　1.3.3　Modular Verification of Type Invariants
　　1.3.4　The Extended State Problem
　　1.3.5　Alias COntrol
　1.4　Modularity Aspects of Programs，Specifications，and Proo~
　　1.4.1　Modularity of Programs
　　1.4.2　Modularity of Universal Specifications
　　1.4.3　Modularity of Interface Specifications
　　1.4.4　Modularity of Correctness Proos
　1.5　Approach，Outline，and Contributions
　　1.5.1　Approach
　　1.5.2　Outline
　　1.5.3　C0ntributions
　1.6　Related Work
　　1.6.1　Specification Techniques
　　1.6.2Verification and Analysis：Techniques
2.Mojave and the Universe Type System
　2.1　Mojave：The Language
　　2.1.1　The Language Core
　　2.1.2　Modularity
　2.2　Universes：A Type System for Flexible Alias Control
　　2.2.1　The Ownership Model
　　2.2.2　The Universe Programming Model
　　2.2.3　Programming with Universes
　　2.2.4　Examples
　　2.2.5　Formalization of the Universe Type System
　　2.2.6　Discussion
　2.3　Related Wbrk
3.The Semantics of Mojave
4.Modular Specification and Verification of Functional Behaviou
5.Modular Specification and Verification of Frame Properties
6.Modular Specification and Verification of Type Invariants
7.Conclusion
A.Formal Background and Notations
B.Predefined Type Declarations
C.Examples