'Design By Contract' in C#

Question

I wanted to try a little design by contract in my latest C# application and wanted to have syntax akin to:

public string Foo()
{
    set {
        Assert.IsNotNull(value);
        Assert.IsTrue(value.Contains("bar"));
        _foo = value;
    }
}

I know I can get static methods like this from a unit test framework, but I wanted to know if something like this was already built-in to the language or if there was already some kind of framework floating around. I can write my own Assert functions, just don't want to reinvent the wheel.

Campy

You should change your accepted answer. – Inscrutable

Answer 1

C# 4.0 Code Contracts

Microsoft has released a library for design by contract in version 4.0 of the .net framework. One of the coolest features of that library is that it also comes with a static analysis tools (similar to FxCop I guess) that leverages the details of the contracts you place on the code.

Here are some Microsoft resources:

• The main Microsoft Research site
• The user manual
• The 2008 PDC presentation
• The 2009 PDC presentation

Here are some other resources:

• Code Contracts for .NET 4.0 - Spec# Comes Alive
• .NET Code Contracts and TDD Are Complementary
• Code Contracts Primer – Part 5: Utilizing Object Invariants
• Code Contracts Primer – Part 6 Interface Contracts

Florenceflorencia

The problem with Spec# is that it is bound to the IDE. Lucky I'm using 4.0 because System.Diagnostics.Contracts is exactly what I was looking for. Attributes + code. Awesome. This should be the answer. Debug.Assert? That is NOT DbC. – Kingston

But any code contracts support is going to disappear with .NET 5.0: github.com/dotnet/docs/issues/6361 – Noenoel

Answer 2

Spec# is a popular microsoft research project that allows for some DBC constructs, like checking post and pre conditions. For example a binary search can be implemented with pre and post conditions along with loop invariants. This example and more:

 public static int BinarySearch(int[]! a, int key)
    requires forall{int i in (0: a.Length), int j in (i: a.Length); a[i] <= a[j]};
    ensures 0 <= result ==> a[result] == key;
    ensures result < 0 ==> forall{int i in (0: a.Length); a[i] != key};
 {
   int low = 0;
   int high = a.Length - 1;

   while (low <= high)
     invariant high+1 <= a.Length;
     invariant forall{int i in (0: low); a[i] != key};
     invariant forall{int i in (high+1: a.Length); a[i] != key};
   {
     int mid = (low + high) / 2;
     int midVal = a[mid];

     if (midVal < key) {
       low = mid + 1;
     } else if (key < midVal) {
       high = mid - 1;
     } else {
       return mid; // key found
     }
   }
   return -(low + 1);  // key not found.
 }

Note that using the Spec# language yields compile time checking for DBC constructs, which to me, is the best way to take advantage of DBC. Often, relying on runtime assertions becomes a headache in production and people generally elect to use exceptions instead.

There are other languages that embrace DBC concepts as first class constructs, namely Eiffel which is also available for the .NET platform.

Holiness

Answer 3

Aside from using an external library, you have a simple assert in System.Diagnostics:

using System.Diagnostics

Debug.Assert(value != null);
Debug.Assert(value == true);

Not very useful, I know.

Barbabra

And that would be compiled out in Release builds. – Othilia

Yes, if in Debug.* they are compiled out of release builds. – Mistranslate

Only problem with this approach is that the check is is still done at runtime. I know a compiler can't verify everything at compile time. But say you require x != null and then invoke f(null), a compiler could warn the user something is not ok. – Noticeable

Answer 4

There has an answer in .net Fx 4.0:

System.Diagnostics.Contracts

http://msdn.microsoft.com/en-us/library/dd264808.aspx

Contract.Requires(newNumber > 0, “Failed contract: negative”);
Contract.Ensures(list.Count == Contract.OldValue(list.Count) + 1);

Bridgetbridgetown

Answer 5

Looking over the code for Moq I saw that they use a class called 'Guard' that provides static methods for checking pre and post conditions. I thought that was neat and very clear. It expresses what I'd be thinking about when implementing design by contract checks in my code.

e.g.

public void Foo(Bar param)
{
   Guard.ArgumentNotNull(param);
} 

I thought it was a neat way to express design by contract checks.

Rawlins

I am sorry for being a necromancer, but the Guard class of Moq is just perfect if you don't wan't to force everyone to install ccrewrite.exe and all that jazz. – Cap

Answer 6

You may want to check out nVentive Umbrella:

using System;
using nVentive.Umbrella.Validation;
using nVentive.Umbrella.Extensions;

namespace Namespace
{
    public static class StringValidationExtensionPoint
    {
        public static string Contains(this ValidationExtensionPoint<string> vep, string value)
        {
            if (vep.ExtendedValue.IndexOf(value, StringComparison.InvariantCultureIgnoreCase) == -1)
                throw new ArgumentException(String.Format("Must contain '{0}'.", value));

            return vep.ExtendedValue;
        }
    }

    class Class
    {
        private string _foo;
        public string Foo
        {
            set
            {
                _foo = value.Validation()
                    .NotNull("Foo")
                    .Validation()
                    .Contains("bar");
            }
        }
    }
}

I wish the Validation extensions were builders so you could do _foo = value.Validation().NotNull("Foo").Contains("bar").Value; but it is what it is (fortunately its open source so making it a builder is a trivial change).

And as an alternative solution you could consider domain validation.

Finally the new M languages, as part of Oslo, support restrictions on their extents and fields which translate both to T-SQL validation and a CLR class with functioning validation tests (though Oslo is a long time off from release).

Moriarty

Answer 7

For my current project (february 2010, VS 2008) I've choose http://lightcontracts.codeplex.com/

Simple, it's just runtime validation, without any weird complexity, you don't need to derive from some 'strange' base classes, no AOP, VS integration which won't work on some developer workstations, etc.

Simplicity over complexity.

Sadden

Answer 8

The most straightforward way, and the way used in the .NET Framework itself, is to do:

public string Foo()
{
    set {
        if (value == null)
            throw new ArgumentNullException("value");
        if (!value.Contains("bar"))
            throw new ArgumentException(@"value should contain ""bar""", "value");

        _foo = value;
    }
}

Weltanschauung

Answer 9

Please note that I created an extremely simple class for DbC in C#, it should work in .NET 6, and any .NET I believe, it is very simple and limited, but it can serve the purpose of using preconditions, postconditions and assertions.

Here it is

namespace System.Diagnostics.Meyer.Contracts
{
    public static class Contract
    {
        private static void Initialize()
        {
            System.Diagnostics.Trace.Listeners.Clear();
            DefaultTraceListener defaultListener;
            defaultListener = new DefaultTraceListener();
            Trace.Listeners.Add(defaultListener);
            defaultListener.LogFileName = @".\Logs\contract.log";
        }

        static Contract()
        {
            Initialize();
        }

        public static void Assert(bool condition, string message = "")
        {
            System.Diagnostics.Trace.Assert(condition, "Assertion violation:", message);
        }

        public static void Require(bool condition, string message = "")
        {
            System.Diagnostics.Trace.Assert(condition, "Precondition violation:", message);
        }

        public static void Ensure(bool condition, string message = "")
        {
            System.Diagnostics.Trace.Assert(condition, "Postcondition violation:", message);
        }
    }
}

and the usage can go something like

        public void Open(LoggerLevel level, string version)
        {
            Contract.Require(version != null, "version != null");
            Contract.Require(_open == false, "_open == false");
            // ...
            _open = true;
            Contract.Ensure(_open == true, "_open == true");
        }

or

        public LoggerLevel Level
        {
            get
            {
                return _level;
            }
            set
            {
                Contract.Require(_open == true, "_open == true");
                if (value != _level)
                {
                    _level = value;
                    if (Level != LoggerLevel.Off)
                    { 
                        WriteContent(GetLevelChangeContent());
                    }
                }
            }
        }

or

    public class Program
    {
        private static Utility _utility = new Utility();

        public static void Main(string[] args)
        {
            Utility utility = _utility;
            Contract.Assert(utility != null, "utility != null");

etc.

Irrawaddy