SRC Technical Note 1997-001

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

K. Rustan M. Leino and Raymie Stata

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 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.

Back to the SRC Technical Notes main page.

• PostScript compressed with UNIX compress -- 72 Kbytes
  
• PostScript compressed with GNU compress (gzip) -- 59 Kbytes
  
• PostScript compressed with ZIP -- 59 Kbytes
  
• PostScript -- 122 Kbytes
  
• Portable Document Format (PDF) -- 64 Kbytes