Microsoft offers language-agnostic coding technology

Code Contracts enables "design by contract" programming for .Net

Bolstering developers, Microsoft Research has developed Code Contracts, offering a language-agnostic way to express coding assumptions in .Net.

The technology was released on the Microsoft DevLabs site this week. Code Contracts provide the innovations of "design by contract" programming to .Net programming languages. Contracts take the form of pre-conditions, post-conditions, and object invariants, and they act as checked documentation of APIs. Also, contracts improve testing via runtime checking and enable static contract verification and documentation generation.

[ At the VSLive conference today, Microsoft showed off the new Visual Studio UI. ]

"Today’s release, Code Contracts for .Net, is a general design-by-contract mechanism that all .Net programmers can now take advantage of," said S. "Soma" Somasegar, senior vice president of the Microsoft developer division, in his blog on Monday. "Using it, programmers provide method preconditions and post-conditions 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.) "

Contracts, Somasegar said, are used for runtime checking, static verification, and documentation generation. Additionally, contracts allow automatic documentation checking and improved testing. Code Contracts for .Net consists of three components: the static library methods used for expressing the contracts, a binary rewriter, and a static checker.

The binary rewriter modifies a program by injecting contracts, which are checked as part of a program execution. Rewritten programs improve testability, and each contract offers a pass/fail indication for test runs. The static checker decides if there have been any contract violations, checking for implicit contracts, such as null dereferences and array bounds, as well as checking for explicit contracts.

Code Contracts can be used within Visual Studio 2008 Team System.

The design-by-contract mechanism was pioneered by Eiffel, Somasegar said.