text: Understanding and Benefiting from Code Contracts in .NET 4.0
  Note that because of the asynchronous nature of the static checks, you will not immediately see the results in the Error List. Instead, you will have to wait, depending on your project size, around ten seconds to several minutes for the checks to be finished. In the IDE, there is no direct indication (as of yet) that the checks are underway, but you can do this indirectly from Windows Task Manager. Check if the static checker process "
  cccheck.exe" is running, as it only runs when the checks are underway. The EXE can be found from the Bin directory under the installation path.
  Using pre and post conditions is simple to understand and effective, but this where the problem lies in that many code lines are still needed to enforce object state. In fact, pre and post conditions do not help much in reducing the amount of code that you need. Luckily, Code Contracts supports a feature called object invariants, which is an effective solution to the problem.
  ContractInvariantMethodattribute, through which the Code Contracts engine can find the method. Here is an example:
  [ContractInvariantMethod] protected void GlobalRules() { Contract.Invariant((Percentage >= 0) && (Percentage <= 100)); }
  With this method in place, static checks are available just like before. At runtime however, the presence of invariants alters the execution of your application slightly. After each call to a public method of the class having contract invariants in place, a second call to the invariant method is injected. This means the invariants are automatically checked without the developer doing anything special. Note however that you have to specifically enable these runtime checks, as calling the invariant checking method introduces overhead to your application. The code injection is done by a special rewriter application called
  ccrewrite.exe, part of the Code Contracts file set.
  In addition to these two basic types of checks (conditions and invariants), there is more functionality in Code Contracts. For instance, the Contracts class in the
  System.Diagnostics.Contracts namespace (refer to
  mscorlib.dll version 4.0) contains methods to enforce that array elements have certain properties. Similarly, there is a possibility to configure what happens when exceptions are thrown. This is useful especially when combined with unit tests, as you will learn later. But first a few words about static analysis.
  Benefitting from static analysis
  If you have the luxury of using any of the Visual Studio 2008 Team System editions like Team Developer or Team Tester (or the equivalent 2010 versions, for that matter), you are already likely familiar with the valuable Code Analysis tool (Figure 4). This tool allows you to statically scan your application's code, and receive a report of potential issues found regarding areas such as performance, security, globalization, object naming, application design, and so on.
  Figure 4. Visual Studio Team System provides the valuable Code Analysis tool.
  The static analysis provided by Code Contracts is similar in nature: it tries to spot problems before they are noticed at run-time. For instance, if a call to a certain method using pre-conditions would cause the pre-condition to fail, Code Contracts reports about its findings when you build your application.
  For instance, assume you had created a class to process numeric data samples and you need to calculate an average value. Your class might look something like this:
  internal class NumericSamples { internal int Average(int[] numbers) { int sum = numbers.Sum(); int count = numbers.Length; return sum / count; } }
  Here, the Average method calculates the average of the samples given as a parameter. Since there is no guarantee that the parameter has a valid set of values, the final division might fail. For instance, the number of samples could be zero (i.e. an empty array was passed), which in turn will cause a division by zero when calculating the average.
  Although Code Contracts cannot tell you straight away that this is a possibility, you can indirectly get information that a condition might be violated. The logical check to make sure there are more than zero samples in the array:
  internal class NumericSamples { internal int Average(int[] numbers) { Contract.Requires(numbers.Length > 0); int sum = numbers.Sum(); int count = numbers.Length; return sum / count; } }
  With this implementation, the method could be called for instance like this:
  NumericSamples samples = new NumericSamples(); int avg = samples.Average(new int[] { 1, 5, 3, 7, 4, 9, 2, 8 });
  If you now compile the application with static analysis enabled, the analysis will report success similar to that shown earlier in Figure 3:
  contracts: Checked 1 assertion: 1 correct
  This message tell you that the condition in the Average method is always satisfied, and thus the given requirement is met....