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年Ethereum DAO 错误,其中5 000万美元被盗,是调回一个变数无效的结果。讨论从简化的计算模型和相关的证明规则开始,显示了其健全性。然后将三个简化的假设之一除去,每个移走都提出三个问题中的一个问题,并导致对证据规则的相应调整。规则的最后版本可以解决棘手的例子,包括文献中列出的“挑战问题”。