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.

翻译：类不变量——对给定类型对象的每次操作都保持一致性的约束——是构建、理解和验证面向对象程序的基础。然而，在验证过程中，它们会带来尚未得到普遍接受的解决方案的困难。本研究引入了一种证明规则，旨在解决这些问题，使验证工具能够受益于不变量。它阐明了不变量的概念，并识别出三个相关的问题：回调、隐蔽访问和引用泄漏。以2016年价值5000万美元被盗的以太坊DAO漏洞为例，该漏洞源于使不变量失效的回调。讨论从简化的计算模型和相关的证明规则开始，展示了其可靠性。然后逐一移除三个简化假设，每次移除都会引发三个问题之一，并导致对证明规则的相应调整。该规则的最终版本能够处理棘手的示例，包括文献中列出的“挑战性问题”。