Vlad's blog

In programming veritas

Introduction to Code Contracts

leave a comment »

Starting from .Net 4.0 we have a support of new design by contracts technology called Code Contracts. This post is quick introduction to Code Contract’s basic elements: preconditions, postconditions and invariants with practic examples how to use them.

Suppose we develop an application for online flight booking service. User should go through the following steps in order to book a ticket.

  • Choose a seat from seat map
  • Login into the system
  • Payment

This logic is usually implemented as series of screens that follow each other. The Command pattern can be used in the implementation. Consider ICommand interface which must be implemented by each screen.

interface ICommand
{
    void Execute(Context context);
}

SelectSeatsCommand class encapsulates logic for choosing a seat from the list of available seats.

class SelectSeatsCommand : ICommand
{
    public void Execute(Context context) { }
}

Context class stores a state common for all commands. The definition is below.

class Context
{
    public int AdultCount { get; set; }
    public int ChildCount { get; set; }
    public OnlineBookingServer Server { get; set; }
}

OnlineBookingServer provides all services needed for business logic implementation in screens.

Preconditions

A precondition specifies a condition which is validated before a method is invoked. The Contract.Requires(bool condition) method is used to check a precondition. In our example we express two preconditions for the SelectSeatsCommand.Execute method. First we need to make sure context.Server is not null. After that we check whether there are empty seats.

class SelectSeatsCommand : ICommand
{
    public void Execute(Context context)
    {
        Contract.Requires(context.Server != null);
        Contract.Requires(context.Server.GetAvailableSeats() > 0);
    }
}

Postconditions

Postconditions are contracts for the state of a method when it terminates. The Contract.Ensures(bool condition) is used to check a postcondition. In our example we need to make sure that amount of selected seats is less or equal than amount of empty seats.

public void Execute(Context context)
{
    Contract.Requires(context.Server != null);
    Contract.Requires(context.Server.GetAvailableSeats() > 0);
    Contract.Ensures((context.ChildCount + context.AdultCount) <= context.Server.GetAvailableSeats());

    context.ChildCount = 0;
    context.AdultCount = 1;
}

You may notice that postconditions are placed at the top of the method along with preconditions. By definition preconditions should be placed at the end of the method and validated when the method terminates. Technically speaking, the compiler does not generate any code for contracts,there is special utility ccrewrite that does actual code generation. It is invoked after the compiler finishes its job as a part of build process. The utility finds all occurrences where contracts are defined and injects own code based on a particular contract semantics. As the result of ccrewrite work the Contract.Ensures which was originally placed at the beginning of the method was moved to the end.

Invariants

These are object-wide contracts about a condition that is guaranteed to always hold. It cannot be checked with either preconditions or postconditions. Consider class OnlineBookingServer to illustrate invariants. This class provides all services needed for business logic implementation in screens. Technically speaking, OnlineBookingServer is a proxy that establishes a connection with some remote service that does actual work. I don’t want to deep into the details of interpocess communication between OnlineBookingServer and the remote server. The only thing I want to express here is a fact that connection must be active in order to provide correct implementation of every methods of OnlineBookingServer. The implementation that does not make use of code contracts is shown below.

class OnlineBookingServer
{
    public int GetAvailableSeats()
    {
        if (!IsConnected())
            throw new InvalidOperationException("No connection to remote service");
    }
}

The drawback of this implementation is the need to place a condition in the each method we want to validate. The invariants offer better solution. Invariant condition must be placed in a separate method that has attribute [ContractInvariantMethod] defined.

[ContractInvariantMethod]
private void EnsureConnected()
{
    Contract.Invariant(IsConnected() == true);
}

Interface contracts

One of the most powerful code contracts features are interface contracts. Suppose we want to perform validation context != null for each implementations of ICommand.Execute(Context context). Since interface can’t have implementation we need to place contract conditions in a separate class that implements this interface.

    [ContractClass(typeof(CommandContracts))]
    interface ICommand
    {
        void Execute(Context context);
    }

[ContractClass] attribute is used to specify class that implements ICommand interface contract. This class must have an attribute [ContractClassFor] defined in order to establish an association between interface and contract class.

[ContractClassFor(typeof(ICommand))]
internal abstract class CommandContracts : ICommand
{
    public void Execute(Context context)
    {
        Contract.Requires(context != null);
    }
}

Contract failure

What happens when a contract fails? The answer depends largely on a purpose of using contracts. There are several options available to customize code contracts in the project settings. You are able to include only preconditions, preconditions and postconditions or turn code contracts off for particular project configuration. All types of contracts are turned on by default. When contract is violated ContractException exception is raised. But you are unable to catch this type of exception in your code because it is available as Exception type. It is supposed that program must be interrupted when any contract is violated. Generally speaking, there is some difference between exception and violation of contract. Exception is usually raised when critical error is occurred that can’t be handled in the current scope and must be propagated higher in the stack. A nature of error might vary from resource allocation failure to coding error. A contract failure is usually caused by coding error and program termination looks like a natural way to handle this type of problem. Of course this approach is not applicable for variety of applications that can’t be terminated even in case of critical error. In order to solve this problem you can handle global event Contract.ContractFailed that is raised when a contract fails. A handled failure won’t trigger an exception if you call args.SetHandled().

Contract.ContractFailed += (sender, args) =>
    {
        Console.WriteLine("{0}: {1} : {2}", args.FailureKind, args.Condition, args.Message);
        args.SetHandled();
    };

A diagnostic message will be printed when a contract fails. A handled failure won’t trigger an exception because we called args.SetHandled().

References

  1. С# in Depth. Second Edition. Jon Skeet
  2. Code Contracts User Manual
Advertisements

Written by vsukhachev

July 12, 2011 at 4:15 am

Posted in Development

Tagged with ,

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: