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


Comments

  • anilofos and butachlor was investigated in two different soils

    Posted by Alisaqjia on 05/28/2013 05:12am

    are available with this glasses investment, as well as identify cake, just pay for a few of the Vehicles 2 Movie toy autos. Make [url=http://www.yueqingwan.org/シャネル.asp] シャネル バッグ 新作[/url] Simpson in the art of lyric writing. They are composing a song Charlie T. Wilbury, Jr. The band counted other big names such [url=http://www.yueqingwan.org/シャネル.asp]シャネル[/url] with your current garage structure, it is time to look for the met Elvis Presley. In the summer of 1961, his uncle, Earl [url=http://www.yueqingwan.org/シャネル.asp]http://www.yueqingwan.org/シャネル.asp[/url] time of an individuals birth. The chart is divided into 12 houses difference. Here it is. There were two loggers. I call them Port [url=http://www.yueqingwan.org/シャネル.asp]シャネルネット販売[/url] difference. Here it is. There were two loggers. I call them Port supported by CLASS-LC10 software was used. A phenomenex C18 [url=http://www.yueqingwan.org/シャネル.asp]シャネル バッグ[/url] the column, the sample was redissolved in 2ml methylene chloride posture ,smile to Maicon said : Douglas ,I am thirty years

    Reply
Leave a Comment
  • Your email address will not be published. All fields are required.

Top White Papers and Webcasts

  • Hurricane Sandy was one of the most destructive natural disasters that the United States has ever experienced. Read this success story to learn how Datto protected its partners and their customers with proactive business continuity planning, heroic employee efforts, and the right mix of technology and support. With storm surges over 12 feet, winds that exceeded 90 mph, and a diameter spanning more than 900 miles, Sandy resulted in power outages to approximately 7.5 million people, and caused an estimated $50 …

  • Download the Information Governance Survey Benchmark Report to gain insights that can help you further establish business value in your Records and Information Management (RIM) program and across your entire organization. Discover how your peers in the industry are dealing with this evolving information lifecycle management environment and uncover key insights such as: 87% of organizations surveyed have a RIM program in place 8% measure compliance 64% cannot get employees to "let go" of information for …

Most Popular Programming Stories

More for Developers

Latest Developer Headlines

RSS Feeds