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!
PingBack from http://www.clickandsolve.com/?p=13327
In my Introduction to Code Contracts post, I mentioned that the tools to enable runtime checking and
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?
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.Ja
Just what we need, another dev labs project that requires a Team System -level VS 2008 license! Sigh.
@Jeremy: If you go the the site, you'll also find installers for the other (non-Express) SKUs under non-commercial license.
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.
It's about time we had support for this, thanks.
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
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!
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.
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.
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?
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.
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.