Enforce behavioral subtyping on @param of overridden method in subclass

[bjkeller]

For the classes

package pkg;

public class SuperClass {
  /**
   * @param count  the object count, must be positive
   */
  public void methodWithOverride(int count) {}

  /**
  * @param count  the something count, must be positive
  */
  public void methodWithoutOverride(int count) {}
}

and

package pkg;

public class SubClass extends SuperClass {
  /**
  * @param count the count of things, must be less than 3
  */
  @Override
  public void methodWithOverride(int count) {
    super.methodWithOverride(count);
  }
}

Toradocu generates the condition count > 0 for SuperClass.methodWithOverride(count), and count < 3 for SubClass.methodWithOverride(count). This, technically, is correct in general since the overriding method could change the behavior, even it it would be bad code. But, in this case the overriding method calls super.methodWithOverride(count) where count must be positive, and so the condition should be count > 0 && count < 3.

[khaeghar]

Does this happens with @throws too?

So, a fix could be reading the .java and identify the super.methodWithOverride call, then just add the condition since the override tag does not provide that information.

Other option would be to add it without contemplations, just by reading the @override tag and just adding all the conditions. Is it correct to suppouse that every overrided method gets the same pre-conditions that the inherited method has in the other class?

[bjkeller]

I haven't tried with @throws.

In principle, the pre-conditions stated for the superclass method should hold for all overrides, but it doesn't have to be true in practice. The only reason the condition should be enforced in this case is the explicit call to the superclass method.

[albertogoffi]

I don't think is a good idea to assume that all the pre-conditions stated for a superclass method are valid for the overrides if the overrides have their own Javadoc specification (if not, the Javadoc comment is inherited and therefore the pre-conditions).

I'd rather say that the Javadoc comment of the override method in the example is wrong and should be fixed. I understand though that the composition of Javadoc comments is almost impossible, and that's why probably developers in some cases (wrongly) rewrite only part of the Javadoc.

[mernst]

Behavioral subtyping requires that when overriding a method, the specification can only be strengthened, never weakened. This means that every post-condition on the overridden implementation is also true of the overriding implementation. These postconditions may be strengthened or new ones may be added, but the old ones must also hold. An overriding implementation can weaken pre-conditions, but must never strengthen them.

I agree that it can be confusing if there is no {@inheritDoc} clause in the overriding method, but that doesn't change the requirements of behavioral subtyping.

Regarding Ben's concrete example:

public class SuperClass {
  /** @param count  the object count, must be positive */
  public void methodWithOverride(int count) {}
}

public class SubClass extends SuperClass {
  /** @param count the count of things, must be less than 3 */
   @Override
   public void methodWithOverride(int count) { ... }
}

the pre-conditions stated for the superclass method should hold for all overrides,

The pre-conditions for the superclass method may be overridden and weakened.

the [pre]condition should be count > 0 && count < 3

This precondition is not correct. The two conditions should be joined with "or" rather than with "and". An overriding implementation is allowed to expand, but not to contract, the set of possible arguments.

Consider a client:

  client(SuperClass x) {
    x.methodWithOverride(4);
  }

The call methodWithOverride(4) should work. A call to client() is allowed to pass in a SubClass instead of a SuperClass. In that case, the source code that mentions SuperClass.methodWithOverride()' actually invokesSubClass.methodWithOverride()at run time, but the code should still work. Thus, any arguments that are legal to pass toSuperclass.methodWithOverride()must be legal to pass to SubClass.methodWithOverride; the call toSubClass.methodWithOverride()is not allowed to fail where the specification ofSuperClasssays thatSuperClass.methodWithOverride()` will succeed.

(The source code in the body of the implementation is not relevant to reasoning about the specification.)

Consider some other examples: a superclass search routine might work only for sorted input arrays, but a subclass might work for any array. Or, a superclass routine might only handle non-negative numbers, but a subclass might also handle negative numbers.

Because it's wrong for SubClass.methodWithOverride() to forbid 4 as an argument, Toradocu should help the user find the error. Toradocu can do so by logically comparing the specifications to make sure that the programmer has not incorrectly weakened a specification. (There are libraries that can help with this.) Toradocu can also do so by outputting conditions that satisfy behavioral subtyping, and then tests may fail at run time, for example if Randoop generates a call to methodWithOverride whose receiver is a SubClass and whose argument is 4.

In addition to helping users to find errors where the specification is incorrectly weakened through changes to pre-conditions, Toradocu should find errors due to incorrect changes to postconditions or throws clauses (where throws clauses are akin to preconditions). Let's make sure it does so, because this is a rich source of user confusion and errors that Toradocu can reveal.

[albertogoffi]

Thanks @mernst for the interesting clarification. I did not think about this problem in terms of behavioral subtyping.

I agree that Toradocu can help developers in avoiding such kind of errors, specifically because the widening of pre- and post-conditions is not checked or enforced by the compiler. In general, this is a nice area to further develop Toradocu.