Abstract

Although invariants have a long history, their meaning in OO designs is still under discussion. OO designs often include functionality that is used by different otherwise unrelated objects (shared functionality). We identify a problem with current interpretations of invariants in such designs. OO designs are often layered, where a layer uses functionality of a lower layer (in particular, shared functionality) but has little or no involvement with higher layers. As a result, higher layers can rely on lower layer invariants and lower layers do not rely on higher layer invariants. This is not reflected by current interpretations of invariants. We propose to make layers explicit in specifications and introduce a new interpretation of invariants that exploits these layers. Furthermore, we present a sound, modular verification technique that ensures the new interpretation is satisfied.
Original languageEnglish
Place of PublicationEindhoven
PublisherTechnische Universiteit Eindhoven
Number of pages43
Publication statusPublished - 2008

Publication series

NameComputer science reports
Volume0801
ISSN (Print)0926-4515

Fingerprint Dive into the research topics of 'A proof system for invariants in layered OO designs'. Together they form a unique fingerprint.

  • Cite this

    Middelkoop, R., Huizing, C., Kuiper, R., & Luit, E. J. (2008). A proof system for invariants in layered OO designs. (Computer science reports; Vol. 0801). Technische Universiteit Eindhoven.