There are some convenient shorthands that make it easier to write specifications.

When a method does not modify anything, we specify the return value in a returns clause. If an exception is thrown, the condition and the exception are given in a throws clause. For example, instead of:

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

write

    public boolean startsWith(String prefix)
    // throws: NullPointerException if (prefix = null)
    // returns: true if exists a sequence s such that (prefix.seq ^ s = this.seq)

The use of these shorthands implies that no modifications occur.