The documentation for Commons Math's SparseGradient.multiply is
/** Compute this × a.
* @param a element to multiply
* @return a new element representing this × a
* @throws NullArgumentException if {@code a} is {@code null}.
*/
The translated postcondition is result.equals(a).
This expression is type-correct, but the documentation says that the return value is fresh, so this should be translated into (!result.equals(this)) && (!result.equals(a)).
The documentation for Commons Math's
SparseGradient.multiply
isThe translated postcondition is
result.equals(a)
. This expression is type-correct, but the documentation says that the return value is fresh, so this should be translated into(!result.equals(this)) && (!result.equals(a))
.