Code Contracts FAQ

 

Why not use Debug.Assert instead of Contract.Requires etc..?

Use of Debug.Assert is encouraged within your code to specify invariants that your code should satisfy at certain program points. However Debug.Assert is ill-suited to specify method-boundary contracts for the following reasons:

  • Pre-condition visibility: Pre-conditions specify the conditions a caller should establish prior to calling a method. Because of this, pre-conditions must be visible to the caller in the sense that the caller should be able to determine if he/she satisfies the pre-conditions. Thus, pre-conditions should not refer to internal state that the caller cannot access. Debug.Assert on the other hand can be used to specify internal consistency. Use Contract.Requires for pre-conditions so humans and tools can identify the condition as a method contract, rather than an internal consistency check.
  • Post-conditions: Using Debug.Assert for post-conditions is tedious and error-prone. A normal post-condition should be checked on every normal return from a method. With {Debug.Assert}, the programmer is forced to insert it at the appropriate places in the code. This is error prone, causes duplication, and is hard to maintain. Use Contract.Ensures at the beginning of a method to specify the post-condition once. The tools take care to interpret it at all exit points. Contract.Ensures also distinguishes the post-condition from an internal consistency check.
  • Inheritance: Method contracts of overridden methods should have the same pre-condition as their parent methods, and post-conditions that are at least as strong as the parent method's post-conditions. With Debug.Assert, the programmer has to duplicate pre- and post-condition checks in his code, making it error prone. Also, there is no tool support to enforce the required consistency among contracts in overridden methods. With Contract.Requires and Contract.Ensures, the tools take care of enforcing consistency and proper inheritance of contracts.

 

What happens at runtime when a contract fails?

The failure behavior is highly configurable. The binary rewriter has an option that allows the user to specify a set of methods to call for every contract failure. See Section 7.1 in the user guide for information on how to use this.

When the user does not specify a set of methods, then the default behavior is to first see if any handlers are registered. This is described in Section 7.2 of the user guide. If no handler is registered, or if no registered handler signals that the contract failure has been handled, then the method Contract.Failure is called. Its behavior depends on whether you are using the CLR v4.0 CTP or not:

  • If you are using it, then the failure mode is to simply assert and then terminate the process using Environment.FailFast. The behavior of future releases will be defined when they are available.

  • If you are not using it (for instance, you are using .NET 2.0 or 3.5), then you are using the implementation of the contract class supplied in the assembly Microsoft.Contracts.dll and Debug.Assert is called with an appropriate string specifying what kind of failure was encountered (pre-condition, post-condition, etc...). Thus, the programmer is free to use the customization provided by Debug.Assert using assert listeners to obtain whatever runtime behavior they desire (e.g., ignoring the error, logging it, or throwing an exception).

    // Clears the existing list of assert listener (the default pop-up box)
    System.Diagnostics.Debug.Listeners.Clear();
    // Install your own listener
    System.Diagnostics.Debug.Listeners.Add(MyTraceListener);

 

Why not use attributes instead of method calls to specify contracts?

The advantage of using custom attributes is that they do not impact the code at all. However, the benefits of using method calls far outweigh the seemingly natural first choice of attributes:

  • Runtime support: Without depending on a binary rewriter, contracts expressed with attributes cannot be enforced at runtime. This means that if there are preconditions (or other contracts) that you want enforced at runtime, you need to either duplicate the contracts in the code or else include a binary rewriter in your build process. Contract.RequiresAlways serves both as a declarative contract and as a runtime-checked validation.
  • Need for parsing: Since the values that can be used with custom attributes are limited, conditions end up being encoded as strings. This requires defining a new language that is appropriate for all source languages, requires the strings to be parsed, duplicating all of the functionality the compiler already possesses.
  • Lack of IDE support: Expressed as strings, there is no support for Intellisense, type checking, or refactoring, all of which are available for authoring contracts as code.

 

I already use "if (...) throw ..." to validate pre-conditions. What now?

You don't have to convert your conditions to use Contract.Requires to take advantage of the Code Contracts tools. All that is required for the tools to recognize your "if (...) throw ..." code as a pre-condition is:

  • It must appear at the beginning of the method, prior to any code that performs actual work.
  • It must be side-effect free.
  • It must be followed by a call to Contract.XXX: if you are adding Contract.Ensures after your tests or additional Contract.Requires, then your pre-conditions will be recognized automatically. If you don't have any additional method contracts after the "if (...) throw ..." code, add the contract end marker call Contract.EndContractBlock();. A typical use looks as follows:

void MyMethod(Foo foo)
{
  if (foo == null) throw new ArgumentNullException(...);
  Contract.EndContractBlock();

  ... normal method code ...
}