Virginity: A contribution to the specification of object-oriented software

In object-oriented programs built in layers, an object at a higher level of abstraction is implemented by objects at lower levels of abstraction. It i s usually crucial to correctness that a lower-level object not be shared am ong several higher-level objects. This paper unveils some difficulties in w riting procedure specifications strong enough to guarantee that a lower-lev el object can be used in the implementation of another object at a higher l evel of abstraction. To overcome these difficulties, the paper presents vir ginity, a convenient way of specifying that an object is not globally reach able and thus can safely be used in the implementation of a higher-level ab straction. (C) 1999 Elsevier Science B.V. All rights reserved.