Flexible Invariants Through Semantic Collaboration

Abstract

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.

22 pages

Cited by in corpus (8)

• AutoProof: Auto-active Functional Verification of Object-oriented Programs
• Inferring Loop Invariants by Mutation, Dynamic Analysis, and Static Checking
• The AutoProof Verifier: Usability by Non-Experts and on Standard Code
• Verifying Functional Correctness Properties At the Level of Java Bytecode
• Class Invariants: Concepts, Problems, Solutions
• Targeted Synthesis for Programming with Data Invariants
• Sound Invariant Checking Using Type Modifiers and Object Capabilities
• Seamless Requirements