Code Contracts

Code contracts provide a way to specify preconditions, postconditions, and object invariants in your code. Preconditions are requirements that must be met when entering a method or property. Postconditions describe expectations at the time the method or property code exits. Object invariants describe the expected state for a class that is in a good state.

Code contracts include classes for marking your code, a static analyzer for compile-time analysis, and a runtime analyzer. The classes for code contracts can be found in the System.Diagnostics.Contracts namespace.

The benefits of code contracts include the following:

Improved testing: Code contracts provide static contract verification, runtime checking, and documentation generation.

Automatic testing tools: You can use code contracts to generate more meaningful unit tests by filtering out meaningless test arguments that do not satisfy preconditions.

Static verification: The static checker can decide whether there are any contract violations without running the program. It checks for implicit contracts, such as null dereferences and array bounds, and explicit contracts.

Reference documentation: The documentation generator augments existing XML documentation files with contract information. There are also style sheets that can be used with Sandcastle so that the generated documentation pages have contract sections.

All .NET Framework languages can immediately take advantage of contracts; you do not have to write a special parser or compiler. A Visual Studio add-in lets you specify the level of code contract analysis to be performed. The analyzers can confirm that the contracts are well-formed (type checking and name resolution) and can produce a compiled form of the contracts in Microsoft intermediate language (MSIL) format. Authoring contracts in Visual Studio lets you take advantage of the standard IntelliSense provided by the tool.

Most methods in the contract class are conditionally compiled; that is, the compiler emits calls to these methods only when you define a special symbol, CONTRACTS FULL, by using the #define directive. CONTRACTS FULL lets you write contracts in your code without using #ifdef directives; you can produce different builds, some with contracts, and some without.

For tools and detailed instructions for using code contracts, see Code Contracts on the MSDN DevLabs Web site.

Preconditions

You can express preconditions by using the Contract.Requires method. Preconditions specify state when a method is invoked. They are generally used to specify valid parameter values. All members that are mentioned in preconditions must be at least as accessible as the method itself; otherwise, the precondition might not be understood by all callers of a method. The condition must have no side-effects. The run-time behavior of failed preconditions is determined by the runtime analyzer.

For example, the following precondition expresses that parameter x must be non-null.

Contract.Requires( x != null );

If your code must throw a particular exception on failure of a precondition, you can use the generic overload of Requires as follows.

Contract.Requires<ArgumentNullException>( x != null, "x" );

Legacy Requires Statements

Most code contains some parameter validation in the form of if-then-throw code. The contract tools recognize these statements as preconditions in the following cases:

The statements appear before any other statements in a method.

The entire set of such statements is followed by an explicit Contract method call, such as a call to the Requires, Ensures, EnsuresOnThrow, or EndContractBlock method.

When if-then-throw statements appear in this form, the tools recognize them as legacy requires statements. If no other contracts follow the if-then-throw sequence, end the code with the Contract.EndContractBlock method.

Copy

if ( x == null ) throw new ...

Contract.EndContractBlock(); // All previous "if" checks are preconditions

Note that the condition in the preceding test is a negated precondition. (The actual precondition would be x != null.) A negated precondition is highly restricted: It must be written as shown in the previous example; that is, it should contain no else clauses, and the body of the then clause must be a single throw statement. The if test is subject to both purity and visibility rules (see Usage Guidelines), but the throw expression is subject only to purity rules. However, the type of the exception thrown must be as visible as the method in which the contract occurs.

Postconditions

Postconditions are contracts for the state of a method when it terminates. The postcondition is checked just before exiting a method. The run-time behavior of failed postconditions is determined by the runtime analyzer.

Unlike preconditions, postconditions may reference members with less visibility. A client may not be able to understand or make use of some of the information expressed by a postcondition using private state, but this does not affect the client's ability to use the method correctly.

Standard Postconditions

You can express standard postconditions by using the Ensures method. Postconditions express a condition that must be true upon normal termination of the method.

Contract.Ensures( this .F > 0 );

Read more: MSDN

Posted via email from Jasper-net