Introduction to Code Contracts [Melitta Andersen]

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.

Comments

• Anonymous
  November 11, 2008
  PingBack from http://www.tmao.info/introduction-to-code-contracts-melitta-andersen/

• Anonymous
  November 11, 2008
  The comment has been removed

• Anonymous
  November 11, 2008
  Update: As Chris Nahr pointed out, there&#39;s a blog post by Melitta Andersen of the BCL team explaining

• Anonymous
  November 12, 2008
  If I make one API suggestion (which may already be followed, I have no idea)... Ensure You mention: "They also have an overload that takes a string parameter as a message for when the contract is false." Please, please, PLEASE make the overloaded method take a "string format, params object[] args" argument list and not just a string.  For simple code there will be no difference for the developer, but if you ever need to "format" the message string it looks far cleaner than needing to insert string.Format().  Compare: CodeContract.Requires(parameter >= 0, "parameter value {0} must be greater than 0", parameter); To: CodeContract.Requires(parameter >= 0, string.Format("parameter value {0} must be greater than 0", parameter));

• Anonymous
  November 12, 2008
  First showed at the PDC as a part of this Pex session was support for contracts , if you have seen the

• Anonymous
  November 13, 2008
  This is the greatest news I heard in years. I was very exited about the things Spec# could bring us, but bringing verification to the rest of the framework is superb. The most development teams I help use C# and moving to another language wouldn’t be feasible for them. I have a question though. I’m a big believer of the Framework Design Guidelines and they state that a failing precondition should throw an ArgumentException (or descendant). How does Contracts deal with this? I don’t think it’s necessarily to add a ‘string, parms object[]’ overload to the Requires and Ensures methods, as Melitta Andersen suggests. Using a string.Format() would be sufficient when the post-compilation process changes the implementation to something like ‘if (conditions) throw new Exception(string.Format(…))’. How is this currently implemented?

• Anonymous
  November 14, 2008
  First, great news! I think this is the best news coming out for .NET 4. It's something I've wanted for years. Question: Care to talk a little bit about how this works for interfaces, where you can't actually put code inside your methods? interface IFoo {    DoSomething(string s)    {        CodeContract.Requires(s != null);    }; } In the above interface, the compiler will issue an error; you can't have code statements inside an interface. (This is another argument in favor of using attributes, as they are allowed in interfaces.) Another question: If attributes were powerful and expressive enough, would the team consider implementing code contracts using attributes? I ask because there has been a lot of feedback on the MS Connect website to allow more expressiveness inside attributes. See https://connect.microsoft.com/VisualStudio/feedback/ViewFeedback.aspx?FeedbackID=254057

• Anonymous
  November 14, 2008
  Hi snprbob86, Thanks for passing along the link to the Python decorators.  That looks like an interesting contract system, and seems to have some of the same concepts as the one we implemented.  For example, the ability to have contracts at debug time only or the ability to incorporate functions into conditions to make them more expressive are elements of our own code-based implementation. Thanks, Melitta

• Anonymous
  November 14, 2008
  Hi Jonathan, Thanks for the API suggestion.  It's an interesting idea, and does make the code a little neater.  However, at this point we're trying to keep the code contract APIs as minimal as possible.  This makes it less complicated for the tools to extract the conditions.  Overloads with more parameters make the task more difficult.  It's something we'll think about, but we may not be able to make it happen in this release. Thanks, Melitta

• Anonymous
  November 14, 2008
  Hi Steven, You have some good questions here.  We don't have any official Framework Design Guidelines yet for when to use code contracts and when to use ArgumentExceptions.  While many of us are fans of contracts, clearly we can't just say "change all of your existing preconditions to code contracts," because there is often already infrastructure in place around throwing these ArgumentExceptions and there is too much potential to break people.  This is a brand new feature, and we're doing some experimentation internally to find out what works best so that we can make more informed recommendations. As for your question about how we implement the behavior of code contracts under the hood, we don't convert it to an exception.  In the CTP bits we check the condition and then tear down the process if they fail.  We use the string as part of a message to the user when this happens.  As I mentioned above, we're considering options to make this behavior more flexible, and especially to make it friendlier to hosts.   Thanks, Melitta

• Anonymous
  November 14, 2008
  Hi Judah, Thanks for pointing out that I neglected to mention how code contracts work on interfaces.  As you've said, you can't put code into interface methods.  What you do is create a separate class to contain the contracts that <i>explicitly</i> implements the interface.  Then you link them with a pair of attributes:  [ContractClass(Type)] and [ContractClassFor(Type)].  For example you could have an interface IFoo  with a class IFooContract that contains the contracts.    [ContractClass(typeof(IFooContract))]    interface IFoo    {        int DoSomething(string parameter);    }    [ContractClassFor(typeof(IFoo))]    sealed class IFooContract : IFoo    {        int IFoo.DoSomething(string parameter)        {            CodeContract.Requires(parameter != null);            CodeContract.Ensures(0 <= CodeContract.Result<int>());            throw new NotImplementedException("This method is only for interface contracts.  Do not call");        }    } As for your question about attributes, if they were powerful enough, we certainly would have considered using them to implement contracts, though I can't say for sure what we would have decided.    As it is, we don't know of any plans for more expressive attributes, and even if they do come along later, we would already have an established contracts system.  There would by that point be many factors to take into consideration when looking at adding attribute support. Thanks, Melitta

• Anonymous
  November 15, 2008
  I don't like using attributes for the contracts. It’s almost impossible to do compile time checking on them, and they’re very verbose. I've seen Spec# and it has the ideal language syntax. I hope this syntax makes it to C# 5.0. (Well… I'm really hoping C# 4.0 will have all this, but I know this isn't going to happen ;-)).

• Anonymous
  November 15, 2008
  Judging by its past track, one .NET language that will almost certainly provide syntactic sugar for the library contracts is Delphi Prism (aka RemObjects Oxygene). They do in fact already have "require", "ensure", and "invariant" keywords, so it would make sense for them to plug them into those BCL bits for .NET 4.0, and extend the syntax to cover all other cases ("require ... on raise ..." etc).

• Anonymous
  November 20, 2008
  I've been catching up on my blog reading...interesting stuff I came across; PNRP in Windows 7 being...

• Anonymous
  November 25, 2008
  InfoQ に日本語記事が載ったので f(^^; .NET 4 の新機能を探る： コード契約作者 Jonathan Allen, 翻訳者 金森 諭 投稿日 2008年11月22日 午前12時53分 契約による設計は静的型付けのように、 コンパイル時に検証されないと一定の動作を実行することができないという考え方だ。 契約

• Anonymous
  December 01, 2008
  Hi, Contracts are really nice. In order to be able to use them properly though, we will need pre and postconditions from all the classes we use in our program, for exemple, List<T>.Count is always positive or zero. Are you going to update the whole BCL with code contracts for .NET 4.0? This sounds like a huge work, but without that, contracts won't be usable at their full potential. My second question is why C# wouldn't have a syntax that would get translated into CodeContracts upon compilation. With this we get a good langage support in C#, as well as the ability to have it supported accross all CLR langages.

• Anonymous
  February 23, 2009
  In my Introduction to Code Contracts post, I mentioned that the tools to enable runtime checking and

• Anonymous
  March 04, 2009
  We’ve mentioned Code Contracts over on the BCL Blog a few times now, but never yet on the CLR Blog. Basically,

• Anonymous
  March 15, 2009
  Dzień: 14 marca 2009. Miejsce: Wydział Biologii UW. Wydarzenie: druga edycja konferencji Communities

• Anonymous
  March 15, 2009
  Relacja z C2C (Communities to Communities) 2009