Base types, Collections, Diagnostics, IO, RegEx…
This blog post is to provide a bit more detail about the Code Contracts feature that was recently announced at the PDC and in Justin’s blog entry, and that can be found in the Visual Studio 2010 and .NET Framework 4.0 CTP. I’ll include some information on what can be found in the CTP, some of the history and design decisions we made while developing the feature, and some places to get more information. Both of the announcements mentioned above give details about why we added this feature, but I’ll summarize here. The main point of contracts is to reduce bugs by helping you not write them in the first place, or at least catch them sooner. Contracts let you express statements about the behavior of your code in a way that is accessible to tools for runtime and static analysis.
One thing you should note is that the tools to enable runtime checking and static analysis are not in the CTP. However, you can still write your contracts now and then use the tools when they become available. This works because the contracts are conditionally defined. They’ll only appear in your code when you have the CONTRACTS_FULL symbol defined. Until the tools are available and runtime checking is enabled, do not define this symbol. Full contract checking will not work without the tools. However, you also have the option of getting only preconditions with the CONTRACTS_PRECONDITIONS symbol. Preconditions happen to be in the correct place in the code, so your program will still run with this symbol defined. But the runtime checking tool provides many additional benefits, such as contract inheritance, so checking is still not recommended without the tools.
The CTP includes a CodeContracts class in the System.Diagnostics.Contracts namespace that allows you to write contracts in your code. All contracts are static methods that return void. They take a Boolean expression which encodes the condition that must be true. They also have an overload that takes a string parameter as a message for when the contract is false. Contracts are declarative and come at the beginning of your method. You can think of them as part of the signature. Here’s a rundown of what contracts are in the CTP:
Please note that this is only what is in the CTP. This is a feature still under development, and things could change before we ship. In fact, we’re considering a couple of changes. One is changing the class name from CodeContract to Contract to make contracts more readable. Another is adding more sophisticated runtime failure behavior that is customizable by applications and hosts.
The idea for this feature originated with the Spec# project in Microsoft Research. Spec# has its own programming language, an extension of C#, which includes contracts in the syntax of the language. We’re working closely with a team from Microsoft Research to bring contracts to the BCL. One of the main questions we’ve had about the way we are including contracts in the .NET Framework is why we chose to implement them as library calls instead of making them part of “the language.”
There are quite a few reasons for this, but one of them is that the CLR is the Common Language Runtime, and we wanted a feature that all of the languages using the .NET Framework could use, not just one of them. The best way to do this was with library calls. As far as compilers need to be concerned, these are just static method calls. Spec# was great because it had contracts integrated into the language, but that only solved the problem for one language.
People have brought up attributes as another way we could have accomplished this. One argument for that approach is that contracts are declarative, and this would make them look more like part of the method signature instead of the method body. The problem with this approach is that attributes are very limited in what they can express. It would be difficult or impossible to use attributes for all of the contracts you can write in code.
If you’re concerned about it because of the aesthetics, you might want to check out Scott Guthrie’s demo of VS2010, which starts about 88 minutes into this PDC2008 Keynote.
There are a few places you can go if you’re looking for more information.
Contracts are really nice.
In order to be able to use them properly though, we will need pre and postconditions from all the classes we use in our program, for exemple, List<T>.Count is always positive or zero.
Are you going to update the whole BCL with code contracts for .NET 4.0? This sounds like a huge work, but without that, contracts won't be usable at their full potential.
My second question is why C# wouldn't have a syntax that would get translated into CodeContracts upon compilation.
With this we get a good langage support in C#, as well as the ability to have it supported accross all CLR langages.
In my Introduction to Code Contracts post, I mentioned that the tools to enable runtime checking and
We’ve mentioned Code Contracts over on the BCL Blog a few times now, but never yet on the CLR Blog. Basically,
Dzień: 14 marca 2009. Miejsce: Wydział Biologii UW. Wydarzenie: druga edycja konferencji Communities
Relacja z C2C (Communities to Communities) 2009