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.
与恶龙缠斗过久,自身亦成为恶龙;凝视深渊过久,深渊将回以凝视…