我对 java 有点陌生，所以在编程时我注意到我必须为我的子例程提供 JML 注释。当我使用面向对象编程时，我注意到接口的使用，并且我必须使用 JML 规范声明方法，问题是，当我完成接口之后，我现在在类中实现方法实现接口，当我再次声明该类时，我是否也应该再次在该类上方指定 JML 规范，还是可以将其省略，因为它位于接口中？
问问题
46 次
1 回答
0
JML 验证工具应该意识到这种情况，但是您需要查阅使用的验证工具的文档。例如，对于 KeyY（Java/JML 的交互式定理证明器），它的行为在第二本 Keyy book中得到了很好的描述，它类似于Leavens：
在 JML 中，规范继承意味着实例方法必须遵守它们覆盖的所有方法的规范。这与不变量和历史约束的继承一起，迫使子类型成为行为子类型 [Dhara-Leavens96] [Leavens-Naumann06] [Leavens06b]。
所以你不需要重复 JML 合约，你的验证工具应该根据超类型中的合约来验证被覆盖的方法。
于 2021-01-13T21:02:04.027 回答