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)

Abstract

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
Pages225-237
DOIs
Publication statusPublished - 2006

Publication series

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

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

  • Cite this

    Middelkoop, R., Huizing, C., Kuiper, R., & Luit, E. J. (2006). Cooperation-based invariants for OO languages. In Z. Liu, & L. Barbosa (Eds.), Proceedings of the 2nd International Workshop on Formal Aspects of Component Software (FACS'05, Macao, October 24-25, 2005) (pp. 225-237). (Electronic Notes in Theoretical Computer Science; Vol. 160). https://doi.org/10.1016/j.entcs.2006.05.025