Introduction
This post will be mostly about Microsoft’s Research in Software Engineering (RiSE) group’s Code Contracts. I’ll also cover the role of code contracts in conjunction with test-driven development. There seems to be a debate over the role of test-driven development when using code contracts. I’m going to weigh in on that debate.
In order to demonstrate code contracts, I’m going to return to the Category
class that I used as an example in my blog post Advanced Test-Driven Development. This post may also be a little on the longer side.
An Introduction to Code Contracts
What are code contracts? Where did they come from? Why should I care?
The term ‘code contract’ was coined by Bertrand Meyer while he was developing the Eiffel programming language around 1986. In fact, code contracts are a core part of the Eiffel programming language to this day.
Code contracts are a way of specifying pre-conditions, post-conditions for methods and invariants for objects. Pre-conditions are predicates that specify conditions that must be met in order for a method to be in a state that can result in successful execution. Post-conditions are predicates that must be met upon any exit from a method. Invariants are predicates that validate state that must hold at all throughout the lifetime of an object.
Microsoft & Code Contracts
Microsoft’s RiSE team first introduced code contracts to .NET as an extension to the C# language known as Spec#. Spec# was basically a DSL especially for defining code contracts when programming in C#. Fast forward a few years, and shortly after the release of the .NET Framework 3.5, the RiSE team released the successor to Spec#, Code Contracts, in the form of an assembly that you can reference from your project. This assembly replaced the DSL with a native C# language implementation. For the first time in .NET (aside from the Spec# augmented language), programmers could employ code contracts (and not just simple guard conditions at method entry and rudimentary forms of post-conditions). With the release of the .NET Framework 4.0, Code Contracts have found their way into the base class library (BCL) itself. Code contracts can be found in the System.Diagnostics.Contracts
namespace. You no longer need to reference an external assembly to employ code contracts.
In order to make full use of code contracts in your .NET projects, you will need to install the necessary tooling from Microsoft’s RiSE Code Contracts site. Installing this tooling installs a new project properties tab for controlling how contracts are incorporated into your assemblies, whether contracts will be enforced at runtime, and/or whether or not the static analyzer will perform an analysis of your code. For the full details, check out the Code Contracts documentation. Furthermore, the tooling installs a code contracts re-writer. The re-writer is the component responsible for weaving the necessary IL into your assemblies in order to enforce the contracts according to the options specified. OK, enough of the history lesson. Let’s get to the fun part: the code.
Using Code Contracts with the Category Class
As I stated in the introduction to this post, I’m going to be reusing the Category
class example I went through in my post on advanced TDD. This class represents a category that you might find in some online e-commerce product catalog. I'm going to highlight just a few areas of the Category
class as it pertains to implementing code contracts. The first part of the class we’re going to look at is instantiating the class given a name, since the pre- and post-conditions are pretty easy to follow. Also, because of this easiness, it will be easier to introduce how to incorporate unit testing when using Code Contracts.
So, starting with the a category's name: it cannot be null; it must not be the empty string; and it must not consist solely of whitespace. In my advanced TDD post, we enforced these requirements with the following code:
public class Category { private string name; public Category(string name) { if (string.IsNullOrWhiteSpace(name)) throw new InvalidCategoryNameException(); this.name = SanitizeName(name); } }
The guard clause is known as a pre-condition. This particular form of pre-condition is considered a defensive programming style. If the name
parameter is null, the empty string, or only whitespace, an InvalidCategoryNameException
exception is thrown. Notice that the constructor has no post-conditions—there is no code to ensure that the private class field name
also satisfies these conditions. (In all honesty, it's hard to think of a reason why, if the name
parameter meets the pre-conditions, the corresponding class field would not end up being assigned.) Let's see what this same constructor would look like using Code Contracts.
using System; using System.Diagnostics.CodeContracts; namespace DDDSportsStore.Domain { public class Category { private string name; public Category(string name) { Contract.Requires<InvalidCategoryNameException>( !string.IsNullOrWhiteSpace(name) ); Contract.Ensures(!string.IsNullOrWhiteSpace(this.name)); this.name = SanitizeName(name); } } }
As you can see, the guard clause was replaced with a call to Contract.Requires<T>(bool precondition)
. (Important: read the documentation before using the generic form of the Requires
method in your release code.) This line of code guarantees that if the name
parameter does not meet the specified pre-condition, the specified exception will be thrown. Similarly, we have stated a post-condition: namely that when this constructor exits, the class's name
field will also not be null, an empty string, or whitespace. In my advanced TDD post, the constructor ended up having a lot more guard clauses in it for other properties of the Category
class. Don't worry, we'll come to those soon.
Code Contract Violations
When a pre-condition, post-condition, or invariant condition is violated, an exception is thrown. The exception is the System.Diagnostics.Contracts.ContractException
. The catch is, this exception’s access modifier is internal
; so you can’t catch this exception directly. This is actually a very good design decision on the part of the RiSE team, even thought it causes headaches for us developers—especially when it comes to unit testing. Programmers should not be able to circumvent contract violations by catching these exceptions and “handling” them. Contracts are guarantees. Pre-conditions guarantee that, given parameters that satisfy the stated pre-conditions, the method can perform its duties. Similarly, post-conditions guarantee to the caller that upon exit from the method, certain conditions will be true. And invariants guarantee that certain conditions hold throughout the lifetime of the object before and after each method call. So while this is a bit of a pain when it comes to unit testing, this was a very good decision.
Code Contracts and Test-Driven Development
As I alluded to in the introduction to this post, there is a debate that’s been going on in Internet land regarding the roles of code contracts and test-driven development and when and how they are used together. I’ve seen many people giving bad advice in regards to these development practices and I wish to argue the case for my opinion in the next few paragraphs.
What, traditionally, has been the purpose of unit tests (especially those unit tests written as part of a test-driven development effort)? Traditionally, they’re written to ensure that a method does what it’s supposed to do. In fact, there’s a whole style of test-driven development known as behavior driven development (BDD). BDD’s main focus is tests that are named after the behavior that the function is performing. BDD tests strive to be as human readable as possible in an effort to be somewhat of a requirements document for the code base. (I’m over simplifying a bit—I urge you to become familiar with it, as the style has many merits over regular TDD.) But no matter the testing style you use, tests are written to verify that: 1) method parameters are checked to ensure successful execution of a method; 2) the method executes successfully and the proper outputs are returned; and 3) that the state of the object is valid when the method has finished executing (not all tests require this last point to be checked). The first point sounds a lot like pre-conditions—and in a sense, that’s exactly what’s being checked. The second point sounds exactly like post-conditions—and it is. The third point, if part of the test, might be an object invariant (I say might, because what’s being tested in the third point may only be true for that particular case and not a true invariant.)
So now the question is, if I use code contracts, do I need to test pre-conditions and post-conditions? Emphatically, I say YES!! You will find many who disagree with me. Let’s examine the two main arguments against writing tests that exercise code contracts.
You Don’t Write Unit Tests that Exercise Debug Asserts—Why Write Tests That Exercise Your Contracts?
First, I would like to say that this is an invalid statement to begin with. Of course you don’t exercise debug asserts. There’s nothing you can do with them in the testing framework. Your test will fail if a debug assert fails because the program aborts (and therefore, your test runner aborts, too)! So that’s just a ridiculous comparison to make. Furthermore, pre-conditions are not debug asserts. I think this argument comes about because there is a Contract.Assert
method in Code Contracts. But this method is not used as a pre- or post-condition. The Contract.Assert
method is used as a hint to the static analyzer that, at some point in your code, some condition should hold. That’s it. It’s just a hint to the static analyzer—not a contract. These hints are sometimes needed in order to give the static analyzer a little bit of help when it can’t quite figure out what should hold or not.
Testing Code Contracts Pre-Conditions is Akin to Testing the BCL
This argument is almost plausible; but ultimately, it is flawed. First, it is true that Code Contracts are now a part of the .NET base class library. That’s what makes this argument so plausible. However, when you write tests to test your pre-conditions, the goal is not to test that Code Contracts “does the right thing” when a contract is violated. Indeed, that would be silly. It’s 3rd party code that I have no control over, so why test it? No, what I am testing is that I didn’t accidentally mistype the condition that is checked as part of the pre-condition contract!
Seriously, you must write unit tests for your pre-conditions. While adding code contracts to the Category
class used in this blog post, I did mistype a pre-condition specification. The specification was supposed to ensure that when adding a subcategory to a category, the category being added as a subcategory is not null and was not the NullCategory
. So when I ran my unit tests and two of them failed (again, I had added the contracts after I had already written the majority of the class in this instance using the standard defensive coding practice of guard clauses at method entry), I was surprised. What happened is that I had accidentally used an ||
instead of an &&
in the pre-condition (I probably had copied the guard clause condition; pre-conditions are often the opposite of traditional guard clauses—guard clauses check that something isn’t true, pre-conditions check that something is true). So again I say, YES, you must test your pre-conditions to ensure, not that Code Contracts is behaving, but that you didn’t mistype your pre-condition!
I do find, however, that it’s not practical to test your post-conditions, even though the same possibility of mistyping the post-condition exists. This is because 1) it’s really hard to make your method fail a post-condition on purpose, and 2) chances are, if your post-condition is wrong, a ContractException
exception will be thrown. Again, this argument is not water tight—but it is difficult to test post-conditions, and therefore I believe, not worth the effort.
I think that these two arguments are the most frequent reasons given for not testing your code contracts; and I think I have demonstrated why these arguments don’t hold water.
Test-Driven Development with Code Contracts
Now that we have that out of the way, I want to share with you how you can perform test-driven development while using code contracts. This did take me quite a bit of time to figure out. So let’s re-introduce unit tests for the constructor as it's currently implemented above.
The first thing we need to take care of is the fact that when a contract is violated, a private ContractException
exception is thrown, and since it’s private, it cannot be caught. So how can we test our pre-conditions? Code contracts provides an event on the static Contract
class called ContractFailed
. You can subscribe to this event to get access to the contract exception that was thrown. You can also flag the exception as handled from within this event. (So apparently, even thought you can’t catch the exception, you can subscribe to this event and effectively handle it there. Why any good developer would do this is beyond me, after all, why use code contracts in the first place, then? But for unit testing, this is just the hook we need for testing our contracts—but this is the only place where you should ever write this code.)
Now if you remember back to our constructor example, I was using the generic form of the Contract.Requires
method that allowed me to specify the exception that is thrown. How this works is, upon a contract violation, code contracts will still throw the System.Diagnostics.Contracts.ContractException
exception. But there is a class that is emitted as part of the code contracts re-writer that is able to catch this exception. When the exception is caught, the exception’s InnerException
property contains an instance of the exception specified for the generic type parameter. This inner exception is then thrown back to the application. (Read the documentation before using the generic version of Contract.Requires
.)
Shown below, I have written a class that subscribes to the Contract.ContractFailed
event, which is meant to serve as a base class for all test classes that will be testing objects written with code contracts.
using System; using System.Diagnostics.Contracts; using Microsoft.VisualStudio.TestTools.UnitTesting; namespace DDDSportsStore.Domain.Tests { // Probably not the best named class for this purpose... // but good enough. [TestClass] public abstract class UnitTestBase { private EventHandler<ContractFailedEventArgs> ContractFailedHandler = new EventHandler<ContractFailedEventArgs>((s, e) => e.SetHandled()); [TestInitialize] public void HookContractFailed() { Contract.ContractFailed += ContractFailedHandler; } [TestCleanup] public void UnhookContractFailed() { Contract.ContractFailed -= ContractFailedHandler; } } }
This class has both a setup and a teardown method. It hooks and unhooks an event handler to handle the Contract.ContractFailed
event. In the official documentation, the RiSE team show that you should call e.SetUnwind()
. If you call that method, your unit tests will stop running the moment a contract is violated. That’s because that method causes another exception to be thrown. Any exception thrown from the ContractFailed
event handler winds up causing the application to terminate—which means no other tests will run because the test runner will be terminated. But in this case, we want the exception to be thrown because it verifies that when we pass invalid parameters to the method under test, that the pre-condition contract was specified correctly, and therefore, the correct exception is thrown. So now you can use your test framework’s method for asserting thrown exceptions and the tests will pass. Let’s look at an example test that tests our Category
constructor by passing a null
name, an empty string name, and a name consisting entirely of whitespace.
[TestClass] public CategoryTests : UnitTestBase { private void AssertCannotCreateCategoryWithName(string name) { ExceptionAssert.Throws<InvalidCategoryNameException>( () => new Category(name) ); } [TestMethod] When_creating_a_category_with_an_invalid_name_then_an_InvalidCategoryNameException_is_thrown() { AssertCannotCreateCategoryWithName(null); AssertCannotCreateCategoryWithName(string.Empty); AssertCannotCreateCategoryWithName("\n"); } }
If you look back to my previous post, you will see my implementation of the ExceptionAssert
class that I created to handle testing for thrown exceptions. I prefer using this utility class to using the ExpectedExceptionAttribute
attribute. Pretty much, that's all there is to incorporating unit tests with code that uses code contracts and maintaining the ability to test that you typed your pre-conditions correctly. If you don't want to use the generic form of the Contract.Requires
method (and there may be good reasons for you to do so, see the code contracts documentation for details), then you may need to modify how you test your pre-conditions. But the basic elements remain the same. I'll leave that as an exercise for you.
For the remainder of this blog post, I'm going to skip showing unit tests. As, apart from what I showed above, there's nothing different about my unit tests than what I demonstrated in my previous blog post. For the rest of this post, I want to focus on Code Contracts and incorporating more of its features into your classes.
Code Contracts and Inheritance
The great thing about Code Contracts is that you don’t need to redefine them on all of your sub-types. Once you define them on a base class, they’re defined for all sub-types. In this way, using Code Contracts can help ensure that your code follows the Liskov Substitution Principle (LSP). Because code contracts are inherited, all derived types can be used in place of their base types and clients are guaranteed that all pre-conditions, post-conditions, and invariants of the base type will still hold on all derived types.
This does have some implications for derived types however. Derived types are not allowed to define pre-conditions that are stronger than their base types (in fact, doing so would most likely be a direct violation of the LSP to begin with). It is interesting to note, that while weaker pre-conditions should be allowed, they are not. The RiSE team, in their work with Spec#, found that allowing weaker pre-conditions often provided little value but added a large amount of complexity to the analyzer. So in effect, you cannot even add any pre-conditions to derived types. This is even true for interfaces (after all, interfaces are nothing more than pure, abstract classes for which C# has simply provided syntactic sugar (and built-in compiler constraints) in the form of the interface
keyword). It should also be noted that if you don’t specify any pre-condition on a method in a base class, then that method is considered to have the weakest of all pre-conditions: true
.
These same rules, however, do not apply to post-conditions. You are allowed to specify stronger post-conditions on derived types. This just provides further guarantees for clients that call those methods on derived types compared to their base class method counterparts.
Code Contracts and Abstract Class Methods and Interfaces
Naturally, the question should arise: how can I implement contracts on abstract class methods and interfaces, neither of which are permitted to have method bodies? The answer is to create a special class that overrides the abstract class methods or implements the interface. Code Contracts provides two attributes, one that adorns the abstract class or interface (ContractClassAttribute
), and the other that adorns the contract class itself (ContractClassForAttribute
).
Keeping Your Contracts DRY
If you find yourself repeating many contracts over and over again in various methods throughout your objects, you can group them together into methods adorned with the ContractAbbreviatorAttribute
attribute and call them directly from methods that require the contracts. Let me show you an example. For any Category
that is created, it must have a non-null list of subcategories. It’s parent category must also not be null (if a category has no parent, it should have the NullCategory
Category.None
assigned as its property value). And of course, a category should not have a null, empty string, or whitespace only name after it’s been instantiated. Here’s how I can “group” my contracts together:
public class Category { public static readonly Category None = new NullCategory(); private string name; private Category parentCategory; private List<Category> subCategories; protected Category() { subCategories = new List<Category>(); } public Category(string name) : this(name, None) { } public Category(string name, Category parent) : this() { Contract.Requires<InvalidCategoryNameException>( !string.IsNullOrWhiteSpace(name) ); Contract.Requires(parent != null); EnsureThisCategoryIsValid(); this.name = SanitizeName(name); if (parentCategory == null) parentCategory = parent; else SetParentCategory(parent); } [ContractAbbreviator] private void EnsureThisCategoryIsValid() { // Obviously, separate calls to Ensures or Requires are ANDed together... Contract.Ensures(subCategories != null); Contract.Ensures( this == None || !(string.IsNullOrWhiteSpace(name) || parentCategory == null) ); } }
Again, while this example is trivial, if you have a lot of methods with the same pre- and/or post-conditions, this can be a valuable tool in keeping your code contracts code DRY.
Specifying Object Invariants
Code contracts has a way of telling the analyzer the various invariants of your objects. Invariants are conditions that must be met by your object after each public method call. In the Category
class, for example, the following invariants are true: a category’s name is not null, a category’s parent is not null, and a category’s list of subcategories is not null. These conditions can be checked by placing them within calls to Contract.Invariant
inside of a method adorned with the ContractInvariantMethodAttribute
attribute as shown below:
[ContractInvariantMethod] public void CategoryInvariants() { Contract.Invariant(Name != null); Contract.Invariant(Parent != null); Contract.Invariant(Subcategories != null); }
Invariants can be especially useful with automatic properties (properties that don't have explicit backing fields that are retrieved/assigned from the property's getters/setters).
Code Contract Helper Methods
Let's say you have some helper method to help you in determining whether certain conditions hold (either for pre- or post-conditions on a method) due to some complex logic. You don't really want all that complex logic in the Contract.Requires
or Contract.Ensures
method call. So instead, you'll have something like Contract.Ensures(ThisMethodsResultsAreVaild());
. In order to use this method without code contracts emitting an error at compile time, you should mark the method as pure using the PureAttribute
attribute. This tells code contracts that this method has no visible side-effects and will remove the compiler error. The effects of the PureAttribute
attribute are also inherited by derived classes.
Giving the Analyzer a Helping Hand
Determining the various states that the source code could leave the object in at any particular time is a fairly difficult task. You’ll see this is true when you start to use Code Contracts because it will slow down your build times a bit (static analysis runs as a post-build activity). For this reason, Microsoft does suggest that you only run contract checking for a custom build configuration that you would create in addition to your normal Debug and Release builds (e.g., Checked).
Due to the complexity involved in analyzing the source code, sometimes the static analyzer will ask for your help. It does this by writing informational messages to the Error Output window in Visual Studio. Sometimes it tells you exactly what it’s looking for in the form of suggesting appropriate Contract.Requires
or Contract.Ensures
statements. Other times, it tells you that it’s assuming one thing or another (and suggests that you specify these assumptions for next time).
Code Contracts has two other static methods on the Contract class called Assume
and Assert
. These are not pre- or post-conditions or even object invariants. In the case of Assume
, you’re informing the static analyzer that it should assume the condition specified for the argument to the method is true at that point in the execution of the code. It is merely a hint to the analyzer. On the other hand, Assert
tells the static analyzer that some condition must be true at that point in code execution in order for successful execution to continue. If at runtime (for builds where asserts are left in the code, such as your Checked build confiuration) an assertion is violated, your program will terminate.
Conclusion
I've touched upon many of the features of Microsoft's RiSE Code Contracts in this blog post along with a few code illustrations. If you find Code Contracts interesting and an acceptable way of practicing Design by Contract, I encourage you to check out the Code Contracts website and the corresponding documentation. Below, find the complete Category
class re-written to include all Code Contracts. Except for having to hook the ContractFailed
event in a base class for all my unit tests in order to test that expected exceptions where thrown, the unit tests did not need to change in any other way, and so I have not repeated them here. Until next time, take care.
using System; using System.Collections.Generic; using System.Diagnostics; using System.Diagnostics.Contracts; using System.Text.RegularExpressions; namespace DDDSportsStore.Domain { [DebuggerDisplay("[Name: {Name}]")] public partial class Category { public static readonly Category None = new NullCategory(); private string name; private Category parentCategory; private ListsubCategories; protected Category() { subCategories = new List (); } public Category(string name) : this(name, None) { } private Category(string name, Category parent) : this() { Contract.Requires<InvalidCategoryNameException>( !string.IsNullOrWhiteSpace(name) ); RequiresCategoryIsNotNull(parent); EnsureThisCategoryIsValid(); this.name = SanitizeName(name); if (parentCategory == null) parentCategory = parent; else SetParentCategory(parent); } protected virtual int Id { get; set; } public virtual string Name { get { return name; } set { RequiresValidName(value); name = SanitizeName(value); } } public virtual Category Parent { get { return parentCategory; } set { RequiresCategoryIsNotNull(value); Contract.Assume(parentCategory != null); SetParentCategory(value); } } public IReadOnlyCollection Subcategories { get { Contract.Ensures( Contract.ForAll( Contract.Result<IReadOnlyCollection<Category>>(), c => c != null && c != Category.None ) ); Contract.Assume(subCategories != null); return subCategories; } } /// <summary> /// Creates a new <see cref="Category"/> as a subcategory of the /// current instance. /// </summary> /// <param name="name">The name of the new category.</param> /// <exception cref="InvalidOperationException"> /// Thrown if the current instance is <see cref="Category.None"/> /// </exception> /// <exception cref="InvalidCategoryNameException"> /// Thrown if the <paramref name="name"/> is <c>null</c>, /// the empty string, or consists entirely of whitespace. /// </exception> public virtual Category AddSubcategory(string name) { RequiresValidName(name); Category subCategory = new Category(name, this); AddSubcategory(subCategory); return subCategory; } private void AddSubcategory(Category c) { Contract.Requires<InvalidOperationException>( this != Category.None && !(c == None || c == null) ); Contract.Requires<InvalidOperationException>( !( Contract.Exists<Category>( subCategories, sc => sc.Name == c.Name ) ) ); this.subCategories.Add(c); } public bool Equals(Category other) { if ((object)other == null) return false; return this.ToString() == other.ToString(); } private string SanitizeName(string proposedName) { Contract.Assume(!string.IsNullOrWhiteSpace(proposedName)); return Regex.Replace(proposedName, @"\s+", " "); } private void SetParentCategory(Category c) { RequiresCategoryIsNotNull(c); RequiresCategoryIsNotNull(parentCategory); Contract.Requires<InvalidOperationException>( c == Category.None || !this.HasDescendant(c), "Attempted to set the parent of this category to " + "one of this category's descendants." ); parentCategory = c; if (parentCategory != None) parentCategory.AddSubcategory(this); } #region System.Object Overrides public override bool Equals(object obj) { if (obj == null) return false; Category c = obj as Category; if ((object)c == null) return false; return this.ToString() == c.ToString(); } public override int GetHashCode() { return this.ToString().GetHashCode(); } public override string ToString() { return Parent == Category.None ? Name : string.Concat(Parent.ToString(), "/", Name); } #endregion #region Operator Overrides public static bool operator ==(Category a, Category b) { if (object.ReferenceEquals(a, b)) return true; if ((object)a == null || (object)b == null) return false; return a.ToString() == b.ToString(); } public static bool operator !=(Category a, Category b) { return !(a == b); } #endregion #region Code Contracts Helper Methods [ContractInvariantMethod] private void CategoryInvariants() { Contract.Invariant(Name != null); Contract.Invariant(Parent != null); Contract.Invariant(Subcategories != null); } [Pure] private bool HasDescendant(Category c) { RequiresCategoryIsNotNull(c); bool result = false; if (this == c) result = true; else if (c.Parent != None) result = this.HasDescendant(c.Parent); return result; } [ContractAbbreviator] private void EnsureThisCategoryIsValid() { Contract.Ensures(subCategories != null); Contract.Ensures(this == None || !(string.IsNullOrWhiteSpace(name) || parentCategory == null)); } [ContractAbbreviator] private void RequiresValidName(string name) { Contract.Requires<InvalidCategoryNameException>( this == None || !string.IsNullOrWhiteSpace(name) ); } [ContractAbbreviator] private void RequiresCategoryIsNotNull(Category c) { Contract.Requires(c != null); } #endregion } }