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:
Precondition visibility: Preconditions specify the conditions a caller should establish prior to calling a method. Because of this, preconditions must be visible to the caller in the sense that the caller should be able to determine if he/she satisfies the preconditions. Thus, preconditions 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 preconditions so humans and tools can identify the condition as a method contract, rather than an internal consistency check.
Postconditions: Using Debug.Assert for postconditions is tedious and error-prone. A normal postcondition 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 postcondition once. The tools take care to interpret it at all exit points. Contract.Ensures also distinguishes the postcondition from an internal consistency check.
Inheritance: Method contracts of overridden methods should have the same precondition as their parent methods, and postconditions that are at least as strong as the parent method's postconditions. With Debug.Assert, the programmer has to duplicate pre- and postcondition checks in their 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.
[Note: This is more restrictive than absolutely necessary. Theoretically, preconditions could be allowed to be weakened, but our experience with Spec# has indicated that this is of very little practical use and just makes the tooling more complicated. If you have any scenarios where you would really benefit from weakening preconditions, please let us know about it!]
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 (precondition, postcondition, 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)
// Install your own listener
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 preconditions. 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 cannot have an else branch.
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(...);
... normal method code ...
Do Code Contracts have anything to do with Spec#?
Code Contracts is a spin-off from the Spec# project. Spec#’s research focus is to understand the meaning of object invariants in the presence of inheritance, call backs, aliasing and multi-threading. Spec# is a superset of C# v2.0 and uses a source level rewriter to weave the contracts into the code. It uses verification condition generation and a theorem prover for the static verification of Spec# code. But dealing soundly with all the complex issues around maintaining object invariants has a price: verification becomes non-trivial. That’s why Spec# also needs an ownership discipline to know which objects may alias or cannot alias each other.
Code Contracts is the result of learning from Spec# what works and what doesn’t. Unlike Spec#, Code Contracts are language agnostic, and thus work across all .NET languages, from VB to C# to F#. The rewriter works on MSIL and thus had no dependency on particular compilers. Its static analysis engine uses abstract interpretation, which is much faster and more predictable than verification; furthermore abstract interpretation infers loop invariants and method contracts, which helps in adoption and ease of use of Code Contracts.