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