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.
|Title of host publication||Proceedings of the 2nd International Workshop on Formal Aspects of Component Software (FACS'05, Macao, October 24-25, 2005)|
|Editors||Z. Liu, L. Barbosa|
|Publication status||Published - 2006|
|Name||Electronic Notes in Theoretical Computer Science|
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