Modular Specification and Verification of Type Invariants
Type invariants (invariants for short) describe well-formedness criteria of objects and object structures. Based on a discussion of an invariant semantics for nonmodular programs, we explain the problems of modular verification of invariants and our approach to their solution. By regarding invariants as boolean abstractions, we apply our techniques for alias and dependency control to invariants. Thereby, we define a meaning for type invariants that is appropriate for modular verification. We show how invariants can be verified modularly, discuss the expressiveness of our invariants, and present related work.
Unable to display preview. Download preview PDF.