Design by Contract + Precondition Weakened Example

Design by Contract

(Fowler UML Distilled, 3rd Ed)

Design by Contract uses three particular kinds of assertions: post-conditions, pre-conditions, and invariants. Pre-conditions and post-conditions apply to operations.

A post-condition is a statement of what the world should look like after execution of an operation.
For instance, if we define the operation "square root" on a number, the post-condition would take the form input = result * result, where result is the output and input is the input value.

A pre-condition is a statement of how we expect the world to be before we execute an operation. We might define a pre-condition for the "square root" operation of input > = 0. Such a pre-condition says that it is an error to invoke "square root" on a negative number and that the consequences of doing so are undefined.

An invariant is an assertion about a class.
In essence, this means that the invariant is added to pre-conditions and post-conditions associated with all public operations of the given class.
The invariant may become false during execution of a method, but it should be restored to true by the time any other object can do anything to the receiver.

The invariants and post-conditions of a class must apply to all subclasses. The subclasses can choose to strengthen these assertions but cannot weaken them. The pre-condition, on the other hand, cannot be strengthened but may be weakened.

http://www.stanford.edu/~pgbovine/programming-with-rep-invariants.htm

class Child {

  ...

  private void checkRep() {
    assert (0 <= age < 18);
    assert (birthdate + age == todays_date);
    assert (isLegalSSN(social_security_number));
  }
}

    ... and call checkRep() at the beginning and end of every public method
        The principle here is that clients should only be able to access your object via public methods, so ...
            at the beginning of a method, check to make sure the representation is intact before it starts operating on its internal state (fields)
            at the end of a method, check to make sure the representation is intact before it hands over control back to the client (caller)
        For example, look at the changeSSN() method:

class Child {
  ...

  public void changeSSN(int newSSN) {
    checkRep();
    ... method body ...
    checkRep();
  }


http://earthli.com/news/view_article.php?id=2183

An example for "The pre-condition of the parent class cannot be strengthened but may be weakened by the subclasses."

In general, the sub class may say that 'I don't mind if some requirment by the method from my parent class is not met, I will handle it (differently) in my method'.

- Example: a failback machansim

class Transmitter
{
  public Server Server { get; }

  [Pure]
  public virtual bool ServerIsReachable
  {
    get { return Server.IsReachable; }
  }

  public virtual void SendData(Data data)
  {
     Contracts.Requires(data != null);
     Contracts.Requires(ServerIsReachable);
     Contracts.Ensures(data.State == DataState.Sent);

     Server.Send(data);
  }

  [ContractInvariantMethod]
  protected void ObjectInvariant
  {
    Contract.Invariant(Server != null);
  }
}

class TransmitterWithFallback : Transmitter
{
  public Server FallbackServer { get; }

  [Pure]
  public override bool ServerIsReachable
  {
    get { return Server.IsReachable || FallbackServer.IsReachable; }
  }

  public override void SendData(Data data)
  {
    if (Server.IsReachable)
    {
      base.SendData(data);
    }
    else
    {
      FallbackServer.Send(data);
    }
  }

  [ContractInvariantMethod]
  protected void ObjectInvariant
  {
    Contract.Invariant(FallbackServer != null);
  }
}