Operational specifications give a series of steps that the method performs; pseudocode descriptions are operational.

Declarative specifications don’t give details of intermediate steps. Instead, they just give properties of the final outcome, and how it’s related to the initial state.

The class StringBuffer provides objects that are like String objects but mutable. The reverse method reverses a string. Here’s how it’s specified in the Java API:

    public StringBuffer reverse()
    // modifies: this
    // effects: Let n be the length of the old character sequence, the one contained in the string buffer
    // just prior to execution of the reverse method. Then the character at index k in the new
    // character sequence is equal to the character at index n-k-1 in the old character sequence.

Note that the postcondition gives no hint of how the reversing is done.

Another example, this time from String. The startsWith method tests whether a string starts with a particular substring.

    public boolean startsWith(String prefix)
    // Tests if this string starts with the specified prefix.
    // effects:
    // if (prefix = null) throws NullPointerException
    // else returns true if exists a sequence s such that (prefix.seq ^ s = this.seq)

The final example shows how a declarative specification can express what is often called non-determinism.

y not giving enough details to allow the client to infer the behavior in all cases, the specification makes implementation easier.

There is a class BigInteger in the package java.math whose objects are integers of unlimited size. The class has a method similar to this:

    public boolean maybePrime ()
    // effects: if this BigInteger is composite, returns false

If this method returns false, the client knows the integer is not prime. But if it returns true, the integer may be prime or composite. So long as the method returns false a reasonable proportion of the time, it’s useful.