java - 返回 'false' 是方法的有效后置条件吗？

Question

我最近一直在学习后置条件、前置条件和契约设计，但我一直无法找到这个问题的确切答案。

对我来说，后置条件似乎本质上是“该方法在被调用后要实现的目标”。

举个例子

//If x is not equal to y, do something with x and return true. Otherwise, return false.

public boolean example(int x)
{
    if(x != y)
    {
        return true;
        //do something with x.
    }
    else
    {
            return false;
    }
}

在陈述此方法的后置条件时，说它返回“false”是其中之一有意义吗？还是后置条件只是对 x 所做的？

编辑:

这是一个带有实际先决条件的更好示例 -

public boolean example2(Example x)
{
    if (x == a)
    {
        throw new IllegalArgumentException("x must not be the same as a");
    }

    if(x != y)
    {
        return true;
        //do something with x.
    }
    else
    {
            return false;
    }
}

Answer 1

您没有在您的示例 方法中提供任何前置条件或后置条件。您提供的是类不变量。

在检查后置条件之前先在方法中检查前置条件。通常这是通过 assert 为后置条件完成的。

A postcondition states what a method ensures if it has been called by fulfilling its precondition. If the postcondition is violated although the precondition holds, the method (the supplier) has broken the contract (implementation error). In other words a postcondition is a right to the customer and an obligation to the supplier.

报价来源:https://c4j-team.github.io/C4J/examples_postcondition.html

您通常不会返回 true 或 false。后置条件由断言处理。这个 Oracle 页面给出了很好的 examples :

   /**
     * Returns a BigInteger whose value is (this-1 mod m).
     *
     * @param  m the modulus.
     * @return this-1 mod m.
     * @throws ArithmeticException  m <= 0, or this BigInteger
     *         has no multiplicative inverse mod m (that is, this BigInteger
     *         is not relatively prime to m).
     */
    public BigInteger modInverse(BigInteger m) {
        if (m.signum <= 0)
          throw new ArithmeticException("Modulus not positive: " + m);
        if (!this.gcd(m).equals(ONE))
          throw new ArithmeticException(this + " not invertible mod " + m);

        ... // Do the computation

        assert this.multiply(result).mod(m).equals(ONE);
        return result;
    }