This blog post is to provide a bit more detail about the Code Contracts feature that was recently announced at the PDC and in Justin’s blog entry, and that can be found in the Visual Studio 2010 and .NET Framework 4.0 CTP.  I’ll include some information on what can be found in the CTP, some of the history and design decisions we made while developing the feature, and some places to get more information.  Both of the announcements mentioned above give details about why we added this feature, but I’ll summarize here.  The main point of contracts is to reduce bugs by helping you not write them in the first place, or at least catch them sooner.  Contracts let you express statements about the behavior of your code in a way that is accessible to tools for runtime and static analysis.

What’s not in the CTP

One thing you should note is that the tools to enable runtime checking and static analysis are not in the CTP.  However, you can still write your contracts now and then use the tools when they become available.  This works because the contracts are conditionally defined.  They’ll only appear in your code when you have the CONTRACTS_FULL symbol defined.  Until the tools are available and runtime checking is enabled, do not define this symbol.  Full contract checking will not work without the tools.  However, you also have the option of getting only preconditions with the CONTRACTS_PRECONDITIONS symbol.  Preconditions happen to be in the correct place in the code, so your program will still run with this symbol defined.  But the runtime checking tool provides many additional benefits, such as contract inheritance, so checking is still not recommended without the tools.

What is in the CTP

The CTP includes a CodeContracts class in the System.Diagnostics.Contracts namespace that allows you to write contracts in your code.  All contracts are static methods that return void.  They take a Boolean expression which encodes the condition that must be true.  They also have an overload that takes a string parameter as a message for when the contract is false.  Contracts are declarative and come at the beginning of your method.  You can think of them as part of the signature.  Here’s a rundown of what contracts are in the CTP:

• Preconditions
  Preconditions are statements about what must be true at method entry for successful execution of the method.  It’s the responsibility of the caller to make sure these conditions are met.  Often, preconditions are used for parameter validation.  There are 3 possible ways to encode preconditions with code contracts:
   
  • CodeContract.Requires
    This method simply states a precondition.  Here’s an example:
    
        CodeContract.Requires(parameter >= 0);
    
    
  • CodeContract.RequiresAlways
    This method is the one exception to the conditional compilation rule.  It is always included, no matter which symbols are defined.  Thus, you can use RequiresAlways for preconditions that you want in your released code.  Here’s an example:
    
        CodeContract.RequiresAlways(parameter >= 0);
    
    
  • CodeContract.EndContractBlock
    This method name might seem a bit odd to include in the precondition section, so let me explain.  Much code already exists in the world that has some kind of parameter validation in the form of “if [condition] then throw [exception]”, e.g.
    
        if (parameter < 0)
            throw new ArgumentOutOfRangeException();
    
    
    We don’t expect everyone to go back and change their existing validation code.  However, we wanted a way to let the tools recognize these legacy contracts.  So we added the CodeContract.EndContractBlock method, which tells the tools that all if-checks of that form before the call can be considered preconditions.
    
        if (parameter < 0)
            throw new ArgumentOutOfRangeException();
        CodeContract.EndContractBlock();
    
    
    This method is needed only if you have no other contracts in your method, as all CodeContract preconditions and postconditions have this effect.
    
    
• Postconditions
  Post conditions are guarantees a method makes about what must be true at the conclusion of a method.  It is the method’s responsibility to live up to those promises.  These are declared at the beginning of a method, just like preconditions.  The tools take care of checking them at the right times.  There are two types of post conditions you can write with the CodeContract class.
   
  • CodeContract.Ensures
    This method states conditions that must be true upon successful method exit.  For example, this condition says that when the method exits the value will not be null.
    
        CodeContract.Ensures(SomeSharedState != null);
    
    
• CodeContract.EnsuresOnThrow<TException>
  This method makes guarantees about exceptional termination from a method.   In general, such guarantees can only be made for very specific exceptions, so letting TException be Exception is not a good idea.  For example, the following condition says that if an IOException escapes this method, the given variable is not null.
  
      CodeContract.EnsuresOnThrow<IOException>(SomeSharedState != null);
  
  
• Special values for postconditions
  As you can imagine, it is often necessary to refer to certain values in postconditions, such as the result of the method, or the value of a variable at method entry.  There are methods in the CodeContract class that allow this; they are valid only in a postcondition.
   
  • CodeContract.Result<T>()
    This method represents the value returned from a method.  The T parameter indicates the return type.  For example, the following condition says that the result of this method is always non-negative.
    
        CodeContract.Ensures(CodeContract.Result<Int32>() >= 0);
    
    
  • CodeContract.OldValue<T>(T value)
    This method represents the value as it was at the start of the method or property.  It captures the pre-call value in a shallow copy.  For example, this condition says that the method increased the value of SomeSharedInt.
    
        CodeContract.Ensures(SomeSharedInt > CodeContract.OldValue(SomeSharedInt));
    
    
  • CodeContract.ValueAtReturn<T>(out T value)
    This method is just to let you refer to the final value of an out parameter in a postcondition.  Since you write postconditions at the beginning of a method, the compilers would otherwise complain as the parameter hasn’t been assigned yet.  Other by-reference parameters don’t need this method.  Normal parameters don’t need this method because the compiler doesn’t care if it sees references to their values before it sees an assignment to them.
    
    
• Object Invariants
  The last major kind of contract that can be expressed with the CodeContract class is the object invariant.  Object invariants are statements about what must be true at all public method exits for an object.  It is up to the programmer to ensure these invariants are maintained.  Object invariants are contained in a separate method that is marked with the ContractInvariantMethodAttribute.  The name of the method does not matter, but it must be parameter-less and return void.  That method contains some number of calls to the CodeContract.Invariant method.  Here’s an example of an invariant stating that the value in Data is always non-negative.
  
          [ContractInvariantMethod]
        void ObjectInvariant() {
            CodeContract.Invariant(Data >= 0);
        }
     


• CodeContract.Assert and CodeContract.Assume
  I’ll briefly touch on the other two types of contracts included in the class.  Assert and Assume, unlike the others, aren’t part of a method’s signature, and unlike the others they don’t come at the beginning of a method.  They’re simply statements about what must be true at a particular point in the code.  There exists many other ways to do this verification, but the main value with these methods is that they can be recognized by the tools.  The difference between Assert and Assume is that an Assume is your way to tell the static checker that instead of trying to prove the expression to be true, it should add the expression to its body of facts for your code.

Please note that this is only what is in the CTP.  This is a feature still under development, and things could change before we ship.  In fact, we’re considering a couple of changes.  One is changing the class name from CodeContract to Contract to make contracts more readable.  Another is adding more sophisticated runtime failure behavior that is customizable by applications and hosts.

History and Design Decisions

The idea for this feature originated with the Spec# project in Microsoft Research.  Spec# has its own programming language, an extension of C#, which includes contracts in the syntax of the language.  We’re working closely with a team from Microsoft Research to bring contracts to the BCL.  One of the main questions we’ve had about the way we are including contracts in the .NET Framework is why we chose to implement them as library calls instead of making them part of “the language.”

There are quite a few reasons for this, but one of them is that the CLR is the Common Language Runtime, and we wanted a feature that all of the languages using the .NET Framework could use, not just one of them.  The best way to do this was with library calls.  As far as compilers need to be concerned, these are just static method calls.  Spec# was great because it had contracts integrated into the language, but that only solved the problem for one language. 

People have brought up attributes as another way we could have accomplished this.  One argument for that approach is that contracts are declarative, and this would make them look more like part of the method signature instead of the method body.  The problem with this approach is that attributes are very limited in what they can express.  It would be difficult or impossible to use attributes for all of the contracts you can write in code. 

If you’re concerned about it because of the aesthetics, you might want to check out Scott Guthrie’s demo of VS2010, which starts about 88 minutes into this PDC2008 Keynote.

More Information

There are a few places you can go if you’re looking for more information.

• Microsoft Research’s code contracts website.
• For discussion of contracts, we’re currently sharing the Pex forum until we get our own.  Please use the Code Contracts Community thread.
• To provide feedback, you can make comments to this post, send mail via this blog’s contact form, or e-mail codconfb_at_microsoft_dot_com.