Design by Contract Framework for .Net

Environment:
C#, Visual Studio .Net, Windows 2000 SP2, Windows XP Professional


This C# class library provides a Design by Contract framework for use in .Net projects. 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 http://www.eiffel.com/doc/manuals/technology/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, e.g., 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());
}
}

If you wish to use Trace statements rather than exception handling then call the methods ending in Trace. e.g.,

Check.RequireTrace(x > 0, "x must be positive"); 

Then output will be directed to a Trace listener. For example, you could insert

Trace.Listeners.Clear();

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

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

The Framework

using System;
using System.Diagnostics;

namespace DesignByContract
{
    public sealed class Check
    {
       // No creation
       private Check() {}

       [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 (!assertion) throw new
                            PreconditionException(message);
       }

       [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 (!assertion) throw new
                     PreconditionException(message, inner);
       }

       [Conditional("DBC_CHECK_ALL"),
       Conditional("DBC_CHECK_INVARIANT"),
       Conditional("DBC_CHECK_POSTCONDITION"),
       Conditional("DBC_CHECK_PRECONDITION")]
       public static void Require(bool assertion)
       {
         if (!assertion) throw new PreconditionException();
       }

       [Conditional("DBC_CHECK_ALL"),
       Conditional("DBC_CHECK_INVARIANT"),
       Conditional("DBC_CHECK_POSTCONDITION")]
       public static void Ensure(bool assertion,
                                 string message)
       {
         if (!assertion) throw new
                           PostconditionException(message);
       }

       [Conditional("DBC_CHECK_ALL"),
       Conditional("DBC_CHECK_INVARIANT"),
       Conditional("DBC_CHECK_POSTCONDITION")]
       public static void Ensure(bool assertion,
                                 string message,
                                 Exception inner)
       {
         if (!assertion) throw new
                    PostconditionException(message, inner);
       }

       [Conditional("DBC_CHECK_ALL"),
       Conditional("DBC_CHECK_INVARIANT"),
       Conditional("DBC_CHECK_POSTCONDITION")]
       public static void Ensure(bool assertion)
       {
        if (!assertion) throw new PostconditionException();
       }

       [Conditional("DBC_CHECK_ALL"),
       Conditional("DBC_CHECK_INVARIANT")]
       public static void Invariant(bool assertion,
                                    string message)
       {
         if (!assertion) throw new
                               InvariantException(message);
       }

       [Conditional("DBC_CHECK_ALL"),
       Conditional("DBC_CHECK_INVARIANT")]
       public static void Invariant(bool assertion,
                                    string message,
                                    Exception inner)
       {
         if (!assertion) throw new
                        InvariantException(message, inner);
       }

       [Conditional("DBC_CHECK_ALL"),
       Conditional("DBC_CHECK_INVARIANT")]
       public static void Invariant(bool assertion)
       {
         if (!assertion) throw new InvariantException();
       }

       [Conditional("DBC_CHECK_ALL")]
       public static void Assert(bool assertion,
                                 string message)
       {
         if (!assertion) throw new
                           AssertionException(message);
       }

       [Conditional("DBC_CHECK_ALL")]
       public static void Assert(bool assertion)
       {
         if (!assertion) throw new AssertionException();
       }

       [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);
       }

       [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.");
       }

       [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);
       }

       [Conditional("DBC_CHECK_ALL"),
       Conditional("DBC_CHECK_INVARIANT"),
       Conditional("DBC_CHECK_POSTCONDITION")]
       public static void EnsureTrace(bool assertion)
       {
         Trace.Assert(assertion, "Postcondition failed.");
       }

       [Conditional("DBC_CHECK_ALL"),
       Conditional("DBC_CHECK_INVARIANT")]
       public static void InvariantTrace(bool assertion,
                                         string message)
       {
         Trace.Assert(assertion,  "Invariant: " + message);
       }

       [Conditional("DBC_CHECK_ALL"),
       Conditional("DBC_CHECK_INVARIANT")]
       public static void InvariantTrace(bool assertion)
       {
         Trace.Assert(assertion, "Invariant failed.");
       }

       [Conditional("DBC_CHECK_ALL")]
       public static void AssertTrace(bool assertion,
                                      string message)
       {
         Trace.Assert(assertion, "Assertion: " + message);
       }

       [Conditional("DBC_CHECK_ALL")]
       public static void AssertTrace(bool assertion)
       {
         Trace.Assert(assertion, "Assertion failed.");
       }

   } // End Check

   // Exception Classes

   public class AssertionException :
                                System.ApplicationException
   {
       public AssertionException() {}
       public AssertionException(string message) :
                                           base(message) {}
       public AssertionException(string message,
                 Exception inner) : base(message, inner) {}
   }

   public class PreconditionException :
                             System.ApplicationException
   {
     public PreconditionException() {}
     public PreconditionException(string message) :
                                        base(message) {}
     public PreconditionException(string message,
                 Exception inner) : base(message, inner) {}
   }

   public class PostconditionException :
                                System.ApplicationException
   {
     public PostconditionException() {}
     public PostconditionException(string message) :
                                           base(message) {}
     public PostconditionException(string message,
                 Exception inner) : base(message, inner) {}
   }

   public class InvariantException : System.ApplicationException
   {
     public InvariantException() {}
     public InvariantException(string message) : base(message) {}
     public InvariantException(string message, Exception inner) :
                    base(message, inner) {}
   }

} // End Design By Contract 

Downloads

Download source – 2 Kb

More by Author

Previous article
Next article

Get the Free Newsletter!

Subscribe to Developer Insider for top news, trends & analysis

Must Read