Design by Contract Framework

• Download source files - 5Kb

This class library provides a Design by Contract framework for use in .NET projects. A Visual Basic .NET version is also included in the download but the following discussion is in C#. In both cases the library can be used by a .NET client written in any .NET language. (Though if the VB.NET version is used IntelliSense code comments will not be visible in the client application.)

"Design by Contract" is a method made famous by Bertrand Meyer in the Eiffel programming language where support is built right into the language constructs.

See Chapter 11 of Object-Oriented Software Construction - 2nd Edition (Prentice Hall, 1997) by Bertrand Meyer and Building Bug-free O-O Software: An Introduction to Design by Contract.

The basic idea is that a class can be viewed as having a contract with its clients whereby the class guarantees to provide certain results (postconditions of its methods) provided that the clients agree to satisfy certain requirements (preconditions of the class's methods). For example, consider a routine:

string FindCustomer(int customerID) 

The precondition might be that customerID is positive. The postcondition might be that we guarantee to find the customer, i.e., possibly among other things, that the return value is a non-empty string.

A failure of the precondition indicates a bug in the caller, the client. A failure of the postcondition indicates a bug in the routine, the supplier. These conditions, or specifications, are implemented by assertion statements. In C/C++ code the assert macro is used for these purposes. The .NET Framework Class Library uses assertion functions available in the System.Diagnostics namespace. By default these generate an "abort, ignore, retry" message box on assertion failure. An alternative approach is to use exception-handling. This is the approach used in the framework that I describe below, although I also wrap the .NET assertion functions as an alternative.

We cannot be as comprehensive in C# as in Eiffel but we can go some of the way. The library provides a set of static methods for defining preconditions, postconditions, class invariants and general assertions and the exception classes that represent them. Methods are also provided that invoke the .NET System.Diagnostics.Trace() assertions as an alternative to throwing exceptions. When debugging, sometimes, you want to be able to ignore assertions and continue stepping through code, especially when routines are still in a state of flux. For example, an assertion may no longer be valid but you still want to have the assertion flagged to remind you that you've got to fix the code (remove the assertion or replace it with another).

After building the code into a C# library you can include a reference to it in a .NET client application written in any .NET language. Then all you need do is import the DesignByContract namespace.

For each project that imports the DesignByContract namespace you can:

1. Generate debug assertions instead of exceptions.
2. Separately enable or disable precondition, postcondition, invariant and assertion checks.
3. Supply a description for each assertion, or not. If you do not the framework will tell you what type of error - precondition, postcondition, etc. - you have generated.
4. Define different rules for Debug and Release builds.

Contracts and Inheritance

There are certain rules that should be adhered to when Design by Contract is used with inheritance. Eiffel has language support to enforce these but in C# we must rely on the programmer. The rules are, in a derived class (Meyer, Chapter 16):

1. An overriding method may [only] weaken the precondition. This means that the overriding precondition should be logically "or-ed" with the overridden precondition.
2. An overriding method may [only] strengthen the postcondition. This means that the overriding postcondition should be logically "and-ed" with the overridden postcondition.
3. A derived class invariant should be logically "and-ed" with its base class invariant.

Example (using pseudo-C# syntax)

class D inherits B

public virtual int B.Foo(int x)
{
  Check.Require(1 < x < 3);
  ...
  Check.Ensure(result < 15);
  return result;
}

public override int D.Foo(int x)
{
  Check.Require (1 < x < 3 or 0 < x < 5); // weakened precondition

  ...
  Check.Ensure (result < 15 and result < 3); // strengthened postcondition

  return result;
}
 

Eiffel has code constructs to support the above. In D.Foo() we would write:

require else 0 < x < 5

meaning "check base class precondition first and if it fails check the derived class version."

ensure then result < 3

meaning "check base class postcondition and the derived class postcondition and ensure they both pass."

For C# we need only write:

Check.Require(0 < x < 5 )
Check.Ensure(result < 3)

making sure that the precondition is always equal to or weaker than the base version and the postcondition is always equal to or stronger than the base version.

For invariants, in B we might have

Check.Invariant(B.a > 0 and B.b > 0);

and in D

Check.Invariant(D.c > 0 and D.d > 0);

The rule says we should combine these in D

Check.Invariant(B.a > 0 and B.b > 0 and D.c > 0 and D.d > 0);

or

Check.Invariant(B.a > 0 and B.b > 0);
Check.Invariant(D.c > 0 and D.d > 0);

Conditional Compilation Constants

For enabling and disabling each type of contract.

These suggestions are based on Meyer p393.

• DBC_CHECK_ALL - Check assertions - implies checking preconditions, postconditions and invariants.
• DBC_CHECK_INVARIANT - Check invariants - implies checking preconditions and postconditions.
• DBC_CHECK_POSTCONDITION - Check postconditions - implies checking preconditions.
• DBC_CHECK_PRECONDITION - Check preconditions only, e.g., in Release build.

So to enable all checks write:

#define DBC_CHECK_ALL // at the top of the file

Alternatively, for a global setting, define the conditional compilation constant in the project properties dialog box. You can specify a different constant in Release builds than in Debug builds. Recommended default settings are:

• DBC_CHECK_ALL in Debug build
• DBC_CHECK_PRECONDITION in Release build

The latter means that only Check.Require statements in your code will be executed. Check.Assert, Check.Ensure and Check.Invariant statements will be ignored. This behaviour is implemented by means of conditional attributes placed before each method in the Check class below.

For example, [Conditional("DBC_CHECK_ALL"), Conditional("DBC_CHECK_INVARIANT")] , placed before a method means that the method is executed only if DBC_CHECK_ALL or DBC_CHECK_INVARIANT are defined.

Examples

A C# client:

using DesignByContract;
...
public void Test(int x)
{
  try
  {
    Check.Require(x > 0, "x must be positive.");
  }
  catch (System.Exception ex)
  {
    Console.WriteLine(ex.ToString());
  }
}
    

You may also wish to incorporate the .NET Framework's own exceptions for invalid arguments, etc. In which case the catch block should be more fine-grained. For example,

using DesignByContract;
...
public void Test(int x)
{
  try
  {
    Check.Require(x > 0, "x must be positive.", 
                      new ArgumentException("Invalid argument.", "x"));
  }
  catch (DesignByContractException ex)
  {
    Console.WriteLine(ex.GetType().ToString() + "\n\n" 
                      + ex.Message + "\n\n" + ex.StackTrace);
    Console.WriteLine("Retrieving exception history...");

    Exception inner = ex.InnerException;

    while (inner != null)
    {
      Console.WriteLine(inner.GetType().ToString() + "\n\n"
                           + inner.Message + "\n\n" + inner.StackTrace);
      inner = inner.InnerException;
    }
  }
  catch (Exception ex)
  {
    Console.WriteLine(ex.GetType().ToString() + "\n\n"
                                 + ex.Message + "\n\n" + ex.StackTrace);
  }
}
    

If you wish to use trace assertion statements, intended for Debug scenarios, rather than exception handling then set

Check.UseAssertions = true;

You can specify this in your application entry point and maybe make it dependent on conditional compilation flags or configuration file settings, e.g.,

#if DBC_USE_ASSERTIONS
Check.UseAssertions = true;
#endif
    

You can direct output to a Trace listener. For example, you could insert

Trace.Listeners.Clear();
Trace.Listeners.Add(new TextWriterTraceListener(Console.Out));

or direct output to a file or the Event Log.

A VB client:

Imports DesignByContract
...
Sub Test(ByVal x As Integer)
  Try
    Check.Require(x > 0, "x must be positive.")
  Catch ex As System.Exception
    Console.WriteLine(ex.ToString())
  End Try
End Sub
    

Limitations

As it stands the library cannot be used for exceptions that need to be remoted. To do this each exception class must be marked as [Serializable] and must also provide a Deserialization constructor as explained in the article, The Well-Tempered Exception by Eric Gunnerson, Microsoft Corporation.

The Framework

Note: In order to view IntelliSense code comments in a client application you need to edit the class library's Project Properties -> Configuration Properties setting. In the Outputs -> XML Documentation section enter: bin\Debug\DesignByContract.xml. The path is the path to your DLL. Also, make sure that the name of the .dll and .xml files both share the same name prefix, i.e., if the library is named DesignByContract then the name of the documentation file should be DesignByContract.xml.

  public sealed class Check
  {
    #region Interface

    /// <summary>

    /// Precondition check.

    /// </summary>

    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT"),
    Conditional("DBC_CHECK_POSTCONDITION"),
    Conditional("DBC_CHECK_PRECONDITION")]
    public static void Require(bool assertion, string message)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new PreconditionException(message);
      }
      else
      {
        Trace.Assert(assertion, "Precondition: " + message);
      }
    }

    /// <summary>

    /// Precondition check.

    /// </summary>

    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT"),
    Conditional("DBC_CHECK_POSTCONDITION"),
    Conditional("DBC_CHECK_PRECONDITION")]
    public static void Require(bool assertion, string message, Exception inner)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new PreconditionException(message, inner);
      }
      else
      {
        Trace.Assert(assertion, "Precondition: " + message);
      }
    }

    /// <summary>

    /// Precondition check.

    /// </summary>

    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT"),
    Conditional("DBC_CHECK_POSTCONDITION"),
    Conditional("DBC_CHECK_PRECONDITION")]
    public static void Require(bool assertion)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new PreconditionException("Precondition failed.");
      }
      else
      {
        Trace.Assert(assertion, "Precondition failed.");
      }
    }

    /// <summary>

    /// Postcondition check.

    /// </summary>

    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT"),
    Conditional("DBC_CHECK_POSTCONDITION")]
    public static void Ensure(bool assertion, string message)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new PostconditionException(message);
      }
      else
      {
        Trace.Assert(assertion, "Postcondition: " + message);
      }
    }

    /// <summary>

    /// Postcondition check.

    /// </summary>

    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT"),
    Conditional("DBC_CHECK_POSTCONDITION")]
    public static void Ensure(bool assertion, string message, Exception inner)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new PostconditionException(message, inner);
      }
      else
      {
        Trace.Assert(assertion, "Postcondition: " + message);
      }
    }

    /// <summary>

    /// Postcondition check.

    /// </summary>

    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT"),
    Conditional("DBC_CHECK_POSTCONDITION")]
    public static void Ensure(bool assertion)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new PostconditionException("Postcondition failed.");
      }
      else
      {
        Trace.Assert(assertion, "Postcondition failed.");
      }
    }

    /// <summary>

    /// Invariant check.

    /// </summary>

    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT")]
    public static void Invariant(bool assertion, string message)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new InvariantException(message);
      }
      else
      {
        Trace.Assert(assertion, "Invariant: " + message);
      }
    }

    /// <summary>

    /// Invariant check.

    /// </summary>

    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT")]
    public static void Invariant(bool assertion, string message, Exception inner)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new InvariantException(message, inner);
      }
      else
      {
        Trace.Assert(assertion, "Invariant: " + message);
      }
    }

    /// <summary>

    /// Invariant check.

    /// </summary>

    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT")]
    public static void Invariant(bool assertion)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new InvariantException("Invariant failed.");
      }
      else
      {
        Trace.Assert(assertion, "Invariant failed.");
      }
    }

    /// <summary>

    /// Assertion check.

    /// </summary>

    [Conditional("DBC_CHECK_ALL")]
    public static void Assert(bool assertion, string message)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new AssertionException(message);
      }
      else
      {
        Trace.Assert(assertion, "Assertion: " + message);
        //Trace.Assert(assertion, "Assertion: " + message);

      }
    }

    /// <summary>

    /// Assertion check.

    /// </summary>

    [Conditional("DBC_CHECK_ALL")]
    public static void Assert(bool assertion, string message, Exception inner)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new AssertionException(message, inner);
      }
      else
      {
        Trace.Assert(assertion, "Assertion: " + message);
      }
    }

    /// <summary>

    /// Assertion check.

    /// </summary>

    [Conditional("DBC_CHECK_ALL")]
    public static void Assert(bool assertion)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new AssertionException("Assertion failed.");
      }
      else
      {
        Trace.Assert(assertion, "Assertion failed.");
      }
    }

    /// <summary>

    /// Set this if you wish to use Trace Assert statements

    /// instead of exception handling.

    /// (The Check class uses exception handling by default.)

    /// </summary>

    public static bool UseAssertions
    {
      get
      {
        return useAssertions;
      }
      set
      {
        useAssertions = value;
      }
    }

    #endregion // Interface


    #region Implementation

    // No creation

    private Check() {}

    /// <summary>

    /// Is exception handling being used?

    /// </summary>

    private static bool UseExceptions
    {
      get
      {
        return !useAssertions;
      }
    }

    // Are trace assertion statements being used?

    // Default is to use exception handling.

    private static bool useAssertions = false;

    #endregion // Implementation


    #region Obsolete

    /// <summary>

    /// Precondition check.

    /// </summary>

    [Obsolete("Set Check.UseAssertions = true and then call Check.Require")]
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT"),
    Conditional("DBC_CHECK_POSTCONDITION"),
    Conditional("DBC_CHECK_PRECONDITION")]
    public static void RequireTrace(bool assertion, string message)
    {
      Trace.Assert(assertion, "Precondition: " + message);
    }


    /// <summary>

    /// Precondition check.

    /// </summary>

    [Obsolete("Set Check.UseAssertions = true and then call Check.Require")]
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT"),
    Conditional("DBC_CHECK_POSTCONDITION"),
    Conditional("DBC_CHECK_PRECONDITION")]
    public static void RequireTrace(bool assertion)
    {
      Trace.Assert(assertion, "Precondition failed.");
    }

    /// <summary>

    /// Postcondition check.

    /// </summary>

    [Obsolete("Set Check.UseAssertions = true and then call Check.Ensure")]
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT"),
    Conditional("DBC_CHECK_POSTCONDITION")]
    public static void EnsureTrace(bool assertion, string message)
    {
      Trace.Assert(assertion, "Postcondition: " + message);
    }

    /// <summary>

    /// Postcondition check.

    /// </summary>

    [Obsolete("Set Check.UseAssertions = true and then call Check.Ensure")]
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT"),
    Conditional("DBC_CHECK_POSTCONDITION")]
    public static void EnsureTrace(bool assertion)
    {
      Trace.Assert(assertion, "Postcondition failed.");
    }

    /// <summary>

    /// Invariant check.

    /// </summary>

    [Obsolete("Set Check.UseAssertions = true and then call Check.Invariant")]
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT")]
    public static void InvariantTrace(bool assertion, string message)
    {
      Trace.Assert(assertion, "Invariant: " + message);
    }

    /// <summary>

    /// Invariant check.

    /// </summary>

    [Obsolete("Set Check.UseAssertions = true and then call Check.Invariant")]
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT")]
    public static void InvariantTrace(bool assertion)
    {
      Trace.Assert(assertion, "Invariant failed.");
    }

    /// <summary>

    /// Assertion check.

    /// </summary>

    [Obsolete("Set Check.UseAssertions = true and then call Check.Assert")]
    [Conditional("DBC_CHECK_ALL")]
    public static void AssertTrace(bool assertion, string message)
    {
      Trace.Assert(assertion, "Assertion: " + message);
    }

    /// <summary>

    /// Assertion check.

    /// </summary>

    [Obsolete("Set Check.UseAssertions = true and then call Check.Assert")]
    [Conditional("DBC_CHECK_ALL")]
    public static void AssertTrace(bool assertion)
    {
      Trace.Assert(assertion, "Assertion failed.");
    }
    #endregion // Obsolete


  } // End Check


  #region Exceptions

  /// <summary>

  /// Exception raised when a contract is broken.

  /// Catch this exception type if you wish to differentiate between

  /// any DesignByContract exception and other runtime exceptions.

  ///

  /// </summary>

  public class DesignByContractException : ApplicationException
  {
    protected DesignByContractException() {}
    protected DesignByContractException(string message) : base(message) {}
    protected DesignByContractException(string message, Exception inner) : 
                                                   base(message, inner) {}
  }

  /// <summary>

  /// Exception raised when a precondition fails.

  /// </summary>

  public class PreconditionException : DesignByContractException
  {
    /// <summary>

    /// Precondition Exception.

    /// </summary>

    public PreconditionException() {}
    /// <summary>

    /// Precondition Exception.

    /// </summary>

    public PreconditionException(string message) : base(message) {}
    /// <summary>

    /// Precondition Exception.

    /// </summary>

    public PreconditionException(string message, Exception inner) : 
                                            base(message, inner) {}
  }

  /// <summary>

  /// Exception raised when a postcondition fails.

  /// </summary>

  public class PostconditionException : DesignByContractException
  {
    /// <summary>

    /// Postcondition Exception.

    /// </summary>

    public PostconditionException() {}
    /// <summary>

    /// Postcondition Exception.

    /// </summary>

    public PostconditionException(string message) : base(message) {}
    /// <summary>

    /// Postcondition Exception.

    /// </summary>

    public PostconditionException(string message, Exception inner) : 
                                              base(message, inner) {}
  }

  /// <summary>

  /// Exception raised when an invariant fails.

  /// </summary>

  public class InvariantException : DesignByContractException
  {
    /// <summary>

    /// Invariant Exception.

    /// </summary>

    public InvariantException() {}
    /// <summary>

    /// Invariant Exception.

    /// </summary>

    public InvariantException(string message) : base(message) {}
    /// <summary>

    /// Invariant Exception.

    /// </summary>

    public InvariantException(string message, Exception inner) : 
                                           base(message, inner) {}
  }

  /// <summary>

  /// Exception raised when an assertion fails.

  /// </summary>

  public class AssertionException : DesignByContractException
  {
    /// <summary>

    /// Assertion Exception.

    /// </summary>

    public AssertionException() {}
    /// <summary>

    /// Assertion Exception.

    /// </summary>

    public AssertionException(string message) : base(message) {}
    /// <summary>

    /// Assertion Exception.

    /// </summary>

    public AssertionException(string message, Exception inner) : 
                                            base(message, inner) {}
  }

  #endregion // Exception classes


} // End Design By Contract