PDC 2009 Day 1: Code Contracts and Pex: Power Charge Your Assertions and Unit Tests
Code Contracts are a mechanism coming out of incubation at Microsoft Research for expressing design intent when implementing an API. The idea is to specify assertions that are verified at runtime to ensure that callers provide proper information to your methods. There are ways to specify contractual information on methods – Contract.Requires and Contract.Ensures, and there are also interface contracts (for any implementation of the interface) and object invariants. Finally, there are automatic tools that perform runtime checking and static checking and even generate documentation from contracts! (It’s embedded in the XML documentation and Sandcastle can be used to generate from it the actual MSDN-style documentation with a new Code Contracts stylesheet.)
Pex is a tool that enables a new way to write unit tests – it generates an automatic suite of white-box tests from contracts, as well as automatic stubs and mocks.
Code Contracts is currently an external download but then you get an additional page in the project properties. Upon every build you can configure the static checker to look at your code and perform contract validation. Even if there is no use of contracts explicitly in your code, the tool will warn you and tell you that you should add contract calls!
There is also Pex integration in Visual Studio – you can right-click any method and choose to run Pex on it. It will test the code in a white-box fashion trying to provide all kinds of inputs that will fail the tests. You can even inspect the test case – Pex can give you a preview or create an entire test project out of the automatic tests. The generated tests are stored in a partial class, so you can extend it with your manual unit tests in a separate file but under the same test class.
Pex can even generate, from the failed test, the necessary pre-conditions to your method, with a click of a button. There are great advantages to writing pre- and post-conditions explicitly instead of writing checks manually – e.g., you can get automatic documentation, a static compliance checker, and all other advantages.
This is enabled by IL rewriting of your code – the runtime tools with do the checks at runtime and the IDE tools are going to do the checks after compilation. The rewriting, performed by an external tool called ccrewrite.exe, ensures that there is a unified exit point from the method and post-conditions are checked.
Object invariants are a more powerful mechanism that ensures a condition holds as long as an object exists, regardless of the actual methods that execute. Obviously this is much more convenient than to perform the same checks time and again in every method, start and end. (Object invariants are relevant for public method entry and exit only.)
Interface contracts are a little more clumsy, but they provide a means to ensure that all calls to any implementation of the interface undergo the same verifications. Abstract classes can enjoy the same mechanism.
Pex performs parameterized unit tests – it generates a stub for each test and it can be extended with additional assertions. It automatically checks for contract violations, of course. Pex analyzes code and determines the values that trigger code paths in a given method using a constraint solver (visiting each branch in the method – and providing perfect code coverage with the generated tests). For example, when Pex encounters a loop it will generate test cases for 0, 1, and 2 iterations.
There are also the obvious scenarios when you need to test code that relies on external interfaces. Instead of implementing them manually, Pex generates mocks automatically and you can extend them as necessary by assigning lambdas to delegate properties of the generated mock. (The implementation simply calls the delegate property.)
There’s a framework called Moles that ships with Pex that can be used to replace any method and property in .NET – if we want to redefine what DateTime.Now means, we can say:
//here MDateTime is the class generated by Moles
MDateTime.NowGet = () => new DateTime(17,11,2009);
This gives you full interception of whatever property, method, static or instance, you are capable of laying your hands on. (There’s an XML file that tells Moles which classes you want to “mock” this way.) This is essentially an implementation of Detours (which we saw in another MSR presentation earlier today) for managed code…
What does Moles mean for the future of tools like Typemock Isolator?
All in all, both Code Contracts (which is the more mature part of the technology) and Pex are welcome additions to the world of unit testing. I will risk saying that I like these ideas of contract-first development better than TDD ;-)