DevLabs: Code Contracts for .NET
In October of last year, I blogged about Dev Labs - a site dedicated to software innovations for the developer community. Today, Dev Labs released a new innovation that our Microsoft Research organization has been working on: Code Contracts for .NET.
Design-by-contract is an idea that was pioneered by Eiffel. Today’s release, Code Contracts for .NET, is a general design-by-contract mechanism that all .NET programmers can now take advantage of. Using it, programmers provide method preconditions and postconditions that enrich existing APIs with information that is not expressible in the type systems of .NET languages. Additionally, contracts specify object invariants, which define what allowable states an instance of a class may be in (i.e. its internal consistency.)
The contracts are used for runtime checking, static verification, and documentation generation. Contracts also allow automatic documentation checking and improved testing. Code Contracts for .NET currently consists of three components: the static library methods used for expressing the contracts, a binary rewriter and a static checker.
The Library Methods
The static method Contract.Requires() is used for preconditions and Contract.Ensures() is used for postconditions. Programmers write calls to these methods as a preamble at the beginning of a method. The Contract.Invariant() method is used to specify object invariants. All object invariants are put into a method marked with the attribute [ContractInvariantMethod].
You can see how these are used in the screenshot below. Notice the use of the method Contract.OldValue() within the postcondition to refer to values as they existed at the beginning of the method. The code is then compiled by the normal .NET compiler, e.g., C#, to produce IL.
The Binary Rewriter
The Intermediate Language (IL) that the C# compiler produces for the above example cannot be executed as is. To provide for the runtime checking of contracts, the binary rewriter takes the compiled IL and transforms it so that contracts are evaluated at the correct program points. For instance, postconditions are evaluated just before each return point within a method. Any expression within a call to OldValue() is evaluated upon entry into the method with the corresponding value replacing the call when the postcondition is evaluated. (There is also the method Result() which is used to refer to the return value of a method. Its use is illustrated below.) If the instrumented code happens to follow an execution path that violates a contract, then there is a programmable notification component that signals an error. You can see an example in the screenshot below, which shows a precondition that failed at runtime: the method Divide was expecting a non-zero argument. (For this example, the notification resulted in an assert dialog, but you can customize it to perform any action you would like.)
The Static Checker
This tool analyzes code to look for contract violations without having to execute the code. The checker issues a warning if it is not able to determine that the code is correct for all possible executions.
In the example in the screenshot below, the checker warns about a possible violated precondition in the invocation of MyMath.GCD.
If the programmer adds the precondition to NormalizedRational that x must be non-negative and y must be positive, then the checker proves that the precondition of MyMath.GCD will be satisfied in all possible executions.
Furthermore, the checker proves that MyMath.GCD always satisfies its postcondition (i.e. the GCD is positive). The checker uses the postcondition of GCD to prove: (1) that at line 45 there will never be a division by zero; and that “y/gcd” is non-zero, so that the precondition of the Rational constructor is always satisfied.
And, of course, you can use Code Contracts directly in Visual Studio. Installing the Code Contracts MSI enables the “Code Contracts” tab in project properties where you can set your preferences for Code Contracts use. For configurations where the runtime checking is not performed, the library methods are compiled away (via conditional compilation attributes on their definitions --- a very neat feature of .NET!) so that your code pays no performance penalty at all for contracts that you do not want executed.
Here is some feedback from a customer who had a chance to look at an early drop of this. “You have a really nice product here. I enjoy the library+rewriter combination which makes it language agnostic. I can't wait to see the tools improve.”
Namaste!
Comments
Anonymous
February 23, 2009
PingBack from http://www.clickandsolve.com/?p=13327Anonymous
February 23, 2009
In my Introduction to Code Contracts post, I mentioned that the tools to enable runtime checking andAnonymous
February 23, 2009
A while back I heard Microsoft was releasing Spec# - something along the lines of CodeContracts. I believe it was a research project. Whatever happened to it? Or was that completely different from CodeContracts?Anonymous
February 23, 2009
This looks a lot like Spec#. Is this indeed a release of Spec#? Or is this in parallel to that project? I am going to announce this item next week on TechRepublic, and I would love to have the correct information. Thanks in advance! J.JaAnonymous
February 23, 2009
Just what we need, another dev labs project that requires a Team System -level VS 2008 license! Sigh.Anonymous
February 23, 2009
@Jeremy: If you go the the site, you'll also find installers for the other (non-Express) SKUs under non-commercial license.Anonymous
February 23, 2009
If you want something that does almost the same thing with very similar syntax, ContractDriven.NET hosted on CodePlex (http://www.codeplex.com/contractdriven) provides a very similar syntax and has the benefit that it's both Open Source and Free (no Team System licence required!) :-) best regards, Chris.Anonymous
February 23, 2009
It's about time we had support for this, thanks.Anonymous
February 24, 2009
The comment has been removedAnonymous
February 24, 2009
I am fairly certain that this is closely related to Spec#... 2 of the folks who are/were on the Spec# project are on the Code Contract project! Still, I would like some positive confirmation of this for when I write my article. Thanks! J.JaAnonymous
February 24, 2009
Total agree with you @Jason P Sage! There are many "holes" in VS that need mending for Microsoft to be worried about fluff add-ons.Anonymous
February 24, 2009
Hi Soma, I am sure your team is busy finalizing .NET 4.0 Beta 1, so could I make a suggestion ... Traditionally, Microsoft forbid developers publicly deploying apps based on early beta versions of .NET (prior to the go-live licenses, which come with the very late betas in the cycle). Following in the footsteps of MEF, ASP.NET MVC and other recent releases from Microsoft, I think it would be great if with .NET 4.0 Beta 1 you would allow public deployment, with the clear proviso that the beta is, well, an early beta and not supported and used at developers' own risk. Obviously developers who are working on software for nuclear power stations, avionics or Wall Street should not be deploying apps based on the betas, but lots of developers are working on smaller, less critical projects, and start learning the new APIs with simple demo apps, and it is not a major problem if they crash from time to time or have other bugs. You will get significantly more interest in Beta 1 among developers if they can start using it for smaller/demo apps straight away. If they have to wait a year for any deployment options, then the response will be much more muted.Anonymous
February 24, 2009
Hi Soma, In a previous blog comment regarding the Office Ribbon UI licensing: http://blogs.msdn.com/somasegar/archive/2008/11/12/net-fx-4.aspx#comments someone posted: "Soma, the ribbon is currently covered by the bizarre 'Office UI Licence' (which was presumably accidentally excreted in the dying spasms of 'old MS'). Can you reassure us that the absurdity of the UI licence isn't going to encumber the use of WPF4?" to which you replied: "We hear your feedback on the license issues. The .NET FX team is keeping that in mind to ensure you don't encounter these issues with WPF4." Could you confirm that the "new" Microsoft has won this battle and the Office UI License definitely won't be needed for .NET 4.0 users?Anonymous
February 24, 2009
The comment has been removedAnonymous
February 24, 2009
There have been some questions about the relationship of Spec# to the current Code Contracts project. The Code Contracts work is definitely a spin-off from the Spec# project. We learned many things in our work on Spec# --- two of the most important being that it is important to fit into existing languages and that providing total soundness is too burdensome. Spec# continues to be an important research vehicle for us. We are hoping that the current project will provide immediate and practical benefits for working programmers. In a nutshell, Spec# was an extension to C# (v2.0) that provided the same design-by-contract features of method pre- and postconditions and object invariants. It also had a non-null type system and provided support for a sound treatment of object invariants. You can find out much more about it at our web site: http://research.microsoft.com/specsharp.Anonymous
February 24, 2009
In case my previous post was too short and you'd like some more details, here's some comments by Wolfram Schulte: Spec#’s research focus is to understand the meaning of object invariants in the presence of inheritance, call backs, aliasing and multi-threading. Spec# uses a source level rewriter to weave the contracts into the code, and it uses verification condition generation and a theorem prover for static verification of Spec# code. But dealing soundly with all the complex issues around maintaining object invariants has a price: verification becomes non-trivial. That’s why Spec# also needs an ownership discipline to know which objects may alias or cannot alias each other. Code Contracts is the result of learning from Spec# what works and what doesn’t. Unlike Spec# Code Contracts are language agnostic, and thus work across all of .NET languages, from VB to C# to F#. The rewriter works on MSIL and thus had no dependency on particular compilers. Its static analysis engine uses abstract interpretation, which is much faster and more predictable than verification; furthermore abstract interpretation infers loop invariants and method contracts, which helps in adoption and ease of use of Code Contracts.Anonymous
February 24, 2009
And because I keep hitting "Submit" instead of thinking a few more minutes, here's another thought... We want to encourage you to repeat any questions/comments on our forum that is dedicated just to the Code Contracts project: http://social.msdn.microsoft.com/Forums/en-US/codecontracts/threads/.Anonymous
February 24, 2009
Just a minor comment, the example on the "The Binary Rewriter" section is not a good use of Design by Contract. It is indeed a validation on runtime. Design by Contract ensures that the software is correct according to the specifications not to perform validations. I know that it is just an example but it could be confusing to someone who is not aware of the main concepts.Anonymous
February 24, 2009
Ahh, DbC, brings back memories. Now the hip thing is TDD. They achieve similar goals, with different strengths and weaknesses. I do appreciate having this additional tool available as an option. (and personally I prefer DbC over TDD)Anonymous
February 24, 2009
This is great. I have been following any related news and stuff for long. But... Why does it require VSTS not just VS Pro ??Anonymous
February 25, 2009
Check the announcement here and the site is here .Anonymous
February 25, 2009
The comment has been removedAnonymous
February 25, 2009
Check the announcement here and the site is here .Anonymous
February 25, 2009
Thank you for submitting this cool story - Trackback from DotNetShoutoutAnonymous
February 25, 2009
Check out Somasegar's weblog to find out this newly added feature for .NET developers.Anonymous
February 25, 2009
Publicación del inglés original : Lunes, 23 de febrero de 2009 14:11 PST por Somasegar En octubre delAnonymous
February 26, 2009
Is there any solution to use Microsoft.Contracts.dll in a VSTS 2008 Silverlight 2 project (converting the assembly into a silverlight compatible one seems to be unsuccessfull) ?Anonymous
February 26, 2009
@Steven I agree. Limiting access to TeamSystem users would dampen the effect it can have. More verifiable code benefits and strengthens the entire platform, so I hope that Microsoft releases this for everyone to use.Anonymous
February 26, 2009
In response to "Castdev" about Silverlight: we will try it out and make sure it works for Silverlight. (Sorry that we didn't do that already.) I would encourage you to start a thread over on the Code Contracts forum: http://social.msdn.microsoft.com/Forums/en-US/codecontracts/threads/ and then we can track this issue.Anonymous
February 26, 2009
So basically this is compile-time range checking? Kinda like assert() isn't it?Anonymous
February 28, 2009
Soma, I couldnt see the Images in this post. I could see that you have added some images in between your post through HTML, but its not visible to the browser. I have tried in couple of machines in IE & FF.Anonymous
February 28, 2009
Hi Kiruthik, It looks like the server that is hosting the images is down. We will try to get it back up soon. Thanks for the note. -somasegarAnonymous
March 01, 2009
Creio que foi Bertrand Meyer, o autor da linguagem Eiffel, quem primeiro falou sobre Design by ContractAnonymous
March 02, 2009
The comment has been removedAnonymous
March 04, 2009
We’ve mentioned Code Contracts over on the BCL Blog a few times now, but never yet on the CLR Blog. Basically,Anonymous
March 12, 2009
Hi, There has been a bunch of feedback about the restriction for this to work only with VSTS. The team is looking into and hopefully we will get a chance to fix this in a subsequent update. -somasegarAnonymous
March 25, 2009
Non-sense. There is nothing pioneering in this. Even the author admit this prior to talking about it. Somaasegar forgot that Microsoft Research does not exist to do "Research" and "Innovate/invent" but to copy (Microsoft has invented innovative techniques like AJAX BUT never an innovative product.) This feature is just Microsoft copying someone else. I am not criticizing because I use Microsoft in my Software Engineer tasks. I just hate it though when people attach innovation to Microsoft and "Microsoft Research".Anonymous
March 25, 2009
Hi Green, I have never been a a part of MSR (Microsoft Research), but from my perspective I see a fair amount of innovative ideas coming out of MSR - we have successfully brought to market some of the ideas from MSR in our products and MSR continues to be a substantial contributor in terms of publishign papers in SIGGRAPH and other leading forums. -somasegarAnonymous
April 27, 2009
@Steven. Hi Steven, I do agree with you. I was just offering an alternative to those who do not want to pay for the compile time checking as part of the Team System licence. ContractDriven.NET does NOT allow you to do compile time checking. However it does allow you to write runtime contracts in to your code to improve your codes readability, maintainability and runtime reliability (and it supports invariant conditions which many of these types of library do not.) ContractDriven.NET can also be used with the standard .NET CLR (so supporting any .net language and even works on works on Linux via Mono). I like your fluent interface for your conditions BTW.Anonymous
June 06, 2009
The comment has been removedAnonymous
July 23, 2009
using your blog this victim of Canadian incompetance found a trial download link, but certain ew2 issues and ew3 upgrade issues have gone to Connect. A million shining stars to Somasagar for keeping our world on top of ... that world.