Advertisement

Modular Specification and Verification of Type Invariants

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

Abstract

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Personalised recommendations