Is a return of 'false' a valid postcondition of a method?

Question

I've been learning about postconditions, preconditions, and design by contract recently and I haven't been able to find an exact answer to this question.

To me, a postcondition seems to essentially be 'what the method is meant to have achieved' after being invoked.

Here's an example

//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;
    }
}

When stating the postconditions of this method, would it make sense to say that it returning 'false' is one of them? Or is the postcondition only what is done with x?

Edit:

Here's a better example with an actual precondition -

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

You did not provide any preconditions nor postconditions in your example method. What you provided was a class invariant.

The precondition is checked in the method before the postcondition is checked. Often times this is done via assert for post-conditions.

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.

Quote source: https://c4j-team.github.io/C4J/examples_postcondition.html

You are not returning true or false typically. The postcondition is handled by assertions. The Oracle page on this gives good 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;
    }

Answer 2

Basically, pre+postconditions can be anything, that verifies, that the given interface follows the required behaviour.

As an example: List<E> is an interface. ArrayList<E> is a class, implementing List<E> and exposing expected behaviour. Imagine, you write a set of JUnit tests against List<E> and then execute them against ArrayList<E>. If your ArrayList<E> passes the test - it satisfies the contract of list behaviour.

`
//Precondition
List<Object> objectList = new ArrayList<Object>();
//Postcondition: a newly created list must be empty, if you did not put anything there
assertEquals(0,objectList.size);
//Precondition
Object someObject = new Object();
//Precondition
objectList.add(someObject);
//Postcondition: you get exactly the same element, that you have just put
assertEquals(1,objectList.size);
assertEquals(someObject,objectList.get(0));
`

In your case you have the following:

Precondition: x=something, but not equal to y Postcondition: example(x) is true