More Declarative Spec. Examples

/*This one does not determine the outcome but it is
  still useful to clients. */
public boolean maybePrime ()
  // effects: if this BigInteger is composite, returns false


/*Same here, we don't know in which order they will be
    notified */

public void addObserver(Observer o)
  // modifies: this
  // effects: this.observers  = this.observers + {o}

public void notifyObservers()
  // modifies the objects in this.observers
  // effects: calls o.notify on each observer o in this.observers