Cooperation-based invariants for OO languages

R. Middelkoop, C. Huizing, R. Kuiper, E.J. Luit

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)


In general, invariants may depend on the state of other objects. The approach introduced in this paper allows this for objects of mutually visible classes, in a way that supports modular verification. To this end, dependencies are made explicit by cooperation. In particular, invariants expressing non-hierarchical object relations are supported. Furthermore, an inc-set allows a method to specify explicitly that it does not depend on the validity of a certain invariant. This way, it can be called even when that invariant is violated.
Original languageEnglish
Title of host publicationProceedings of the 2nd International Workshop on Formal Aspects of Component Software (FACS'05, Macao, October 24-25, 2005)
EditorsZ. Liu, L. Barbosa
Publication statusPublished - 2006

Publication series

NameElectronic Notes in Theoretical Computer Science
ISSN (Print)1571-0061


Dive into the research topics of 'Cooperation-based invariants for OO languages'. Together they form a unique fingerprint.

Cite this