Writing code contracts on concrete types as I've been doing so far throughout this series is a good skill to have, of course. But if you're like me, most of your development is interface-centric these days. In this segment in the series concerning Microsoft Code Contracts, I'll examine how to write contracts on interfaces and abstract classes, giving you the power to define contracts once to be used across a family of classes.

Let's begin by examining an interface called IAccount. It defines a read-only property for the account balance and two methods for depositing and withdrawing funds.

namespace Interfaces
{
    public interface IAccount
    {
        double Balance { get; }
        void Deposit(double amount);
        bool Withdraw(double amount);
    }
}

If you were to implement the IAccount interface in a very simple way on a class called SimpleAccount, it might look something like this:

using System;
using Interfaces;

namespace Implementation
{
    public class SimpleAccount : IAccount
    {
        public double Balance { get; private set; }

        public void Deposit(double amount)
        {
            if (amount < 0.0d)
                throw new ArgumentOutOfRangeException();
            Balance += amount;
        }

        public bool Withdraw(double amount)
        {
            if (amount < 0)
                throw new ArgumentOutOfRangeException();
            if (amount > Balance)
                return false;
            Balance -= amount;
            return true;
        }
    }
}

Given what you've learned about Microsoft Code Contracts so far, you might be ready to augment the guard code in the Deposit and Withdraw methods with calls to Contract.Requires() like this:

public void Deposit(double amount)
{
    Contract.Requires(amount >= 0.0d);

    if (amount < 0.0d)
        throw new ArgumentOutOfRangeException();
    Balance += amount;
}

public bool Withdraw(double amount)
{
    Contract.Requires(amount >= 0.0d);
    Contract.Requires(amount <= Balance);

    if (amount < 0)
        throw new ArgumentOutOfRangeException();
    if (amount > Balance)
        return false;
    Balance -= amount;
    return true;
}

But when you build the code with these preconditions in it, you'll get some warnings:

Warnings generated when trying to implement a contract on an interface implementation.

Microsoft Code Contracts doesn't allow the implementation of an interface to define contracts unless the enclosing class is abstract and marked with a special attribute named ContractClassForAttribute. This abstract class never really gets instantiated or inherited from again. In fact, you may also define the class that implements the contracts for an interface as a sealed class, too, meaning that it cannot be inherited from. The idea is that there is one and only one implementation of the contracts for an interface. Code Contracts never intends to instantiate the class so defining it as abstract is perfectly OK. It's just a container for the contracts and nothing more.

If you've worked with ASP.NET Dynamic Data annotations or with ASP.NET MVC data validators, you know how the MetadataTypeAttribute is used to mark a class that defines constraints on the members of a data transport class. Code Contracts uses the ContractClassFor attribute to do something quite similar. This specially marked "buddy class" is a place to define some metadata about the interface. We would prefer to write it into the interface definition itself, of course. But languages like C# and Visual Basic.NET don't allow code to exist within an interface declaration. So we have to put the contracts for the interface members someplace else. A buddy class that implements the interface works well for this.

Let's take a look at one of these buddy classes now. The following code describes the original interface IAccount and a new abstract class called AccountContracts that implements the contracts for the IAccount method. The AccountContracts class is the buddy class. It will never be instantiated by the Code Contracts static checker or by the runtime rewriter. But they will borrow the contracts defined in the buddy class and use them to enforce the rules on other implementations of the IAccount interface that are encountered:

using System;
using System.Diagnostics.Contracts;

namespace Interfaces
{
    [ContractClass(typeof(Contracts.AccountContracts))]
    public interface IAccount
    {
        double Balance { get; }
        void Deposit(double amount);
        bool Withdraw(double amount);
    }

    namespace Contracts
    {
        [ContractClassFor(typeof(IAccount))]
        internal abstract class AccountContracts : IAccount
        {
            public abstract double Balance { get; }

            void IAccount.Deposit(double amount)
            {
                Contract.Requires(amount >= 0.0d);

                //throw new NotImplementedException();
            }

            bool IAccount.Withdraw(double amount)
            {
                Contract.Requires(amount >= 0.0d);
                Contract.Requires(amount <= Balance);

                throw new NotImplementedException();
            }

            [ContractInvariantMethod]
            private void Invariants()
            {
                Contract.Invariant(Balance >= 0.0d);
            }
        }
    }
}

See how the AccountContracts class is abstract and marked with that ContractClassFor attribute? See how the attribute is naming the IAccount type as the interface for which it implements contracts? You can also see the redundancy I talked about right there. On the line after the ContractClassFor attribute which specifies that the class defines the contracts for IAccount, the class declares that it implements the IAccount interface. Other important things to note in this code are:

  • Since the class is abstract, some of the IAccount interface members can continue to be abstract if that's what you need. In this case, I have no intention of defining a contract on the Balance property since it's readonly as defined in the interface. So it's included here as an abstract member, i.e. it has no implementation, and that's completely OK.
  • Methods in the buddy class that have some kind of non-void return type don't have to return any value at all. But they need a return value to compile correctly. You can use the default(T) construct in C# to return the default of a type or you may simply throw an exception at the end of the method to make it compile as I did in this code. The exception isn't really going to be thrown, of course. It's just there to satisfy the compiler. Remember, the static checker and the runtime rewriter for Code Contracts are going to borrow the contract code for each implementation of the interface. But they won't borrow the thrown exception code or any other code you happen to include that's not contract-oriented. Only the contracts will be extracted from the buddy class. Everything else will be ignored.
  • Methods that have no return type, like the Deposit method in the IAccount interface, don't need to return anything or throw an exception. Notice here that I've commented out the throw statement in the AccountContracts implementation of the Deposit method to show that it's not needed. The compiler is satisfied without having to return a value in these cases.
  • You can also add object invariants to a buddy class that implements the contracts for an interface. Here, I've included an invariant that ensures that the Balance property will never be negative.

What did I miss? Well, if you look carefully at the code, you will see another attribute marking the interface itself. If you weren't paying strict attention, you could easily have missed it because it looks an awful lot like the ContractClassFor attribute we studied a few moments ago. This attribute, although similarly named, is fundamentally different. It's the ContractClassAttribute and it's used to indicate the one and only class that will implement the contracts for this interface. You can see from the code that it's naming the AccountContracts class as the implementer of the contracts on the IAccount interface.

One way of thinking about this pair of attributes is that the ContractClass attribute points forward to the class that implement the code contracts for an interface and the ContractClassFor attribute points backward from the code contract implementer to the interface for which the contracts are being defined. I said earlier that the backward-pointing ContractClassFor attribute wasn't strictly required in the current version of Microsoft Code Contracts. But the forward-pointing ContractClass attribute is required. A side effect of this requirement is that if you are working with a compiled interface, for which you do not have source code access, you may not define code contracts on it. You'll have to create an intermediate interface over which you do have control and put the ContractClass attribute there.

If we pull the Contract.Requires calls from the Deposit and Withdraw methods as shown in the last listing of the SimpleAccount class and build with the contracts being implemented in the AccountContracts buddy class instead, you'll see that the static checker is satisfied with all of our assertions. Now, let's add some code that actually uses the SimpleAccount class to see our contracts in action.

using System;

class Program
{
    static void Main()
    {
        var account = new Implementation.SimpleAccount();

        Console.WriteLine(
            "After construction, Balance = {0}", 
            account.Balance);

        account.Deposit(100.0d);

        Console.WriteLine(
            "After depositing 100, Balance = {0}", 
            account.Balance);

        account.Withdraw(50.0d);

        Console.WriteLine(
            "After withdrawing 50, Balance = {0}", 
            account.Balance);

        Console.ReadLine();
    }
}

This is good code, right? Well, maybe. Enable the static checker on the project containing this small program, if you haven't done so already and build it. You'll see a warning that makes sense as soon as you read it. Can you assume that withdrawing a value of 50 from the account will be successful? Are there enough funds in the account to make that assumption? Maybe. Maybe not. You haven't checked the Balance first to know that it's safe to do that. So the warning from the static checker is apropos:

Warning about a protocol violation with the Withdraw method on the IAccount interface.

This kind of interaction with stateful classes is called a protocol. Some protocols are very simple like this one: you must check the Balance property before attempting to perform a withdrawal. Code Contracts can figure out many simple protocols from the way that preconditions are written. The precondition in the AccountContracts buddy class that requires the amount of the withdrawal to be less than or equal to the Balance property lets the Code Contracts static checker to know about the simple check that must be performed by a caller prior to making a withdrawal. In essence, that precondition ties the action of the Withdraw method to the value of the Balance property. And thus a protocol is established. I really love this capability of Microsoft Code Contracts. Writing good preconditions is not just a good way to document your code. It can lead to better coding practices overall.

Other more complex protocols can be implemented using Code Contracts, too. The sample entitled ApiProtocols that installs with Microsoft Code Contracts shows two interesting examples of protocols:

  1. One concerning the requirement to call the HasValue property before attempting to read the Value property on a nullable type
  2. Another concerning a class that implements a multi-state state machine for computing a result in several ordered steps.

The solver in the static checker can do an amazing job of figuring out what state the state machine of a class will be in by observing code that uses the class. With the careful management of protocol information within a class, never again must you give a complex, stateful object to a novice developer on your team and wonder if they've wired up everything that the protocol requires correctly. We can fix the code shown above and eliminate the warning by adding one small test before the withdrawal:

if (account.Balance >= 50.0d)
    account.Withdraw(50.0d);

Making this simple change will satisfy the static checker that all assertions in the code hold. Build it and see. Now that we have all the pieces in place, I'll reinforce what you've learned with a graphic that illustrates all the moving parts in defining code contracts on an interface:

A diagram that shows the relationships between the interface, the buddy class that implements the contracts on it and the working implementations of the interface.

Click on the image to see a larger version of it. This graphic depicts the IAccount interface that's marked with the ContractClass attribute pointing forward to the buddy class called AccountContracts which implements the code contracts for the IAccount interface. The buddy class is marked with a different attribute called ContractClassFor which points backward to the interface type for which it implements contracts. The AccountContracts class isn't meant to be instantiated. It's just a container for the code contracts for the IAccount interface. The AccountContracts class is even marked as abstract, a clear indicator that it cannot be instantiated. Lastly, the Account classes, e.g. SimpleAccount and others, implement IAccount normally. But through the magic of the Microsoft Code Contracts static checker and the runtime rewriter, the contracts defined in the buddy class will be harvested to be evaluated and implemented within them as necessary.

In closing, let me address the concept of code contracts on the abstract methods of an abstract class. The process of defining code contracts on an abstract class is very similar to doing so for an interface. You use the same attributes, ContractClass and ContractClassFor, to define the two-way relationship between the abstract class being documented and the abstract class that will serve as the container for the code contracts. The key difference is that the buddy class in which you define the contracts must derive from the abstract class being documented instead of implementing an interface. Because of this nuance, you must then use the override keyword in C# within the buddy class implementation for each method that you're providing contracts for. Other than that, implementing contracts on an abstract class feels very similar to dong so for an interface. That's all for now. Enjoy.

This blog post is part of a series concerning Microsoft Code Contracts. For a complete series directory, please refer to the following list. Articles without a link will be published as they become available.