Today we’re going to keep looking at Code Contracts. Until now, I’ve been concentrating essentially in presenting its use and mentioning how great it is to have static analysis (ie, have something that goes through your code at compile time and detects several places which might breaking existing contracts). Today it’s time to take a look at the advantages associated with its use at runtime.
You’ll get runtime “support” (lets call it this, ok?) whenever you define the CONTRACTS_FULL constant on your code. The easiest way to achieve this is to go to your VS project property window and check the Perform Runtime Contract Checking checkbox (that is near the top of the window). When you do that, you’ll get some interesting things going on on your build. For starters, your assembly will be rewritten. In practice, this means that:
- postconditions are moved to the end of the method;
- method return values are replaced by CodeContracts.Result occurences (more on this on the next paragraphs);
- pre-state values are replaced with CodeContacts.OldValue occurrences;
- contracts are enforced in inheritance scenarios (hurray!).
All this work is done automatically by the ccrewrite tool. If you just go ahead and build a project with Code Contracts runtime support enabled, you’ll see that you’ll get assertions at runtime when one of your contracts is not respected. If you want, you can change that behavior. For instance, lets say that I wanted to get an exception instead of getting the Debug.Assert followed by the Environment.FailFast method calls that are used by default…
Since I’m lazy, I’ll just create a new Exception derived class. If this was production code, I’d probably be creating an exception type for each kind of contract verification (ie, one for preconditions, another for postconditions, etc). Since this is just demo, I’ll probably be able to get away with only one class (ok, I’m really being lazy here! DO check the guidelines before writing your exceptions):
public class DbCException: Exception {
public DbCException(String message)
:base(message)
{}
}
What we need now is a way to throw these exceptions whenever a contract is broken. According to the docs, we need to add a class which has several static methods (one for each “type” of contract):
namespace Test {
public class CustomRewriter {
public static void Requires(Boolean condition, String message)
{
if (!condition) throw new DbCException(message);
}
public static void Ensures(Boolean condition, String message) {
if (!condition) throw new DbCException(message);
}
public static void Assert(Boolean condition, String message) {
if (!condition) throw new DbCException(message);
}
public static void Assume(Boolean condition, String message) {
if (!condition) throw new DbCException(message);
}
public static void Invariant(Boolean condition, String message) {
if (!condition) throw new DbCException(message);
}
}
}
And that’s it. Now, you only need to pass the necessary information for the ccrewrite tool to use these classes instead of the default ones. If you’re using VS, just go to the project’s property window and write the name of the assembly that has the previous classes and the complete name of the class that has the static methods.
Suppose that the CustomRewriter class was on an assembly called anotherassembly. In that case, you should put anotherassembly.dll on the Assembly textbox and Test.CustomRewriter on the Class textbox (do notice that I had to add the dll extension for it to work – not sure if this will remain like this on future versions). Oh, and I almost was forgetting to mention that you need to put that custom assembly on the same folder as the assembly that is being rewritten.
Before ending the post, there’s still time for a quick analysis of the rewriting process. To show you what happens, lets reuse the example presented in the post about quantifiers. Lets focus on the OnPeople method. Originally, it looked like this:
public PersonSearcher OnPeople(Person[] people) {
CodeContract.Requires(CodeContract.ForAll(0, people.Length, pos => people[pos] != null));
CodeContract.Ensures(_people != null);
_people = people;
return this;
}
After the ccrewrite tool ends its work, it will look like this:
public PersonSearcher OnPeople(Person[] people)
{
__copy+<>c__DisplayClass1 CS$<>8__locals2 = new __copy+<>c__DisplayClass1();
CS$<>8__locals2.people = people;
CustomRewriter.Requires(CodeContract.ForAll(0, CS$<>8__locals2.people.Length, new Predicate<int>(CS$<>8__locals2.<OnPeople>b__0)), "CodeContract.ForAll(0, people.Length, pos => people[pos] != null)");
this._people = people;
PersonSearcher CS$1$0000 = this;
PersonSearcher Contract.Result<PersonSearcher>() = CS$1$0000;
CustomRewriter.Ensures(this._people != null, "_people != null");
return Contract.Result<PersonSearcher>();
}
If you go back to the previous list on what happens when rewriting happens, things should start to make sense (please don’t concentrate on the lambdas rewritings done by the compiler; they’re not important in this scenario).
CodeContract.Requires is replaced by a call to the “custom” static CustomRewriter.Requires method. Another thing you’ll notice is that the return value is replaced by a Contract.Result local variable (in order to ensure that the postcondition is correctly run, the rewriting process will introduce a field called Contract.Result so that that you can use it in your postconditions – this wasn’t needed in the previous example though). Finally, the Ensures postcondition verification is moved from the top to the bottom of the method. I’ll leave it to you the verification associated with the use of the OldValues method call.
And that’s all for today. We’re getting near the end of this series on Code Contracts. There are still a couple of things I’d like to mention, so stay tuned if you want to read my ramblings on it.