public bool SendOrdersWithContract(Customer customer)
{
  // Preconditions
  Contract.Requires<ArgumentNullException>(
    customer != null, "customer");

  Contract.Requires(customer.CustomerID > 0,
    "Customer must be registered.");

  // Postcondition
  Contract.Ensures(
    Contract.Result<bool>() == HasErrors);

  // Assumption
  Contract.Assume(
    NetworkInterface.GetIsNetworkAvailable(),
    "Network is not available.");

  // Assertion
  Contract.Assert(
    NetworkInterface.GetIsNetworkAvailable(),
    "Network is not available.");

  // Implementation skipped...

  return HasErrors;
}

[ContractInvariantMethod]
protected void ObjectInvariant()
{
  // Invariant
  Contract.Invariant(
    !string.IsNullOrEmpty(this.SmtpServerName),
    "SMTP server name not initialized.");
}