Flexible Invariants Through Semantic Collaboration
This addresses a modular reasoning problem for developers of sequential object-oriented programs, offering an incremental improvement over prior invariant methodologies.
The paper tackles the challenge of modular reasoning about class invariants in object-oriented programs with inter-object dependencies, presenting semantic collaboration as a methodology that models these dependencies semantically. The evaluation shows it handles various collaboration patterns and is more widely applicable than existing methods.
Modular reasoning about class invariants is challenging in the presence of dependencies among collaborating objects that need to maintain global consistency. This paper presents semantic collaboration: a novel methodology to specify and reason about class invariants of sequential object-oriented programs, which models dependencies between collaborating objects by semantic means. Combined with a simple ownership mechanism and useful default schemes, semantic collaboration achieves the flexibility necessary to reason about complicated inter-object dependencies but requires limited annotation burden when applied to standard specification patterns. The methodology is implemented in AutoProof, our program verifier for the Eiffel programming language (but it is applicable to any language supporting some form of representation invariants). An evaluation on several challenge problems proposed in the literature demonstrates that it can handle a variety of idiomatic collaboration patterns, and is more widely applicable than the existing invariant methodologies.