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.