Code Contracts in .Net 4.0

Introduction

Microsoft Code Contacts is a very exciting new feature for creating reliable software and enhancing code quality by bringing the advantages of design-by-contract programming in all .NET programming languages. Contract Programming practice was first introduced by Bertrand Meyer in Eiffel programming language.

The contracts classes’ new namespace System.Diagnostics.Contracts is in mscorlib of .NET 4.0, while .NET 3.5 has a small separate library named Microsoft.Contracts which needs an explicit reference.

Benefits

• The Code Contracts provide users with a number of benefits:
  Contracts are declarative - The syntax for code contracts is standard, quite rich and variegated to express preconditions, postconditions, and invariants
• Contracts document the design decisions and facilitate code evaluation
• Improved testing - Code contracts provide static checking, runtime checking and documentation generation
• Contracts static verification helps
  · Early error detection and avoids passing defects downstream
  · Clarify responsibility at API boundaries
• We can set up expectations about the behavior of an interface
• Inherited contracts - A contract defined on a class (concrete or abstract type) or interface is automatically inherited by derived classes, which reduces code duplication
• Reliability, Correctness, Fast Problem Resolution, Adaptability, Usability, and Speed are which enhances quality in External Customer's view
• Readability, Reusability, Easy Maintenance, Easy Diagnosis and Easy Deployment are which enhances quality in Internal Developer's viewGood development practices lead to quality software and help control costs
  

The contract take the form of pre-conditions, post-conditions and object invariant, below is the list of Assertion types and its use. Contracts act as checked documentation of external and internal APIs to programmers, unlike comments, which can become stale with changes in the code.

Precondition
Define what is required on entry to a method. If the caller (client) fails to respect the precondition, the caller is defective and exception is thrown on violation. Failure in precondition suggests client code is defective.

Pre-condition is functionally equivalent to the more common form of the argument validation.

Postcondition
Verifies that code did what it was supposed to do. Failure in postcondition suggests supplier code is defective or environmental.

Object Invariant
Must ALWAYS be true for an object on entry to and exit from any public feature. Once checked on entry to a public feature, it is not checked again until exit from the entry point, even if several other public features are called in the course of execution.

Assertion
Checking and specifying conditions at intermediate points. When an assertion is useful but a precondition or postcondition is not the right choice.

Assumption
Inform static checker of conditions believed to be true. Useful when static checking is used and checker cannot determine correctness of an assertion.

The code contracts are used to improve testing via runtime checking, static checking. For example, you might have rules to which the properties and fields of a given class should always conform to. These rules can then be checked both statically at compile-time using static checker and at runtime when the application executes by the runtime checker.

Static checker looks code before we run it and error messages are conveniently shown in the Visual Studio Error-List window, it finds things as early as possible, as we all knows that finding bugs early is the way to make cost effective changes to our code.

Both static checking and runtime behavior can be configured in the properties window for the project. This allows us to have a strategy to include all the contracts in the initial release of the product, if adoption will be slow. In this scenario, the contracts would allow you to more easily diagnose unusual cases as the product experienced usage by a diverse number of end-users for the first time. Later, these uncommon defects have been repaired, and the product has demonstrated its stability and reliability, you could release a newer version with more limited contracts enabled.

We can also use code contracts for documentation generation. The documentation generator arguments exist in XML doc files with contract information.

Automatic testing tools, such as Pex, take advantage of contracts to generate more meaningful unit tests by filtering out meaningless test arguments that don't satisfy the pre-conditions.

Limitations

• Sometimes post-conditions can be expensive
• Not all violations are recognized by the static checker.

Example

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
//To make code contract classes visible, we need to add a diagnostic namespace.
using System.Diagnostics.Contracts;
namespace CodeContractDemo2008
{
public class Rational
{
int N;
int D;
public Rational(int n, int d)
{
Contract.Requires(0 < n =" n;" d =" d;"> 0);
Contract.Invariant(this.N >= 0);
}

public int ToInt()
{
Contract.Ensures(Contract.Result() >= 0);
return this.N / this.D;
}
}
class Program
{
public static void Foo(int n)
{
Contract.Requires(n > 0);
int x = 0, y = 2;
while (x <= n) { x++; y++; } //We need to prove the assertions after the loop, and we can prove more complex assertions Contract.Assert(y == x + 2); Contract.Assert(x >= 0);
}
static void Main(string[] args)
{
Rational r = new Rational(3, 4);
//Foo(2);
Console.WriteLine(r.ToInt());
}
}
}