Elevator pitch
Code contracts allow us to define preconditions, post conditions and the likes in our code. These are constructs I first read about when doing a (very) little bit of Eiffel development.
Visual Studio additions
Before we get into Code Contracts let’s just note that they are available in .NET 4.5 but we need to enable their usage and here we need to install a couple of additions to Visual Studio.
So if you’re running Visual Studio 2012 goto Tools | Extensions and Updates and search online for Code Contract Tools – install this. Then find Code Contracts Editor Extensions VS2012 and install this. You’ll have to restart Visual Studio to see the new installs working. So go ahead and do that.
If Visual Studio 2013 I just install Code Contract Tools.
This will install some addition static analysis tools etc. which we’ll look at later, for now let’s code…
Using Code Contracts
Predconditions
Often in our code we’ll have methods which check the arguments passed to a method or possibly check class wide variables have been set etc. Usually the code might take the following form
public void Analyze(string data)
{
if(data == null)
throw new ArgumentNullException("data");
// do something
}
Well first off we can now replace this with a Code Contract precondition. The precondition ofcourse states that for this method to run, this or these preconditions must be met.
public void Analyze(string data)
{
Contract.Requires<ArgumentNullException>(line != null)
}
We could have specified the same precondition without the ArgumentNullException and a ContractException would be thrown instead.
Postconditions
A postcondition specifies the state of a method when it ends. For example, we can declare that we’ll never return a null by declaring the following contract
public static string Analyze(string line)
{
Contract.Requires<ArgumentNullException>(line != null);
Contract.Ensures(Contract.Result<string>() != null);
// do something
return result;
}
Now if we actually did attempt to return null we’d get a ContractException.
Assumptions
So, we can define pre and postconditions, but also we can define assumptions. Basically let’s assume we have our Analyze method (above) but without the pre or postconditions and we want to declare an assumption that the result from Analyze will not be null, we could write
public string Analyze(string data)
{
// do something
return result;
}
static void Main(string[] args)
{
string result = Analyze("Some Text");
Contract.Assume(result != null);
// do something with result
}
Obviously if result is set to null, our contract is violated and the ContractException will be thrown.
Object Invariants
An object invariant basically defines the state of an object. So for example, let’s assume we have a Person class as below
public class Person
{
public Person(string firstName, string lastName)
{
FirstName = firstName;
LastName = lastName;
}
public string FirstName { get; set; }
public string LastName { get; set; }
}
It may be that we want to define a contract which states that FirstName and LastName are not null. We could add preconditions to the constructor – but what if we also wanted to define a contract that says FirstName and LastName are never null, not just within the contructor’s scope.
Now we can add a ContractInvariantMethod as below
public class Person
{
public Person(string firstName, string lastName)
{
FirstName = firstName;
LastName = lastName;
}
public string FirstName { get; set; }
public string LastName { get; set; }
[ContractInvariantMethod]
private void ContractInvariant()
{
Contract.Invariant(FirstName != null && LastName != null);
}
}
Note: We could have had the left and right parts of the && in different Contract.Invariant declarations if we wished, so basically we can have multiple Contract.Invariant in this method.
The method name can be anything you like and can only contain Contract.Invariant statements. A compile time error will occur if you have other code in this method.
Now when we create a Person object if either FirstName or LastName are set to null a ContractException will occur, but better still let’s assume we add a new method to the class which sets one of these variables to null. The ContractInvariantMethod will be called and the contract will be violated leading to a ContactException.
Contracts on interfaces
An interesting use of contracts is with interfaces. Basically if we define an interface it would be nice if we could declare the contract definitions against the interface. Then any implementation could “inherit” the contract definitions.
So let’s look at our Person class again but now add an interface and define some contracts on the interface
[ContractClass(typeof(IPersonContract))]
public interface IPerson
{
string FirstName { get; set; }
string LastName { get; set; }
}
[ContractClassFor(typeof(IPerson))]
internal abstract class IPersonContract : IPerson
{
public string FirstName
{
get
{
Contract.Ensures(Contract.Result<string>() != null);
return default(string);
}
set { Contract.Requires(value != null); }
}
public string LastName
{
get
{
Contract.Ensures(Contract.Result<string>() != null);
return default(string);
}
set { Contract.Requires(value != null); }
}
}
public class Person : IPerson
{
public Person(string firstName, string lastName)
{
FirstName = firstName;
LastName = lastName;
}
public string FirstName { get; set; }
public string LastName { get; set; }
}
So the interface is a standard interface except that we are declaring (using the ContractClass attribute) that the IPersonContract class includes contract definitions for the interfaces. Likewise on the IPersonContract abstract class. Yes, it’s mean’t to be abstract and implement the interface. Now when we return values, just use default(<type>) so all will compile and add your pre or postconditions. Unfortunately it doesn’t look like we can add a ContractInvariantMethod method to this abstract class (or at least we can but it doesn’t appear to do anything in the current release of .NET).
ContractAbbreviator
The ContractAbbreviatorAttribute is used on a method to denote it contains contract data which, when the method is called from another method in essence runs the contract checks in that method – eh ? It’s a bit like creating a C style macro and having it inlined in a method – eh ?
It’s a was to reuse contracts.
Okay let’s see an example
public class Person
{
public string FirstName { get; set; }
public string LastName { get; set; }
[ContractAbbreviator]
private void Validate()
{
Contract.Ensures(FirstName != null);
Contract.Ensures(LastName != null);
}
public void Amend()
{
Validate();
}
}
Now when we run Amend (with FirstName and/or LastName set to null) the exception occurs from the Amend method, as if the Contract.Ensure’s replaced the Validate call.
Based upon the above information it would come as no surprise to find out that when the ContractAbbreviator attribute is used on a method (and ofcourse the method is called from another method), the compiler does indeed place the contract code into the calling method and replaces the instruments within the Validate method (in the above example) with a nop. When the attribute is not included we really are calling another method.
Obviously this means we can reuse the Amend method now in more than one method (or more specifically the contracts contained within the method), so we’ve created a reusable set of contracts. If you remove the ContractAbbreviator attribute then run as previously suggested, the validation failure will occur in the Validate method.
Visual Studio Plugin
At the start of this post we installed a couple of code contract specific plugins (in VS2012 and only one in VS2013). These added the property editor into the project properties for enabling etc. Code Contracts. But they also installed editor warnings.
If you check the “Perform Static Contract Checking” option in the Code Contract property page, then rebuild your project. Static analysis will take place and may display warnings. For example if your code looked like this
public void Analyze(string data)
{
Contract.Requires<ArgumentNullException>(line != null)
}
static void Main(string[] args)
{
Analyze(null);
}
We would get warnings stating CodeContracts: requires is false: line != null. Along with a red squiggly underline of the code Analyze(null) and a tooltip popup showing the warning message.
So giving us an indication early on of possible contract violations.
References