The Concept of Class Invariants in Object-Oriented Programming

- by Ilgiz Mustafin and Alessandro Schena

This research investigates the central role of class invariants in object-oriented programming, particularly within the framework of design by contract. Class invariants are conditions that define a valid state for an object and must consistently hold true during its public interactions. The study emphasizes that while these invariants can be temporarily broken during internal operations, they must be restored before any public method is invoked, ensuring software correctness, predictability, and maintainability.

The exploration extends to complex object relationships, such as mutual dependencies—for example, between two instances in a Person class representing spouses. It identifies key challenges in maintaining invariants in such interconnected systems, including issues like reference leaks. To address these, the research introduces semantic collaboration, a strategy where objects explicitly manage their dependency networks by tracking both their dependents and dependencies.

A notable contribution of the study is the development of invariant slicing, a technique that aligns the enforcement of invariants with the visibility levels of class members. This approach minimizes the annotation effort required in formal verification and enhances scalability in real-world software development.

The research findings are being operationalized through integration into verification and development environments such as AutoProof and EiffelStudio, marking a significant step toward practical adoption of formal methods in mainstream software engineering.