'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.

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

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.