Code Contracts: Introduction (1 / n)

Posted on Friday, July 09, 2010 5:27 PM

This is the kick-off for my series on Code Contracts, a new addition to the .NET framework, built-in from version 4 and back ported to .NET 3.5 by use of the Microsoft.Contracts assembly. In this first post I’ll try to give a general introduction to the Code Contracts. Just what is it and what purpose does it serve.

I guess many developers have had there time writing classes for some wanna-be framework and trying to defend themselves against all kind of bogus input. So on method entry all parameters are checked for non-null values, for proper values within a predefined range, etc. Throwing ArgumentExceptions and ArgumentNullExceptions all around. An occasional ArgumentOutOfRangeException might also be on the list. And you might conclude you have your method sealed and locked down. No further hassling with the parameters, everything works perfect.

But what about the callers of your locked-down method? Are they going to obey your contract? Or are they just going to put the whole thing in a try-catch bloc and catch the ArgumentExceptions? Which IMHO is always wrong, but that’s a different issue. The compiler won’t complain about a null being passed, even though the method that is called will check for it and throw an ArgumentNullException. It will only appear as such at runtime. And this sums up just two issues we face today when designing and implementing validation checks on method entry.

Just come to think of it, what happens when your precious method gets overloaded in a derived class? You could argue that such a thing should not be possible in a valid interface design and inheritance should be on some protected method and not on a private one. But still, there is no way you can enforce your ‘contract’ to the derived method. It is not obligated to call the base method, and even if it would, it is not ensured that it would happen directly on entry of the method body. Sometimes that would even be the complete opposite of the desired way of coding.

So what’s next? There is no ‘silver-bullet’. Not for parallelism in coding, but also not for ensuring a public contract on a method. But now there is Code Contracts from Microsoft. It’s not the definite answer, but it comes a long way. The issues I mentioned above about runtime failure, inheritance and such do not apply to Code Contracts. Code Contracts get inherited by derived classes and overridden methods. And since the Code Contracts can be statically checked during compile time, it will help developers to deliver better code, with fewer runtime failures.

But what is Code Contracts? As defined at the Microsoft site:

“Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs. The contracts take the form of preconditions, post conditions, and object invariants. Contracts act as checked documentation of your external and internal APIs. The contracts are used to improve testing via runtime checking, enable static contract verification, and documentation generation.”

I could not come up with a better phrase. As can be read from this definition, the Code Contracts take the form of preconditions, post conditions and object invariants.

The following gives a quick overview of each of these:

  • Preconditions
    The preconditions define the state of the world at method entry. They must be true to ensure successful execution of the method. Often you’ll find yourself using preconditions for parameter validation. It is however still the responsibility of the caller to make sure the conditions are met. The preconditions comes in three flavors with Code Contracts:
    • Contract.Requires
      This method states a precondition, simple, plain. A small example:

      Contract
      .Requires(root != null);
    • Contract.Requires
      This method also states a precondition, but adds to the previous call a throw of the specified exception. It is also always included in the final code, as opposed to some other calls on Contract.  Here’s an example:

      Contract
      .Requires<ArgumentNullException>(root != null);
    • Contract.EndContractBlock()
      This method is to be used in legacy code where the preconditions are defined in the common way of ‘IF [condition] THEN throw [exception]’. Take for example the following code:

      if
      (root == null)
      {
        throw new ArgumentNullException("root");
      }

      Since it would not be feasible to go through all your code and rewrite all IF-THEN-THROW sections into Contract.Requires calls, the Contract.EndContractBlock method is a way of telling the tools that any preceding code in the method body before this call must be considered as preconditions. So the example should be changed to:

      if
      (root == null)
      {
        throw new ArgumentNullException("root");
      }
      Contract.EndContractBlock();

      This is needed only when there are no other contracts in the code. If you would add a post condition, the code would look like this:

      if
      (root == null)
      {
        throw new ArgumentNullException("root");
      }
      Contract.Ensures(this.currentRoot != null);
  • Postconditions
    Post conditions give a guarantee on the state at method exit. So what must be true in the state of the world when the method returns control to it’s caller. These conditions are the responsibility of the method. The declaration of the post conditions is set at the beginning of the method, just like the preconditions. The tools that come with Code Contracts will hustle the code and make sure they get called at the right times. This type of condition comes in two flavors:
    • Contract.Ensures
      This method states that a condition must be true on successful method exit. A possible example would be, upon leaving a Save method for instance:

      Contract.Ensures(this.Name != null);
    • Contract.EnsuresOnThrow
      This method enables validation of conditions at unsuccessful method exit. When the method is faced with exceptional termination, post conditions can be met for the specified exception type. A word of caution is at place here though. It is generally not a good idea to make assumptions for all exception types, so letting TException be Exception is just plain foolish. One cannot guarantee anything on the state of the world when for example a StackOverflowException or an OutOfMemoryException is thrown. Some exceptions that may be more appropriate in this case could be IOException or DbException, like so:

      Contract
      .EnsuresOnThrow<DbException>(this.Name != null);
  • Object Invariants
    The last form of Code Contracts mentioned is Object Invariants. These statements define what must be true at all public method exits for an object (instance). The responsibility of maintaining the object’s invariant is up to the developer. Object invariants must be contained in a separate method that is to be marked with the ContractInvariantMethodAttribute attribute. The name of the method is not important, but it’s signature must be a parameter-less method with a void return type. The method body must only contain calls to the Contract.Invariant(…) method, of which there must be at least one. The following example defines an invariant which states that the value in the field is never null:
    [ContractInvariantMethod()]
    void ObjectInvariant()
    {
      Contract.Invariant(this.propertyNameToHandlerMap != null);
      Contract.Invariant(this.propertySourceReference != null);
    }

In the following posts in this series I plan to be more specific on each of the mentioned methods. For now, I’ll leave it to this, with some useful links to conclude with:

That’s it for now
Meile

Feedback

# cartier pasha watches

2/6/2012 11:47 AM by replica watch
ladies watches http://www.spellshop.org/ watches for women.

# no account of time

2/7/2012 1:57 AM by fake watches
ladies watch http://www.cheap-oris-watches.com/ ladies watches.

# colt watches

2/8/2012 10:31 AM by replica watches
watch brands http://www.watchestype.net/chopard-watches.html swiss watches.

# Tom ford dress

2/17/2012 12:05 PM by Wedding Dresses
Blazers buy http://www.enabledress.com/ Evening Dresses

# plus size black party dresses

3/23/2012 3:18 PM by short evening gowns
Wedding shop http://www.offergreat.net/ Fashion design.

# Fashion online

3/27/2012 10:15 PM by Vintage house
dress store http://www.finestshow.net/ bandage dresses for cheap.

Post Comment

Title  
Name  
Url
Comment   

ATTENTION: the code you need to copy is CaSe SeNsItIvE and is required to prevent spam.
Enter the code you see:

posts - 24, comments - 125, trackbacks - 0, articles - 0

Copyright © Meile Zetstra