Dot Net

Design By Contract (DBC)

I want to discuss a concept I first read about when going through the "Pragmatic Programmer" book. By the way this is an awesome book I recommend for every programmer. The book has tons of nuggets of helpful tidbits that every developer will find useful.

The term Design By Contract (DBC) is a term coined by Bertrand Meyer in connection with the Eiffel programming language but can be applied  to any object oriented programming language including .NET. although not as elegantly as Eiffel since DBC is built right into that language. It is a technique that focuses on documenting and agreeing to the rights and responsibilities of software modules to ensure program correctness - doing no more or no less than a program claims to do. The documentation and verification is at the heart of Design by Contract.

Every method has some functionality. The method may have some expectation of the state of the world before it is called as well as make some conclusion about the state of the world after being called. The 3 components of DBC is as follows:

Preconditions: These must be true in order by the routine to be called: These form the conditions or obligations to be guaranteed on entry by any client module that calls the method. A routine should thus never be called when its preconditions would be violated. It is the caller's responsibility to pass good data or set the conditions required before calling the routine.

Post Conditions: This describes what the routine is guaranteed to do and this describes the state of the world when the routine is done. This in essence describes what the callee is expected to do and what the caller should expect after calling the routine.

Class Invariants: A class ensures that this condition is always true from the perspective of the caller. While processing the routine, this invariant may temporarily not hold, but by the time the routine exits and returns control, the invariant must be true.


The contract between a routine and any potential caller can thus be read thus:
If all the routine's preconditions are met by the caller, the routine shall guarantee that all post conditions and invariants will be true when it completes.


Below is a DBC example of a routine that inserts a data value into a unique ordered list. In the example below:

public void insertNode(Node aNode)

The precondition might be that it does not already contain aNode i.e. Contains(aNode) == false;
Post condition might be that it will contain aNode i.e. Contains(aNode) == true;
The invariant could be
    foreach( Node n in nodes)
        if ( node.Prev() != null ) {
          Implies that (  n.value CompareTo (n.Prev().value) > 0 )


 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. These assertions should not have side effects.
Unlike Effiel which has DBC built into the language, C# implements DBC via assertions or exception handling.
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.

The implementation of the DBC for C# could be such.

public void insertNode( Node aNode) {
    // precondition
     Trace.Assert( nodes.Contains(aNode) == false )

   ... code logic to insert the node into the list in a unique ordered fashion

   //  post condition
   Trace.Assert( nodes.Contains(aNode) == true )

}


The invariant can be tested by the caller of the routine.
foreach( Node n in nodes)  {
  if ( node.Prev() != null ) {
      Trace.Assert (  n.value.CompareTo (n.Prev().value) > 0 )
  }
}


If either party fails to live up to the terms of the contract then a remedy ( which was previously agreed to ) is invoked - an exception is raised or the program terminates for instance.