接口和实现类中的 JML 规范

Question

我对 java 有点陌生，所以在编程时我注意到我必须为我的子例程提供 JML 注释。当我使用面向对象编程时，我注意到接口的使用，并且我必须使用 JML 规范声明方法，问题是，当我完成接口之后，我现在在类中实现方法实现接口，当我再次声明该类时，我是否也应该在该类上方再次指定 JML 规范，还是可以省略，因为它位于接口中？

Answer 1

JML 验证工具应该意识到这种情况，但您需要查阅所用验证工具的文档。例如，对于 KeyY（Java/JML 的交互式定理证明器），它的行为在第二个 KeY book 中得到了很好的描述，类似于 Leavens：

在 JML 中，规范继承意味着实例方法必须 遵守它们覆盖的所有方法的规范。这，一起 随着不变量和历史约束的继承，力 子类型是行为子类型 [Dhara-Leavens96] [Leavens-Naumann06] [Leavens06b].

所以你不需要重复 JML 合约，你的验证工具应该根据超类型中的合约来验证被覆盖的方法。