Virginity
Virginity: A contribution to the specification of object-oriented software n object-oriented programs built in layers, an object at a higher level of abstraction is implemented by objects at lower levels of abstraction. It is usually crucial to correctness that a lower-level object not be shared among several higher-level objects. This paper unveils some difficulties in writing procedure specifications strong enough to guarantee that a lower-level object can be used in the implementation of another object at a higher level of abstraction. To overcome these difficulties, the paper presents virginity, a convenient way of specifying that an object is not globally reachable and thus can safely be used in the implementation of a higher-level abstraction.
Keywords for this software
References in zbMATH (referenced in 5 articles , 1 standard article )
Showing results 1 to 5 of 5.
Sorted by year (- Müller, Peter: Modular specification and verification of object-oriented programs (2002)
- Boyland, John: Alias burying: Unique variables without destructive reads (2001)
- Clarke, David G.; Noble, James; Potter, John M.: Simple ownership types for object containment (2001)
- Leino, K. Rustan M.; Stata, Raymie: Virginity: A contribution to the specification of object-oriented software (1999)
- Potter, John; Clarke, David; Noble, James: A mode system for flexible alias protection (1998)