Introducing Advanced Code Contracts with the Entity Framework and Pex (Cont.)
I wouldn’t be objective if I didn’t highlight one of the major issues with Code Contracts. Multithreading is currently not supported. In fact, using Code Contracts run-time checking with multithreading can be downright dangerous sometimes.
Let’s say that you have a critical section managed with a lock or another synchronization mechanism:public class MultithreadedList<T> : IList<T>
List<T> list = new List<T>();
public void Add(T item)
// Code skipped...
You’ve seen by now that interface contracts are inherited and injected. Listing 11 shows the same method after contract injection by the Contract Rewriter. You can see that the postcondition was added after the lock. If another thread empties the list between the lock and the Ensures statement, the clause will fail. In fact, the postcondition should have been injected inside the lock (or not at all) to prevent contract injection from breaking valid code. Having the Contract Rewriter guess where to add the contract clauses in such a context is almost impossible; imagine a multiple-lock method!
The Code Contracts team will provide a way to manage or workaround multithreading in a future release.
Explore Your Entities with Pex
I couldn’t talk about Code Contracts without saying at least a few words on Pex. Pex stands for Program EXploration. This tool drills down into your assemblies, gathers information, and analyzes it in order to provide you with white-box testing.
While covering Pex is beyond the scope of this article, I’ll show you rapidly how it can generate unit tests based on Code Contracts clauses.
Once you’ve installed Pex and you have opened a project for which you’d like to generate unit tests, all you have to do is to use the context menu in Visual Studio to invoke it, as shown in Figure 7. If you open the context menu inside a property or method, Pex will only explore that specific piece of code; otherwise, it will apply the exploration to the entire project.
Figure 7: Running Pex.
Now, be patient! Exploring an assembly can be a lengthy operation. But it’s worth every second of it. When combined with Code Contracts, Pex detects your contract clauses and generates a bunch of tests to stress them. I was curious to see how Pex would behave with the Code Contracts Conditions and with regular expressions, so I challenged it with the Phone property contract already introduced in Listing 5. After tweaking the test project a little bit, I successfully got Pex to generate a valid phone number and quite a lot of unhappy paths to test the property. Figure 8 shows the Pex Exploration Results from this operation.
Figure 8: Pex exploration results.
Pex won’t create all your unit tests, but it can save you a lot of time!
The test projects included in the companion solution presented in Figure 3 are all Pex-generated. Pex won’t create all your unit tests, but it can save you a lot of time!
Contract-First Development and TDD
Let me come back to one of the principles of Design by Contract: design your contracts first. Ouch! That’s quite a blow for Test Driven Development (TDD), which states that you must design your tests first, isn’t it? Maybe not. Maybe both worlds can agree on a truce and find peace by collaborating.
You’ve seen how running a tool like Pex can really help you by generating many of your unit tests. So there’s definitely a paradigm shift here. However, that doesn’t mean the end of TDD either, because not all unit tests can be generated. Furthermore, you can’t write contracts without an API.
So, why not use TDD and start writing your happy path unit test? Then, when you create a new method or property to satisfy your test, switch to DbC. Define your contracts and generate unit tests for them with Pex. After that, switch back to TDD and complete your implementation. You can even go back and forth between both methodologies while refactoring you API before running Pex.
In this article, I presented an overview of Design by Contract and introduced the Code Contracts Library, the Contract Rewriter, the Static Contract Verifier, and Pex. Along the way, I showed how you can apply these principles and tools to the ADO.NET entities of the Entity Framework. I covered advanced strategies and techniques you can use while implementing your contracts, such as the Code Contracts Conditions, object validation, self validation, lazy initialization, and error handling. I also highlighted some limitations you may encounter.
It’s up to you now to dig deeper into these topics by going to DevLabs and familiarizing yourself with Code Contracts and Pex. You like what you see? You don’t? Let Microsoft know by talking to them in the DevLabs forums.
As for me, I’ve got to find out what Doloto, Spec Explorer, STM.NET, Axum, Small Basic, and CHESS are!