This article is to show you how to go from a clean install of Visual Studio 2010 to running the Code Contract tools for the first time. Since the tools aren’t included in VS install, we thought we’d provide some extra information on where to find them. If you’re already using Code Contracts in Visual Studio 2010, this blog post probably won’t have anything new for you. If you want an overview of the System.Diagnostics.Contracts.Contract class, please see earlier blog posts or documentation. This post is just about getting set up for the very first time.
This article might also be useful to you if you’ve tried to run a project and gotten an assert stating that “This assembly must be rewritten using the binary rewriter.” That can happen if you’ve used certain methods on the System.Diagnostics.Contracts.Contract class in your code and defined the appropriate symbol to have them compiled into your code, but haven’t run the tools mentioned here.
If you want the really quick version of this post, the answer is to go download the appropriate installer linked to on the right side of this page: http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx. Then use the Code Contracts pane in the Properties of your project to perform runtime contract checking. Without this setting, contracts are not checked – we don’t compile them into your code without this option. If you want a few more details, read on.
The Contract class is included in the Microsoft .NET Framework 4, but the tools that take advantage of them are found on DevLabs (more on that later). There are two primary tools: ccrewrite.exe, a binary rewriter that moves your contracts to the correct place in the code and checks whether the contracts are written correctly, and cccheck.exe, a static analysis tool that will find places where contracts have been violated without running your code. Think of cccheck like FxCop for finding bugs, using the rules you establish via your own contracts. You cannot do runtime checking of your contracts without using ccrewrite.exe. Because of this, most of the methods on the Contract class are conditionally compiled, which means that calls to them won’t be included in your code without a special symbol being defined. The tools provide an easy way to define that symbol in a new tab on the properties pane of your project and run ccrewrite immediately after compiling your assemblies.
Downloading from DevLabs
DevLabs is a Microsoft site for sharing prototypes of tools for developers and getting feedback on them from the community. The Code Contract tools started out as a project in Microsoft Research. We’re working on getting them incorporated into products, but to get them out where our customers can use them in this release, we’re hosting them on DevLabs. In addition to being a place to host the tools, the Code Contracts page also has a forum, FAQ, and documentation for the tools.
There are two different installers for the Code Contracts tools. The one that includes the static checker requires VS 2010 Premium or VS 2010 Ultimate. The version without the static checker will work on any edition of VS 2010 other than the Express Edition, and is what the DevLabs site refers to (for now) as the “Standard Edition” of the tools. Pick which version works for you, and you’ll get the usual prompt asking if you want to run or save the file.
Enabling Contracts in Projects
The installer adds a tab to the properties pane for projects in Visual Studio. It has quite a few options that are described in the aforementioned documentation for the tools. The two most important, though, are the checkboxes to Perform Runtime Contract Checking and (if you have the static checker) to Perform Static Contract Checking. The option to perform runtime checking will define the symbol to put contracts in your code and enable a post-build step to put the checks for those contracts in the correct place (for instance, placing checks for post-conditions at every exit of a method). If those contracts are violated, an assertion or exception will happen, depending on your selections for the other options on the tab. If you enable static contract checking, cccheck.exe will run in the background to try to prove all of the contracts you have written in your code.
I hope this helps you to get started using Code Contracts. If you’re just getting started with the feature, I strongly encourage you to spend some time on the forum or reading the documentation on MSDN.