Code Contracts with .Net 4.0

I don’t know how many times I have seen a method which I have been trying to debug with a whole stack of parameter checking code at the start of the method to ensure nothing weird happens with unexpected input.  This subsequently caused the nicely abstracted methods to be less abstract than originally intended.  Thankfully .Net 4.0 makes life for the developer, and subsequent debuggers a lot easier with Code Contracts.

Code contracts come under the namespace

 System.Diagnostics.Contracts

and the most used class in this is the Contract class.

Pre-Conditions

There are some different flavours of code contracts, the first is Pre-conditions.  This will be similar to the checks done to insure your method hasn’t been passed some incorrect parameters.

e.g. a simple divide example which requires that the divisor isn’t 0

 public float Divide(float a, float b)
 {
     Contract.Requires(b != 0); // line to ensure code contract
     Return a/b;
 }

if this method is called with b as 0, when compiling and doing static analysis in Visual Studio 2010 (depending on the code contract options set on the project options found in the standard project settings in Visual Studio) will either show as an error, therefore not allowing the project to build, or show an error.  There is an override on the Requires method which allows you to put your own warning/error message if the contract is not met:

 Contract.Requires(b != 0, "Parameter b must not be 0 when calling divide");

this analysis is pretty clever and knows when you are trying to trick it ;)

 Console.WriteLine(Divide(1, 1)); // works fine
  
 Console.WriteLine(Divide(1, 0));
 var a = 1;
 a--;
 Console.WriteLine(Divide(1, a)); // finds this too :)
  
 var b = 1;
 Random r = new Random();
 b -= r.Next(2);
 if (b != 0) // without this, there would be an error saying that b could be 0 was unproven
 {
     Console.WriteLine(Divide(1, b));
 }

Post Conditions

These conditions inform on the finishing state of a method, properties of the return types, objects which should not have been modified etc.

e.g.

 public void AddToCollection(Object o)
 {
     // ensure that the collection is not changed if there is a null reference
     Contract.EnsuresOnThrow<NullReferenceException>
         (Contract.OldValue(collection.Count) == collection.Count);
  
     // ensure that the parameter passed in has not been changed
     Contract.Ensures(Contract.OldValue(o) == o);
  
     collection.Add(o);
 }

now if a NullReferenceException is thrown the code contract will ensure that nothing has been added or removed from the collection.

Invariants

Invariants are rules for objects which should only be modified in a certain way throughout their scope.  e.g. collection must not be empty, a value must not be null, a counter must be non-negative…

For these type of rules you need to mark your method with the attribute:

 [ContractInvariantMethod]

Now inside the method we can set up our rules.

 [ContractInvariantMethod]
 private void Validate()
 {
     Contract.Invariant(collection != null);
     Contract.Invariant(collection.Count > 0);
     Contract.Invariant(collection.First() != null);
 }

this will ensure that the collection is initialized, always has at least 1 non-null entry.

Code contracts seem extremely useful and I look forward to writing code and debugging using them.