Code Contracts Support within .NET Framework BCL

Code Contracts were one of the Holy Grails in Computer Science when I received my bachelor’s degree in 1997. Yes, there was research aplenty including my professor Dr. Tim Wahls’ work with the Larch and later Java Modeling Language (JML) approaches to Design By Contracts. However, it was far removed from mainstream programming. Microsoft is poised to change that with Code Contracts.

Code Contracts allow formal specifications to be applied to code. These consist of preconditions, post-conditions, and object invariants. The idea is that code can have its intent made clearer for callers by specifying characteristics of valid use and code that calls code with contracts available can be more reliable by guaranteeing that the contracts aren’t broken. Compile-time checking allows abuse of contracts to be caught very early in the development cycle. An excellent chapter by Jon Skeet from C# in Depth (second edition) covering contracts is available here.

Code Contracts are still a development labs product but Microsoft has already modified some BCL code to support contracts. An earlier draft of Skeet’s chapter illustrates the progress is making. An example showing a case beyond what Code Contracts were NOT aware of is now caught by .NET 4 and the static contract checker! The system random number generator Next function takes two arguments , a lower bound and upper bound, and produces a pseudorandom number >= lower bound and < upper bound. Looking at the BCL source available through Microsoft’s symbol server shows a contract that stipulates that the lower bound can’t be larger than the upper bound.

 int randomNum;  
 Random randomGenerator = new Random();  
 randomNum = randomGenerator.Next(7, 1);  
 //caught as an exception violation   

If we have a function with a precondition that an input number is a valid output of a six-sided die, then the static contract checker uses the contracts built-in to the BCL to support its inference. The static check has found that the output of the Next function will always produce legal input.

 Random randomGenerator = new Random();  
 randomNum = randomGenerator.Next(1, 7);