The concept of class invariant in object-oriented programming
Bertrand Meyer, Alisa Arkadova, Alexander Kogtenkov
TL;DR
The paper formalizes class invariants as core consistency properties preserved by all object methods and introduces the Invariant Hypothesis to enable modular verification without relying on programmer-annotated wrap/unwrap constructs. It identifies three practical threats—callbacks, furtive access, and reference leaks—through concrete examples and progressively relaxes a Simple Model's restrictions to address them. The Final rule set combines a Callback Model with a Slicing Model, using selective exports and invariant slicing to handle furtive access and aliasing, culminating in strong and weak variants that balance soundness and modular reasoning. The work advances automated OO verification by embedding invariants into a rigorous axiomatic framework, achieving soundness under increasingly realistic language features, and highlighting practical considerations and limitations such as inheritance and mechanization.
Abstract
Class invariants -- consistency constraints preserved by every operation on objects of a given type -- are fundamental to building, understanding and verifying object-oriented programs. For verification, however, they raise difficulties, which have not yet received a generally accepted solution. The present work introduces a proof rule meant to address these issues and allow verification tools to benefit from invariants. It clarifies the notion of invariant and identifies the three associated problems: callbacks, furtive access and reference leak. As an example, the 2016 Ethereum DAO bug, in which $50 million were stolen, resulted from a callback invalidating an invariant. The discussion starts with a simplified model of computation and an associated proof rule, demonstrating its soundness. It then removes one by one the three simplifying assumptions, each removal raising one of the three issues, and leading to a corresponding adaptation to the proof rule. The final version of the rule can tackle tricky examples, including "challenge problems" listed in the literature.