Lecture notes in computer science vol:3582 pages:59-74
Formal Methods edition:2005 location:Newcastle, UK date:18-22 July 2005
Sharing of objects between different modules is often necessary to meet speed and resource demands. The invariants that describe properties of shared objects are difficult to maintain because they can be falsifiable by object allocation. This paper introduces creation guards to
obtain a sound and modular methodology that supports such invariants.