Declarative Specifications

• Operational specifications give a series of steps that the method performs.
• Declarative specifications give properties of final outcome.
• Prefer declarative.

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.


  //Or, more formally

  //effects: length (this.seq) = length (this.seq )
  //for all k: 0..length(this.seq)-1 | this.seq [k] =
  //this.seq[length(this.seq)-k-1]

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

public String substring(int i)
  // effects:
  // if i < 0 or i > length (this.seq) throws IndexOutOfBoundsException
  // else returns r such that
  // some sequence s | length(s) = i && s ^ r.seq = this.seq