Modular Specification and Verification of Type Invariants

Part of the Lecture Notes in Computer Science book series (LNCS, volume 2262)


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.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Personalised recommendations