java - JML specification in the interface and the implementing class

Question

I am a bit new to java and so while programming i have noticed that i have to give JML annotations to my subroutines. As i was working with object-oriented programming i have noticed the use of interfaces and that i have to declare the method there with JML specification, the questions is, when after i have my interface done and i now implement the methods in the classes who implement the interface, as i declare the class once again should i also specify the JML specification above the class once again or this can be omitted as it is located in the interface?

question from:https://stackoverflow.com/questions/65670988/jml-specification-in-the-interface-and-the-implementing-class

Answer 1

The JML verification tool should be aware of this situation, but you need consult the documentation of the used verification tools. For example, for KeY (an interactive theorem prover for Java/JML) its behavior is well described in the second KeY book, which is similar to Leavens:

In JML, specification inheritance means that instance methods have to obey the specifications of all methods they override. This, together with the inheritance of invariants and history constraints, forces subtypes to be behavioral subtypes [Dhara-Leavens96] [Leavens-Naumann06] [Leavens06b].

So you do not need to repeat the JML contract, and your verification tool should verify the overridden methods against the contract in the super type.