By Kevin McFarlane
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/
We cannot be as comprehensive in C# 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
Examples
A C# client:
using DesignByContract;
...
public void Test(int x)
{
try
{
Check.Require(x > 0, "x must be > 0");
}
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(a > 1, "a must be > 1");
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
{
// Design By Contract Checks.
//
// Each method generates an exception or
// a Trace assertion if the contract is broken.
//
// If you wish to use Trace statements rather than exception handling then call the methods ending in Trace
// e.g., Check.RequireTrace(a > 1, "a must be > 1");
// Then output will be directed to a Trace listener. For example, you could insert
//
// Trace.Listeners.Clear();
// Trace.Listeners.Add(new TextWriterTraceListener(Console.Out));
//
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
