The technology was released on the 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 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 Tuesday, ]

"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" , senior vice president of the Microsoft developer division, in his 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.