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.” 




Comments (41)

  1. In my Introduction to Code Contracts post, I mentioned that the tools to enable runtime checking and

  2. Kris says:

    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?

  3. Justin James says:

    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!


  4. Jeremy Gray says:

    Just what we need, another dev labs project that requires a Team System -level VS 2008 license! Sigh.

  5. @Jeremy:  If you go the the site, you’ll also find installers for the other (non-Express) SKUs under non-commercial license.

  6. Chris Varley says:

    If you want something that does almost the same thing with very similar syntax, ContractDriven.NET hosted on CodePlex ( provides a very similar syntax and has the benefit that it’s both Open Source and Free (no Team System licence required!) 🙂

    best regards,


  7. bw says:

    It’s about time we had support for this, thanks.

  8. Jason P Sage says:

    This is range checking, this is more work. I think this is silly and a waste of money and developer time.

    Developers should already be testing input/output parameter validity and have integrated methods from returning error conditions.

    This locks your code in ways that slow productivity. How? Let’s change the code to handle a larger numeric datatype… int32 to int64. Edit the range check – an additional line of code. Test. Yay! Wait… Now I need to go into this tool and tell it of my changes.

    Sorry folks – I like one stop shopping and this is hardly that.

    –Jason P Sage

  9. Justin James says:

    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.



  10. Mark Gordon says:

    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.

  11. .NET 4.0 Dev says:

    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.

  12. .NET 4.0 Dev says:

    Hi Soma,

    In a previous blog comment regarding the Office Ribbon UI licensing:

    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?

  13. For those wondering what the relationship between this CodeContracts library and Spec# is, yes, Microsoft changed Spec# from a language into a library that can be used from any language: CodeContracts.

    This library works in co-ordination with Microsoft’s Pex, the white-box static analysis tool that can generate unit tests for you.

    The guy working on Spec# is now working on this CodeContracts. He gave a talk on this at the last PDC.

  14. Mike Barnett says:

    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:

  15. Mike Barnett says:

    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.

  16. Mike Barnett says:

    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:

  17. Beren Camlost says:

    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.

  18. fschwiet says:

    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)

  19. Mohamed says:

    This is great. I have been following any related news and stuff for long.

    But… Why does it require VSTS not just VS Pro ??

  20. LA.NET [EN] says:

    Check the announcement here and the site is here .

  21. Steven says:

    @Chris Varley. I’m sorry, but you can’t compare ContractDriven.NET with .NET Code Contracts. I know what I’m talking about, because I’ve build a ‘contract’ framework like you did ( However, Code Contracts is about COMPILE TIME verification. That is something we both can not offer in our frameworks. For this reason Code Contracts is the bomb :-).

    I truly hope Code Contracts will not only be included in the team editions of Visual Studio 2010, but also in the professional edition of VS 2010. While I can understand Microsoft trying to get their investments back; releasing Code Contracts to the masses would have serious impact on the quality of the software .NET developers will write. This would reposition .NET as a whole!

  22. ASPInsiders says:

    Check the announcement here and the site is here .

  23. Thank you for submitting this cool story – Trackback from DotNetShoutout

  24. Dr. Z's Blog says:

    Check out Somasegar’s weblog to find out this newly added feature for .NET developers.

  25. Publicación del inglés original : Lunes, 23 de febrero de 2009 14:11 PST por Somasegar En octubre del

  26. Castdev says:

    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) ?

  27. @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.

  28. Mike Barnett says:

    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: and then we can track this issue.

  29. Cardin says:

    So basically this is compile-time range checking? Kinda like assert() isn’t it?

  30. Kiruthik says:


    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.

  31. Somasegar says:

    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.


  32. Creio que foi Bertrand Meyer, o autor da linguagem Eiffel, quem primeiro falou sobre Design by Contract

  33. Mark Gordon says:

    @Mike Barnett you wrote

    "Spec#’s research focus is to understand the meaning of object invariants in the presence of inheritance" …

    While I’m NOT diagreeing with you at all … I only want to point out the inheritance part of your comment is not really relevant in the context of Visual Studio in this regard:  The class browser which should be work horse for true inheritance based programming models is not useful and can’t subclass UI controls. There are numerous challenges subclassing UI controls that need to be worked around even if you hard code the classes. WPF UI controls, best practices, suggests not subclassing UI controls. I could go on especially on the web side of things which is more screwed up then desktop development (including MVC which I was hoping would address many of these issues). The bottom line without sublcassing you don’t have inheritance!

    While I’m a very strong advocate for "true" OOP standards including inheritance, Microsoft redefines patterns/standard as they see fit to overcome short comings in their VS dev tools. This is much easier then actually the fixing the issues!

    Personally I wish all the problems with inheritance where addressed in VS before implementing additional features like this and I don’t understand why they can’t be given they got this right in 6.0 tools sets for the most part. That is what is so frustrating we are forced to develop apps with poor implementations and bugs while Microsoft introduces more technology. Why can Microsoft get what they have released right then introduce new features on a solid foundation!

  34. We’ve mentioned Code Contracts over on the BCL Blog a few times now, but never yet on the CLR Blog. Basically,

  35. Somasegar says:


    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.


  36. Green Williams says:

    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".

  37. Somasegar says:

    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.  


  38. Chris Varley says:

    @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.

  39. Normal 0 21 false false false FR X-NONE X-NONE I heard several times that high test coverage ratio, and

  40. Mark Stewart says:

    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.

Skip to main content