Click here to Skip to main content
15,867,704 members
Articles / Programming Languages / C#
Article

Design by Contract with Extensible C#

Rate me:
Please Sign up or sign in to vote.
4.86/5 (29 votes)
7 Feb 200613 min read 113.4K   119   73   32
Extensible C# (XC#) can be used for Design by Contract (DbC) in C#. This article compares XC# with Eiffel as a DbC tool.

Introduction

Design by Contract (DbC) is a software development methodology invented by Bertrand Meyer. DbC has a lot in common with the aims of Test-Driven Development (TDD): writing executable assertions in your source code to specify, before you write the implementation, the design and behaviour of your classes. DbC and TDD both emphasize that quality should be built into your software right from the start. Meyer's Eiffel programming language has DbC capabilities built into it.

C# does not support DbC, but Extensible C# (XC#) retrofits DbC via "declarative assertions". (Design by Contract is a trademark of Eiffel Software. Maybe that's why XC# uses the phrase "declarative assertions".) XC# provides a good, if imperfect, approximation to DbC.

What is Design by Contract?

The basic idea behind Design by Contract is that each method in a class is a service provider, and that any method that calls it is a client. The method's interface is a contract, guaranteeing clients that, if they satisfy its preconditions, then it will ensure some post-conditions. Both sides of the bargain are stated as Boolean assertions. If a client calls the method without meeting all of the preconditions, then an exception is thrown identifying a bug in that particular client. On the other hand, if a post-condition fails, then an exception points the finger of blame at the method providing the service.

The great thing about this is that, not only are the bugs identified as soon as they occur, but also who is to be blamed: the client, or the service. By unambiguously specifying responsibilities, DbC reduces the number of bugs written in the first place; then, by checking the assertions as the software runs, DbC dramatically cuts the time taken to detect and fix the remaining bugs.

Why DbC when you can TDD?

That sounds a lot like Test-Driven Development! So why not just install NUnit and get on with writing some unit tests, TDD-style? Why do we need DbC?

TDD is great, but it has a few weaknesses.

First of all, unit tests are weak at expressing the responsibilities of clients. For example, this NUnit test specifies that the PageWidth property of a Document class should return the same value that you put into it:

C#
[Test]
public void PageWidthReturnsSameValue()
{
    Document document = new Document();
    document.PageWidth = 14;
    Assert.AreEqual(14, document.PageWidth);
}

That's a very useful thing to test. There's nothing more annoying than setting a property, only to find that it does some hocus-pocus to return a different value from what you put in. This unit test gives us some confidence that PageWidth doesn't misbehave like that.

Now, what happens if we set it to zero? Maybe this unit test is the specification we want:

C#
[Test]
public void PageWidthIsAlwaysGreaterthanZero()
{
    Document document = new Document();
    document.PageWidth = 0;
    Assert.AreEqual(1, document.PageWidth);
}

This says that setting it to zero actually sets it to 1. We don't want that! Is there some way to write a unit test that prohibits callers from setting it to zero? Well yes, we can specify that it will throw an exception:

C#
[Test, ExpectedException(typeof(ArgumentException))]
public void PageWidthIsAlwaysGreaterthanZero()
{
    new Document().PageWidth = 0;
}

That's an improvement. This unit test states that you'd better not set PageWidth to zero; it also suggests that you'd better not set it to a negative value.

The exception that it throws if you break this rule resembles a precondition to a contract. So, TDD can express the responsibilities of clients - the preconditions - but only in a rather indirect way. It's hard to see the precondition; the name of the unit test PageWidthIsAlwaysGreaterThanZero gives the clearest clue. This is the best TDD can do.

TDD's second weakness is that unit tests can specify contracts only via concrete examples. The two unit tests above only exercise two particular values: 14 and zero. Unit tests are great as a kind of specification-by-example, showing what happens in concrete cases. They are incapable, however, of complete, abstract specifications of what happens for all possible values.

A third weakness of TDD is that unit tests are a poor way to specify and check contracts inherited from a base class. For example, suppose that Document is an abstract class and that its subclasses override PageWidth in various ways, but that they all have to obey the specification of PageWidth shown above. With TDD, you could simply assume that all subclasses will override PageWidth in accordance with the ancestor's specification; this is probably the most common approach, but it's a very poor one. It would be better to copy and paste the ancestor's PageWidth unit tests to the subclasses' tests; this produces unit tests that are still easy to read, but with the usual problems of code duplication. You can eliminate the duplication by having the subclasses' test classes inherit from the ancestor's test class; but this makes the unit tests almost incomprehensible to most people.

Writing contracts with XC#

DbC shines in all three cases. It's excellent at stating both pre- and post-conditions abstractly. The following XC# declarative assertions replace both of the unit tests above:

C#
public abstract void PageWidth
{
    [Ensures("result > 0")]
    get;
    [Requires("value > 0", "PageWidth must be greater than zero")]
    [Ensures("PageWidth == value")]
    set;
}

Note how the assertions state the contract explicitly; i.e. if the client meets the requirement of passing a value greater than zero, then the property ensures that it will always return that same value. The Requires attribute states a precondition; the Ensures attributes state post-conditions. The result variable is automatically declared by XC# and is set to the return value of the property.

Note also how it covers every possible input or output. It's checked every time the property is called. Someone once said that DbC is like unit testing on steroids!

You may have noticed that PageWidth is an abstract property. I made it abstract so that we could concentrate for now on the interface (i.e. the contract), and also address TDD's third weakness. In XC#, as in Eiffel, subclasses inherit contracts from their base class. In fact, they also inherit the contracts of any interfaces that they implement. This is so simple and straightforward, it makes the convoluted somersaults that you would have to go through to achieve the same thing in TDD look like a cruel joke.

When the contract is broken in XC#

Remember how the PageWidthIsAlwaysGreaterThanZero unit test said that PageWidth's setter will throw an ArgumentException? To make that unit test pass, we would have had to implement it thus:

C#
set
{
    if (value <= 0)
        throw new ArgumentException("PageWidth must be greater than zero");
    pageWidth = value;
}

The XC# implementation, by contrast, would be trivial:

C#
set
{
    pageWidth = value;
}

With DbC, there's no need to check the value passed in, because the precondition already does so. If a caller does happen to pass an invalid value, then XC# can throw an exception identifying the bug. This is what Eiffel does too, when a contract is broken, and I find it very effective.

It's not XC#'s default way of handling broken contracts, however. By default, instead of throwing an exception, XC# calls System.Diagnostics.Debug.Assert. A stack trace of the failed assertion can then be picked up, in a Debug build, by a standard .NET TraceListener; for example, if you're debugging in Visual Studio, the Debug Output window will display the error. The assertions therefore do not impact on the performance and code size of a Release build. In either build, there is no exception. So the processing continues. Unless you deliberately set up a TraceListener that throws an exception, the buggy code will just keep running. I don't like this default behaviour, so I've configured XC# to throw exceptions instead. This is a simple matter of adding an assembly-level attribute to your projects. In fact, I've written my own such attribute that tweaks the output a bit; they don't call it Extensible C# for nothing!

XC# is great, but...

XC# is far from perfect as a DbC tool.

XC# does not support class invariants. Whereas pre- and post-conditions are assertions that apply on entry to or exit from a particular method, class invariants are assertions that hold true for the whole of an object's lifetime. Class invariants are AND'ed with the pre- and post-conditions of every public method. They are sometimes said to be the most important kind of assertions in DbC, but XC# lacks them entirely. That's the bad news. The good news is that, because XC# is so extensible, it should be relatively easy to add support for invariants. I haven't attempted to do so; I just simulate invariants manually, which is not great but it's better than nothing.

XC# has no old operator. In Eiffel, this operator is frequently used in post-conditions to guarantee that the state on returning from a method has some relationship to its "old" state, i.e., its state on entry to the method. The lack of an old operator makes it impossible to write many post-conditions in XC#. These assertions can be expressed, however, in concrete form via a unit test. As with invariants, it probably wouldn't be hard to rectify this omission; for example, it should be possible to write an OldAttribute class, which would be evaluated immediately after the preconditions:

C#
[Old("string parent.Name")]
[Ensures("parent.Name == old parent.Name")]

Another serious problem is that inherited preconditions are wrongly AND'ed together, thereby strengthening preconditions. This is directly contrary to the rules of DbC. Once again, XC#'s extensibility comes to the rescue of its own deficiencies, because it should be possible to redefine the semantics of preconditions to conform to what one would expect of a contract. Here's a little program that demonstrates the problem; according to the rules of DbC, the preconditions of Parent.ShowNumber() and Child.ShowNumber() should yield i > 0 || i < 10, which of course is always true, so the program should run successfully to completion; but XC# generates i > 0 && i < 10, causing new Child().ShowNumber(10) to fail:

C#
public class Parent
{
    public static void Main()
    {
        new Parent().ShowNumber(10);
        new Child().ShowNumber(10);
    }

    [Requires("i > 0")]
    public virtual void ShowNumber(int i) {}
}

public class Child: Parent
{
    [Requires("i < 10")]
    public override void ShowNumber(int i) {}
}

Another point of difference with Eiffel is that XC# runs assertions every time there is a call to the method on which the assertions are declared. Eiffel does not run them if the method call is implicitly targeted to the current object. Eiffel therefore incurs a much lower performance penalty from running assertions, because assertions are run less frequently. A nasty side-effect of XC# running them all of the time is that XC# does not prevent stack overflow when an assertion makes recursive calls. Eiffel avoids this by not evaluating assertions when a routine is called within an assertion. I have customized XC# with a similar safeguard so that, for example, the following no longer causes StackOverflowException:

C#
[Ensures("other == null || result == other.Equals(this)")]
public override bool Equals(object other)
{
    return base.Equals(other);
}

There are a few more minor irritants. XC# displays no intellisense for much of the assertion syntax, because parts of the assertions are embedded inside strings. These strings are interpreted at compile time, generating compile-time errors, although it can be easy to miss them because they don't always abort the compilation. Intellisense also does not work when adding an XC# attribute above a property getter or setter; this is a nuisance, but I suspect it's a Visual Studio 2003 bug.

One final complaint: XC#'s assertion syntax is a bit ugly compared with Eiffel. This makes the assertions a bit difficult to read. The assertions are a mixture of attributes and strings. Most of them are placed before the method, but some are placed before each method parameter. It's not too bad, but the Eiffel syntax is much cleaner.

Alternatives to XC#

XC# is not the only way to do DbC in C#. The options I know of are, in order from crudest to best:

  • Option 1: Throw exceptions if pre- or post-conditions are not met. The TDD implementation of PageWidth's setter, shown above, is an example of this approach. This tends to cause chaos.
    • It makes no clear distinction between assertions and exceptions thrown for other purposes;
    • nor does it distinguish between preconditions, post-conditions, and invariants;
    • nor does it support inheritance of contracts;
    • and contracts, instead of being in the interface where they belong, are hidden inside the body of methods.
  • Option 2: Call System.Diagnostics.Debug.Assert or System.Diagnostics.Trace.Assert. This is a small improvement on Option 1, because it distinguishes assertions from other exceptions. Unfortunately, it does not fix the other disadvantages of Option 1, and it introduces a new problem. By default, Assert does not throw exceptions; the defect may be logged, but unless a special TraceListener is written, the program will keep running despite the bug. This is a nuisance during development, because unit tests do not detect the failure and falsely report that everything is OK. On a live system, merely logging defects is potentially dangerous.
  • Option 3: A Design by Contract Framework was published by Kevin McFarlane in 2002. It improves on Option 1 by clearly distinguishing assertions from other exceptions, plus it makes a clear distinction between preconditions, postconditions, and invariants.
  • Option 4: XC# overcomes all of the problems with Option 1. By default, it calls Assert, which has problems mentioned under Option 2, but as noted earlier, it is easily configured to throw exceptions instead. XC# still falls well short of Eiffel, however, as mentioned above.
  • Option 5: C#AL resembles XC#. It has two major DbC features that are missing from XC#: class invariants and the old operator. C#AL also has a rich set of quantifiers. It uses proxy classes, which may be a disadvantage. These are generated by an application, the Assertion Tool; running this separately, rather than as part of the normal compilation, would get in the way of development. I also encountered a problem that the proxy did not wrap an indexer properly, changing the interface to a get_Item() function. On the other hand, proxies avoid cluttering the generated IL of the main assembly. Overall, I suspect C#AL may have a more sound approach than XC#. Its developers, researchers at the University of Havana led by Miguel Katrib, are working on improvements which they have described in several articles in the Spanish magazine dotNetMania. This looks very impressive, but it might be too risky for commercial projects.
  • Option 6: nContract is a Master's thesis which, like XC# and C#AL, allows contracts to be written in strings embedded inside attributes. Like C#AL, it supports invariants and old, and it generates an extra class for each class's contracts. This was only recently brought to my attention, and I haven't had a proper look at it.
  • Option 7. Microsoft's Spec# project is researching adding DbC to C#. It looks comparable in sophistication to Eiffel, but Spec# is unfinished: it's not licensed for commercial development. Microsoft's recent announcements about C# 3.0 didn't mention it, but hopefully DbC will make it into C# 4.0 ... whenever that may be.

XC# therefore seems to be the best way to do DbC in commercial C# work at this date.

Conclusion

Overall, I've found working with XC# to be a pleasure. Design by Contract is such a powerful technique, it's great to be able to use a good approximation of it in C#.

I may have sounded rather harsh with respect to Test-Driven Development. I'm actually a big fan of TDD, and I use both TDD and DbC in conjunction with each other. They actually complement each other nicely, each compensating for the other's shortcomings. This combined approach was described at the XP 2004 conference under the name Specification-Driven Development. Another interesting read, written a few years earlier, is Design by Contract and Unit Testing.

I hope this encourages more people to try out Extensible C#!

License

This article has no explicit license attached to it but may contain usage terms in the article text or the download files themselves. If in doubt please contact the author via the discussion board below.

A list of licenses authors might use can be found here


Written By
Web Developer
Australia Australia
This member has not yet provided a Biography. Assume it's interesting and varied, and probably something to do with programming.

Comments and Discussions

 
GeneralRe: Eiffel.NET Pin
Peter Gummer6-Feb-06 11:18
Peter Gummer6-Feb-06 11:18 
GeneralPostconditions and Invariants Pin
Leslie Sanford2-Feb-06 7:29
Leslie Sanford2-Feb-06 7:29 
GeneralRe: Postconditions and Invariants Pin
Peter Gummer2-Feb-06 11:33
Peter Gummer2-Feb-06 11:33 
GeneralnContract Pin
puzzlehacker2-Feb-06 5:57
puzzlehacker2-Feb-06 5:57 
GeneralRe: nContract Pin
Peter Gummer2-Feb-06 11:38
Peter Gummer2-Feb-06 11:38 
GeneralRe: nContract Pin
Tadeusz Dracz14-Feb-06 3:06
professionalTadeusz Dracz14-Feb-06 3:06 
GeneralRe: nContract Pin
Peter Gummer14-Feb-06 10:39
Peter Gummer14-Feb-06 10:39 

General General    News News    Suggestion Suggestion    Question Question    Bug Bug    Answer Answer    Joke Joke    Praise Praise    Rant Rant    Admin Admin   

Use Ctrl+Left/Right to switch messages, Ctrl+Up/Down to switch threads, Ctrl+Shift+Left/Right to switch pages.