Java 2 SDK for Solaris Developer's Guide

Postconditions

Postcondition checks are best implemented via assertions, whether or not they are specified in public methods. For example:


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

In practice, one would not check the second precondition (this.gcd(m).equals(ONE)) prior to performing the computation, because it is wasteful. This precondition is checked as a side effect of performing the modular multiplicative inverse computation by standard algorithms.

Occasionally, it is necessary to save some data prior to performing a computation in order to check a postcondition after it is complete. This can be done with two assert statements and the help of a simple inner class designed to save the state of one or more variables so they can be checked (or rechecked) after the computation. For example, suppose you have a piece of code that looks like this:


void foo(int[] array) {
        // Manipulate array
        ...

        // At this point, array will contain exactly the ints that it did
        // prior to manipulation, in the same order.
    }

Here is how you could modify the above method to turn the textual assertion into a functional one:


 void foo(final int[] array) {

        class DataCopy {
          private int[] arrayCopy;

          DataCopy() { arrayCopy = (int[])(array.clone()); }

          boolean isConsistent() { return Arrays.equals(array, arrayCopy); }
        }

        DataCopy copy = null;

        // Always succeeds; has side effect of saving a copy of array
        assert (copy = new DataCopy()) != null;

        ... // Manipulate array

        assert copy.isConsistent();
     }

Note that this idiom easily generalizes to save more than one data field, and to test arbitrarily complex assertions concerning pre-computation and post-computation values.

The first assert statement (which is executed solely for its side-effect) could be replaced by the more expressive:


  copy = new DataCopy();

but this would copy the array whether or not asserts were enabled, violating the dictum that asserts should have no cost when disabled.