我对java有点陌生，所以在编程时我注意到我必须给我的子例程提供JML注释。当我使用面向对象编程时，我注意到了接口的使用，并且我必须用JML规范在那里声明方法，问题是，当我完成了接口之后，我现在在实现接口的类中实现方法时，当我再次声明该类时，我是否应该再次在该类之上指定JML规范，或者由于它位于接口中，所以可以省略它？
JML验证工具应该知道这种情况，但您需要查阅所用验证工具的文档。例如，对于KeY(Java/JML的交互式定理证明器(，它的行为在KeY的第二本书中有很好的描述，这本书类似于Leavens:
在JML中，规范继承意味着实例方法必须遵守它们覆盖的所有方法的规范。这个，一起通过不变量和历史约束的继承，力行为亚型[Dara-Leavens96][Leavens-Naumann06][Leavens06b]。
因此，您不需要重复JML约定，您的验证工具应该根据超级类型中的约定验证重写的方法。