Introducing the LinFu, Part V: LinFu.DesignByContract2 – Adding Transparent Design by Contract Features to Any .NET Language

• Download LinFu.DesignByContract2 demo - 158 KB
• Download LinFu binaries - 56 KB
• Download LinFu source - 204 KB

Note: To access the latest sources for the LinFu Framework directly from the SVN, click here.

Introduction

In this final installment of the series, I'll discuss some of the concepts behind Design by Contract, and I'll show you how you can use LinFu’s DesignByContract2 libraries to transparently add the same features to your application (such as precondition, postcondition, and invariant checking), regardless of whatever .NET programming language you use (including VB.NET).

Another note: If you're wondering what the entire LinFu Framework is about, click here.

Background

After discovering the Eiffel programming language a few years ago (and subsequently, Eiffel.NET), I wondered if it would be possible to implement the same type of error checking that the Eiffel programming language employs without having to switch to the Eiffel programming language itself. In the process, I ended up studying the intricacies of Reflection.Emit, and I enjoyed it so much that I wrote the original LinFu.DynamicProxy library. As it turned out, I discovered that dynamic proxies were the perfect tools to use for implementing Design by Contract, and thus, the original LinFu.DesignByContract project was born.

Design by Contract 101

Disclaimer: Since there’s already comprehensive methodology that surrounds Design by Contract, I'm only going to focus on explaining the aspects of DbC that pertain to this article, so if you're looking for a more in-depth explanation, I strongly suggest looking at some of the other articles on DbC, such as this one. Otherwise, read on and I'll explain DbC in the simplest way I possibly can.

A Simple Explanation

At its very essence, Design by Contract is a way to find bugs by applying running constraints on a program’s behavior. These constraints are runtime assertions that continually check if the program is running in a valid state. If any of those predefined constraints are violated, it means that one or more bugs exist in the program.

If you've ever used the Debug.Assert() method in the System.Diagnostics namespace, this should be immediately familiar to you. At first, Design by Contract might seem like another name for classic defensive programming techniques, but comparing DbC to defensive programming is like comparing brain surgery using a scalpel versus brain surgery using a broadsword. DbC adds a layer of precision to bug slaying, while standard defensive programming techniques (in comparison) can potentially leave a bloody mess and inadvertently kill the patient (or program, in this case). Design by Contract, in contrast, helps determine not only if these bugs exist, it also identifies where those same bugs are located, and why they occur. In general, DbC identifies three points of failure in all methods of a given class. These points are:

The Rule of Three

Every given method defined in a class (no matter how simple, or complex) has three points where the method can fail. First, a method can fail if it has an invalid input state (such as a null object reference). Secondly, a method can fail if it returns an invalid output state (such as returning a negative balance for a bank account). Lastly, a method can also fail if it leaves its host object in an invalid state (such as having a negative IList<T>.Count property after calling a faulty implementation of IList<T>.Remove() on an empty collection). Given these points of failure, how then does DbC determine the source of a program error?

Identifying the Culprit

The theory behind Design by Contract states that if a method has an invalid input state, then generally, the source of the bug is the calling method and the invalid parameters that were passed to the target method. If the target method itself returns an invalid output state, then the source of the bug is the target method itself. If, on the other hand, the target method has both valid input parameters and a valid output (presumably a return value), yet still leaves the object in an invalid state before or after the method call, then the source of the bug still lies in the target method itself.

Input and Output States?

You're probably wondering why I simply didn't call a method’s input state its parameters, or call its output state its return value. I call it an input state because there might be times when a method doesn't take parameters, yet there might be some conditions that must hold true about the internal state of its host object before the method can be called. For example, I suppose that I have a PayrollAccount class that has a PayWages() method:

public class PayrollAccount
{
   public int Balance
   {
     get { return _balance;  }
     set { _balance = value; }
   }
   public void PayWages()
   {
     // Disburse the wages here..
   }
}

In this example, the actual input state is the PayrollAccount’s Balance property. The PayrollAccount class can only pay wages if there is a positive balance in the account itself. Conversely, I call it an output state because there might be times where the method does not have a return value per se, yet there are some conditions that have to be true once the PayWages() method is finished executing. In the same example above, we want to make sure that the amount deducted from the balance matches the amount of wages paid.

Catching the Bugs

The basic theory behind Design by Contract states that one can identify the source of a bug in any given program by placing assertions at any (or preferably all) of these three failure points. In order to catch those bugs, all you have to do is cause the program to fail if any one of those assertions fails.

It’s also possible to have a method maintain a valid input and output state, yet leave its host object in a completely invalid state. Since a class’ methods typically operate on a common internal state (such as private member variables), it’s fair to assume that any one of these methods can corrupt the internal state of a given object. So, aside from having a valid method input and output, how does DbC ensure that all methods work in tandem to maintain a valid internal object state?

Seeing Double

At first, it might seem like checking for a valid return value after a method call and separately verifying the object state before and after the method call might be redundant, given that they appear to perform the same function. However, an object’s overall state needs to be verified before and after every method call (apart from any checks placed on that method), and that effectively guarantees that the object will always be in a valid state before and after any method is executed. Using this technique makes it incredibly simple to identify bugs, given that identifying the source of any bug is simply a matter of identifying the assertion type that failed, and locating the method that caused that failure. With this in mind, the theory of DbC describes the following types of assertions that should exist within a program, which brings us to the next section.

Assertions Galore

According to DbC, since there are three points of failure in any given class, it naturally implies that there are three equivalent types of assertions that check failures at those given points. These assertions types are: preconditions, postconditions, and invariants. Preconditions are assertions that identify invalid input (or an invalid input state), and postconditions are assertions that identify an invalid output state (or an invalid return value). Invariants, in contrast, are object-level assertions that are checked before a method is called (and thus, before its preconditions are called), and the same invariants are also called after the method is executed and only invoked after the last method postcondition executes. When all three of these assertion types are applied to a given type, they collectively form what is known as a contract.

Up to this point, however, the mechanism that I've just described for DbC only accounts for contracts for types that have a flat class hierarchy (that is, types that directly inherit from System.Object)—but what would happen to a type’s contract if, for example, that particular type has a base class with its own contract defined? How then, according to DbC, should these contracts be combined?

Inherited Contracts

Generally, the collective behavior of combined contracts depends on the types of assertions being combined. Let’s suppose, for example, that I have a base class named ConnectionManager that had a Open() method defined with a NotNull parameter precondition that checks if the connection is null, and a postcondition called EnsureConnected:

public class ConnectionManager
{
   private int  _openConnections;
   public int OpenConections { get { return _openConnections; } }
   [EnsureConnected]
   public virtual void Open([NotNull] IDbConnection connection)
   {
      // Do something useful here...
      _openConnections++;
   }
}

The first question you might be asking is exactly how those custom attributes are defined as contract assertions (don't worry--we'll get to that part later). For now, let’s assume that the embedded attributes are equivalent to writing the following code:

public class ConnectionManager
{
   private int  _openConnections;
   public int OpenConections { get { return _openConnections; } }
   public virtual void Open(IDbConnection connection)
   {
      // The [NotNull] implementation is equivalent to:
      Debug.Assert(connection != null, "The connection cannot be null!");

      // Do something useful here...

      // The [EnsureConnected] implementation is equivalent to:
      Debug.Assert(connection.State == ConnectionState.Open,
            "The connection should be open!");
   }
}

So far, the implementation of ConnectionManager is very straightforward—but suppose I were to implement a derived class named EnhancedConnectionManager with an additional precondition named ConnectionStringNotEmpty, and a postcondition named EnsureConnectionCountIncremented:

public class EnhancedConnectionManager : ConnectionManager
{
   [EnsureConnectionCountIncremented]
   public override void Open([ConnectionStringNotEmpty] IDbConnection connection)
   {
      // [ConnectionStringNotEmpty] is equivalent to:
      // Debug.Assert(!string.IsNullOrEmpty(connection.ConnectionString),
      // "There must be a valid connection string!");

      // Do something useful here...

      // [EnsureConnectionCountIncremented] is equivalent to:
      // Debug.Assert(this.OpenConnections == OpenConnections + 1,
      // "The connection count should have been incremented!");
   }
}

As you can see from the example above, the EnhancedConnectionManager has it own contract in addition to the contract that it must inherit from the ConnectionManager base class. The theory of DbC states that inherited contracts weaken the preconditions inherited from their base classes, and any postconditions (or invariants) added to the derived classes must be strengthened as well.

Combining Contracts

In layman’s terms, this simply means two things. First, it means that the more inheritance levels you impose upon a method contract, the more lenient you have to be when checking method input using preconditions. Secondly, when you add a postcondition to a derived method implementation, it means that the derived method must not only fulfill the postcondition requirements defined in its own contract—it must also fulfill the method postconditions defined on its parents. According to DbC, the actual combined contract of the EnhancedConnectionManager would look something similar to the following:

public class EnhancedConnectionManager : ConnectionManager
{
   public override void Open([ConnectionStringNotEmpty] IDbConnection connection)
   {
      // Combine the preconditions (Logically OR them together)
      // Debug.Assert(!string.IsNullOrEmpty(connection.ConnectionString) ||
      // connection != null);

      // Do something useful here...

      // Combine the postconditions (Logically AND them together)
      // Debug.Assert(this.OpenConnections == OpenConnections + 1 &&
      // connection.State == ConnectionState.Open);
   }
}

Puny Preconditions?

At first glance, it might seem a bit counterintuitive to weaken the postconditions for every level of contract inheritance in the class hierarchy. After all, there doesn't seem to be a fair tradeoff if a single true precondition on one inheritance level can effectively nullify the preconditions defined on previous (or subsequent) method implementations defined in the hierarchy.

In reality, however, for every precondition you define on each inheritance level, there’s a good chance that you'll probably define a corresponding postcondition. While the additional weakened precondition makes it easier to allow for invalid input, its matching postcondition makes it even more difficult for the overridden method implementation to fail. The true tradeoff, in essence, is that the derived method implementations are given more freedom for invalid input at the expense of more responsibility in fulfilling their postconditions.

Comparing the old with the New

The original implementation of the Eiffel language (and thus, Design by Contract itself) had a language feature that allowed postconditions to compare the state of a given object (read: its properties) before and after a given method is executed using something called the old operator. This effectively gave Eiffel language users the ability to compare the current state of an object to a snapshot of its previous state before the previous method was called. In other words, this can be useful if you want to verify a change in the object’s old state using a postcondition.

Inherited Invariants

Inherited invariants in a derived class (much like method postconditions) are simply combined with its parent contract’s invariants using the logical AND operator, and just as with standard invariants, the combined set of invariants are executed before and after each method is called. Fortunately, this part is fairly self-explanatory, so let’s move on to the next section.

Failing Hard

According to DbC, any failure from any one of the three assertion types should cause the entire program to come crashing to a halt. This makes bugs much easier to find since any assertion error will cause the system to come to a standstill until the source of the bug is fixed by the developer. The failure message in a precondition, postcondition, or invariant assertion should tell the user which method caused the failure in addition to telling why the method failed in the first place. Causing the program to grind to a halt immediately causes the bug to show itself. In short, the process of Failing Hard makes any bug immediately stand out from the rest of the code, and needless to say, that can save quite a lot of debugging time.

On to the Playing Field

Now that we a good sense of what kind of behavior one should expect from an implementation of DbC, I'll show you how LinFu fits into the picture and implements all of the features that I just mentioned.

Design by Contract, with LinFu

LinFu has full support for all of the language features that one would expect out of a Design by Contract library. It is language independent, meaning that you can use it in languages where no implementations of DbC exist, such as VB.NET. It has full support for inherited (as well as standard) preconditions, postconditions, and invariants, and LinFu’s DesignByContract2 libraries allow developers to generate transparent contracts at both runtime and compile time. Each one of these contracts can be passed seamlessly between multiple .NET languages regardless of whether or not those languages natively support Design by Contract.

Using LinFu, contracts themselves are first class System.Objects, and as you'll see in the rest of this article, the amount of flexibility that this library affords can be quite staggering. So without further ado, let’s jump straight into the code!

Features and Usage

Gift-Wrapped in Dynamic Proxies

Despite LinFu.DesignByContract2’s seemingly inherent complexity, the core implementation of LinFu’s own DbC Framework is nothing but a contract verifier wrapped around an object instance. Every time a call is intercepted using the contract verifier, it determines whether or not there are any preconditions, postconditions, or invariants that need to be executed before the actual method implementation is called and executes those assertions. For example, suppose that I wanted to apply a particular contract to an instance of IDbConnection:

AdHocContract someContract = new AdHocContract();

// (Add some preconditions, postconditions, or invariants here)
IDbConnection someConnection = new SqlConnection();

// Use the ContractChecker to bind the contract to a proxy instance
// and wrap it around the target connection
ProxyFactory factory = new ProxyFactory();
ContractChecker checker = new ContractChecker(someContract);
checker.Target = someConnection;

IDbConnection wrappedConnection = factory.CreateProxy<IDbConnection>(checker);

// Do something useful with the wrappedConnection here...
wrappedConnection.Open();

The ContractChecker class will scan the AdHocContract instance for any preconditions and postconditions associated with the IDbConnection.Open() method. Any contract assertions defined on that method will automatically be injected and wrapped around the IDbConnection.Open() implementation, using the someContract variable.

Transparently Bound

Using proxies allows the client code to use contracts without ever knowing about the existence of the DbC assertions. Using LinFu.DesignByContract2 comes down to answering a few fundamental design questions. First, we need to determine which preconditions and postconditions need to be assigned to each method. Second, we need to determine which invariants should be applied to the target object instance, and lastly, we need to somehow tie the new contract to the proxy instance. In the following sections, I'll show you some of the different techniques that LinFu uses to generate contracts, and I'll also show you some of the basic methods for applying those contracts to nearly any object instance.

LinFu Contracts

LinFu makes it possible to write a contract in one language (such as C#) and have that same contract consumed in a completely different language (such as VB.NET). No matter which language you decide to use, contracts in LinFu implement at least one of the following interfaces:

public interface ITypeContract
{
    IList<IInvariant> Invariants { get; }
}
public interface IMethodContract
{
    IList<IPrecondition> Preconditions { get; }
    IList<IPostcondition> Postconditions { get; }
}

public interface IContractProvider
{
    ITypeContract GetTypeContract(Type targetType);
    IMethodContract GetMethodContract(Type targetType, InvocationInfo info);
}

As you can see from the example above, there are two types of contracts that can be applied to any given type. The IMethodContract-derived instances keep track of which preconditions and postconditions should be assigned to a particular method, while the ITypeContract implementations hold invariants that need to be applied to a particular target type. The IContractProvider interface, in turn, allows its derived implementations to determine which ITypeContracts to apply to each target type using the GetTypeContract() method. In addition, every time a method is called, the contract verifier calls the GetMethodContract() method to determine which preconditions and postconditions it should apply to the current method. Effectively, a contract can only be formed when all of the IMethodContract and ITypeContract instances combine into a single IContractProvider instance. A contract, of course, is nothing without its preconditions, postconditions, and invariants. Therefore, we need to be able to define our own set of custom contract assertions, and that’s what we're going to examine in the next section.

The Anatomy of an Assertion

The three assertion types are defined as:

// Note: For now, ignore the IContractCheck and IMethodContractCheck
// interfaces--we'll get into that later in the article.
public interface IInvariant : IContractCheck
{
    bool Check(object target, InvocationInfo info, InvariantState callState);
    void ShowError(TextWriter output, object target, InvocationInfo info, 
        InvariantState callState);
}
public interface IPrecondition : IMethodContractCheck
{
    bool Check(object target, InvocationInfo info);
    void ShowError(TextWriter output, object target, InvocationInfo info);
}
public interface IPostcondition : IMethodContractCheck
{
    void BeforeMethodCall(object target, InvocationInfo info);
    bool Check(object target, InvocationInfo info, object returnValue);
    void ShowError(TextWriter output, object target, InvocationInfo info, 
        object returnValue);
}

The first thing that you might have noticed is that each assertion type has its own custom implementation of the Check() and ShowError() methods. Despite the differences in signatures, both sets of methods generally perform the same set of functions across all three assertion types. When a contract assertion is verified, the verifier calls the Check() method to determine if the assertion succeeded. If the Check() fails, then the verifier calls the ShowError() method, giving the assertion the chance to explain the error with its own custom error message. The verifier will then throw a DesignByContractException using the custom error message, and that should allow you to fix whatever error (or set of errors) that the target method has caused.

An Oddity

For the most part, the three assertion interfaces are fairly self-explanatory, except for the IPostcondition interface. If the postcondition is supposed to be executed after a method is called, then why does the IPostcondition interface have a method called BeforeMethodCall()?

The Peeking Postcondition

As I mentioned earlier in this article, some postconditions need to be able to compare the current state of a given object to its previous state. For example, suppose that I had a BankAccount class defined with a Deposit() method, in VB.NET:

Public Class BankAccount
    Private accountBalance As Integer
    Public Overridable Property Balance() As Integer
        Get
            Return accountBalance
        End Get
        Set(ByVal value As Integer)
            accountBalance = value
        End Set
    End Property
    Public Overridable Sub Deposit(ByVal amount As Integer)
        accountBalance += amount
    End Sub
End Class

Using that example, I want to ensure that the account balance is updated every time I make a deposit into that BankAccount instance. The problem is that VB.NET currently doesn't have anything that resembles Eiffel’s old operator. This is where the IPostcondition.BeforeMethodCall() method comes in handy:

Imports System.IO
Imports LinFu.DynamicProxy
Imports LinFu.DesignByContract2.Core

<AttributeUsage(AttributeTargets.All)> _
Public Class EnsureBalanceReflectsDepositAmountAttribute
    Inherits Attribute
    Implements IPostcondition

    Private oldBalance As Integer
    Private expectedBalance As Integer
    Public Sub BeforeMethodCall(ByVal target As Object, ByVal info As  InvocationInfo) _
        Implements IPostcondition.BeforeMethodCall
        If target = Nothing Then Return
 If Not (TypeOf target Is BankAccount) Then Return

        'Save the old balance
        Dim account As BankAccount = CType(target, BankAccount)
        oldBalance = account.Balance

    End Sub

    Public Function Check(ByVal target As Object, ByVal info As InvocationInfo, _
        ByVal returnValue As Object) As Boolean _
        Implements IPostcondition.Check

        'Compare the new balance with the old balance
        Dim account As BankAccount = CType(target, BankAccount)
        Dim newBalance As Integer = account.Balance

        'Determine the deposit amount and use it calculate the expected balance
        Dim depositAmount As Integer = CType(info.Arguments(0), Integer)

        'The expected balance should be the original amount + the new deposit amount
        expectedBalance = oldBalance + depositAmount

        'Perform the actual comparison
        Return account.Balance = expectedBalance
    End Function

    Public Sub ShowError(ByVal output As TextWriter, ByVal target As Object, _
        ByVal info As InvocationInfo, _
                  ByVal returnValue As Object) Implements IPostcondition.ShowError
        output.WriteLine("Deposit Failed! The expected balance should have been '{0}'", _
            expectedBalance)
    End Sub

    Public Function AppliesTo(ByVal target As Object, ByVal info As InvocationInfo) _
        As Boolean _
        Implements IContractCheck.AppliesTo
        'Only BankAccount instances should be checked
        Return TypeOf target Is BankAccount
    End Function

    Public Sub [Catch](ByVal ex As Exception) Implements IContractCheck.[Catch]
        'Ignore the error
    End Sub
End Class

As you can see in this example IPostcondition implementation, the EnsureBalanceReflectsDepositAmountAttribute postcondition uses the BeforeMethodCall() method to save the old account balance right before the actual Deposit() method is called. Once the contract verifier calls its Check() method, the postcondition takes the old balance and compares the new balance with the expected balance. If the Check()fails, then the verifier will use the postcondition’s implementation of the ShowError() method to display the contract error message. So far, everything seems pretty straightforward—but what does the AppliesTo() method do?

An Assertion for Every Occasion

As you probably might have noticed from previous examples, all three of the assertion types inherit from the IContractCheck interface. This interface is simply defined as:

public interface IContractCheck
{
    bool AppliesTo(object target, InvocationInfo info);
    void Catch(Exception ex);
} 

Simply put, the AppliesTo() method determines whether or not each Check() method should be called, given the current context. This method is typically used to determine whether or not a target instance matches the intended type. In the previous example, I used the sample IPostcondition.AppliesTo() method implementation to determine whether or not the target object was actually an instance of the BankAccount class. If the target object was not a BankAccount instance, the verifier would have simply skipped that postcondition, and the Check() method would altogether have been completely ignored.

The Catch

The next thing that you might be wondering about is the Catch() method. At first, it might seem like it doesn't make sense to have that method on the IContractCheck interface, given that one can simply catch any exceptions thrown by an errant precondition, postcondition, or invariant. The problem with injecting code using LinFu.DynamicProxy is that tracking down the source of an exception can be difficult if the application knows nothing about the existence of the injected code. If the injected code throws an exception, how is the program supposed to deal with an error of which it has no knowledge about?

System.Exception, Handle Thyself

LinFu.DesignByContract2 addresses this problem by reflecting any exceptions thrown by an assertion back to the assertion itself. This makes it relatively simple to isolate the injected contract assertions from the actual program. It also makes bugs in the contract code easier to trace since the onus is on each contract assertion to handle their own exceptions.

Dynamic Contracts

If you need something more lightweight than implementing your own versions of the IPrecondition, IPostcondition, and IInvariant interfaces, LinFu.DesignByContract2 also allows you to dynamically create contracts at runtime.

Creating Preconditions

For example, suppose that I wanted to create a precondition on an IDbConnection instance that checks if it has a non-empty connection string before calling the Open() method. Here’s how to do it in C# 3.0:

AdHocContract contract = new AdHocContract();
IDbConnection connection = new SqlConnection();

// Create the precondition
Require.On(contract)
.ForMethodWith(m => m.Name == "Open")
.That<IDbConnection>(c => !string.IsNullOrEmpty(c.ConnectionString))
       .OtherwisePrint("This connection must have a connection string 
        before call the Open() method");

ProxyFactory factory = new ProxyFactory();
ContractChecker checker = new ContractChecker(contract);
checker.Target = connection;

// Bind the contract to the proxy
IDbConnection wrappedConnection = factory.CreateProxy<IDbConnection>(checker);

// This call will fail
wrappedConnection.Open();

As you can see from the example above, the Require statement dynamically does all the work of creating a precondition for you. The code pretty much speaks for itself.

Creating Postconditions

If you need to add a postcondition that verifies that the connection has been opened, then all you have to do is add the following lines of code to the above example:

Ensure.On(contract)
.ForMethodWith(m => m.Name == "Open")
.That<IDbConnection>(c => c.State == ConnectionState.Open)
.OtherwisePrint("The connection failed to open!");

Creating Invariants

If, on the other hand, you wanted to add an invariant that made sure that the same IDbConnection instance always has a connection string, then all you would have to do is add the following code:

Invariant.On(contract)
.WhereTypeIs(t => typeof(IDbConnection).IsAssignableFrom(t))
.IsAlwaysTrue<IDbConnection>(c => !string.IsNullOrEmpty(c.ConnectionString))
.OtherwisePrint("The connection string cannot be empty!"); 

Or if, for some reason, you wanted to invert the logic in the example above and make sure that the IDbConnection instance never has a non-empty or non-null connection string, then you can also write the code like this:

// The differences are highlighted in bold
Invariant.On(contract)
.WhereTypeIs(t => typeof(IDbConnection).IsAssignableFrom(t))
.IsAlwaysFalse<IDbConnection>(c => string.IsNullOrEmpty(c.ConnectionString))
.OtherwisePrint("The connection string cannot be empty!"); 

One could also create an invariant that says that having an open IDbConnection instance implies that the same connection string cannot be empty:

// The differences are highlighted in bold
Invariant.On(contract)
.WhereTypeIs(t => typeof(IDbConnection).IsAssignableFrom(t))
.HavingCondition<IDbConnection>(c => c.State == ConnectionState.Open)
.ImpliesThat(cn => !string.IsNullOrEmpty(cn.ConnectionString))
.OtherwisePrint("You have an open connection with a blank connection string? 
    How is this possible?");

Unlike in Eiffel (or even in Spec#), all of the contracts seen in the above examples are created at runtime, not compile time. These contracts themselves don't even need to be written using the same .NET language. I'll let you ponder that for a moment. Once you're done pondering all of its possible uses, I'll show you how to create even more powerful contracts in the next section.

Attribute-Based Contracts

If you need something more robust rather than lightweight, LinFu.DesignByContract2 supports embedding contract assertions directly into your code using your own custom attributes. If you recall from the EnsureBalanceReflectsDepositAmountAttributeexample from the beginning of this article, our goal was to ensure that the BankAccount class reflected the correct Balance amount every time the Deposit() method is called. As you probably noticed, the EnsureBalanceReflectsDepositAmountAttribute class is both an attribute and an implementation of IPostcondition:

Imports System.IO
Imports LinFu.DynamicProxy
Imports LinFu.DesignByContract2.Core

<AttributeUsage(AttributeTargets.All)> _
Public Class EnsureBalanceReflectsDepositAmountAttribute
    Inherits Attribute
    Implements IPostcondition

    ' Methods omitted for brevity
End Class

If you were to apply the same attribute assertion to the BankAccount class, here is how its new definition would look like:

Public Class BankAccount
    Private accountBalance As Integer
    Public Overridable Property Balance() As Integer
        Get
            Return accountBalance
        End Get
        Set(ByVal value As Integer)
            accountBalance = value
        End Set
    End Property
   <EnsureBalanceReflectsDepositAmount()> _
    Public Overridable Sub Deposit(ByVal amount As Integer)
        accountBalance += amount
    End Sub
End Class

It’s simple, elegant, and yet at this point, it’s still fairly useless. There has to be a way one can take an embedded precondition, postcondition, or invariant attribute and combine all of them into one cohesive contract. That’s where the AttributeContractProvider comes to the rescue. The AttributeContractProvider class will take all of the assertions embedded on the BankAccount class and convert it into a running contract, as shown in the following example:

ProxyFactory factory = new ProxyFactory();
ContractChecker checker = new ContractChecker(new AttributeContractProvider());
checker.Target = new BankAccount();

BankAccount wrappedAccount = factory.CreateProxy<BankAccount>(checker);

// Make a deposit
wrappedAccount.Deposit(100);

With the AttributeContractProvider, there’s no need to manually generate a contract by hand. All you need to do is to define your own custom precondition, postcondition, or invariant attribute that implements one of the three assertion interfaces. Once that attribute has been defined and embedded in your code, the contract will automatically be generated for you.

Custom Assertion Attributes

Now that you have a general idea of what the AttributeContractProvider does, we need to get a sense of how to create our own custom assertion attributes, as well as learn how to declare them on a given type. As an example, suppose that we have the following model, in pseudo-code:

A bank account has an owner, which is a person.
A person has a name, and an age.
You can do these things with a bank account: deposit, withdraw, and get its balance.

The bank account will have the following restrictions:

1) An account will always have one and only one person (Invariant)
2) Accounts with persons under the age of 18 cannot withdraw any money. (Precondition)
3) No account will ever have a negative balance. (Invariant)
4) Bank accounts should never allow negative amounts for withdrawals or deposits. 
    (Parameter Precondition)
5) The new balance after a deposit or a withdrawal should reflect the amount of 
    the transaction (Postcondition)

The model in the above example has all the elements needed for a full-fledged contract. The only thing that we need to do is expand the definition of the BankAccount class to include all of the details mentioned in the model above. To make things interesting, we're going to write the new model in C#, and we'll have the client code written in VB.NET. Let’s start with the definition of the BankAccount class:

// Requirement #1: An account will always have one and only one person
[type: ShouldAlwaysHaveAnOwner]

// Requirement #4: Bank accounts should never allow negative amounts for 
// withdrawals or deposits
[type: BalanceIsAlwaysNonNegative]
public class BankAccount
{
    private int _balance;
    private Person _owner;
    public BankAccount(int balance)
    {
        _balance = balance;
    }
    public virtual Person Owner
    {
        get { return _owner;  }
        set { _owner = value; }
    }
    public virtual int Balance
    {
        // Requirement #3: No account will ever have a negative balance.
        [return:NonNegative] get { return _balance; }
    }

    // Requirement #5a: The new balance after a deposit or a withdrawal 
    // should reflect the amount of the transaction.
    [EnsureBalanceReflectsDepositAmount]

    // Requirement #4: Bank accounts should never allow negative amounts for 
    // withdrawals or deposits.
    public virtual void Deposit([NonNegative] int amount)
    {
        _balance += amount;
    }

    // Requirement #2: Accounts with persons under the age of 18 
    // cannot withdraw any money.
    [MinorsCannotWithdrawAnyMoney]

    // Requirement #5b: The new balance after a deposit or a withdrawal 
    // should reflect the amount of the transaction.
    [EnsureBalanceReflectsWithdrawalAmount]
    public virtual void Withdraw([NonNegative] int amount)
    {
        // Notice that I'm not checking for a negative
        // balance on the postcondition--this is an intentional error
        _balance -= amount;

        // The non-negative balance invariant should catch
        // the error
    }
}

The Person class, in turn, is defined as:

public class Person
{
    private int _age;
    private string _name;

    public Person(string name, int age)
    {
        _age = age;
        _name = name;
    }
    public virtual string Name
    {
       get { return _name;  }
       set { _name = value; }
    }
    public virtual int Age
    {
        [return: NonNegative] get { return _age;  }
        set { _age = value; }
    }
}

As you can see, having assertion attributes directly embedded in the code makes it much easier to understand. More importantly, it isolates the details from the developer about how the assertion is made, and how it works. To create your own custom assertions, you'll need to follow the general set of guidelines for each assertion type:

Precondition Attributes

If you need to create your own custom precondition attribute, then all you need to do is implement the IPrecondition interface in your attribute definition, and make sure that the attribute can be applied to a method. For example, this was the definition used by the MinorsCannotWithdrawAnyMoneyAttribute precondition:

[AttributeUsage(AttributeTargets.Method)]
public class MinorsCannotWithdrawAnyMoneyAttribute : Attribute, IPrecondition
{
    // ...
}

Once you have defined your custom precondition attribute and declared it on a given method, the AttributeContractProvider instance will detect any IPrecondition attribute instances attached to that method at runtime, and add it as part of the method contract. On the other hand, if you look at the following attribute declarations defined on the Deposit() and Withdraw() methods of the BankAccount class:

public virtual void Deposit([NonNegative] int amount)
{
    // ...
}

public virtual void Withdraw([NonNegative] int amount)
{
    // ...
}

The NonNegativeAttribute declaration defined on the amount parameters of both methods is a parameter precondition attribute, which is what we'll examine next.

Parameter Precondition Attributes

Parameter precondition attributes are simply custom attributes that implement the IParameterPrecondition interface, which is defined as:

public interface IParameterPrecondition : IMethodContractCheck
{
    bool Check(InvocationInfo info, ParameterInfo parameter, object argValue);
    void ShowErrorMessage(TextWriter stdOut, InvocationInfo info, ParameterInfo parameter,
        object argValue);
}

Like any other contract assertion attribute, the NonNegativeAttribute must implement the correct assertion interface, and define itself as an attribute:

[AttributeUsage(AttributeTargets.Parameter | AttributeTargets.ReturnValue)]
public class NonNegativeAttribute : Attribute, IParameterPrecondition, IPostcondition
{
    // ...
}

When the AttributeContractProvider detects this attribute attached to a parameter, it will treat it as a parameter precondition, and apply it as such. What’s interesting about the NonNegativeAttribute is that it is both a parameter precondition and a postcondition. If that’s the case, then how does the AttributeContractProvider class determine whether to use it as a precondition, or a postcondition?

Postcondition Attributes

The AttributeContractProviderclass determines how to use the NonNegativeAttribute instance based on where the attribute is placed. For example, you probably might have noticed that the same NonNegativeAttribute was declared on the return value of a property in one of the previous examples:

public virtual int Age
{
    [return: NonNegative] get { return _age;  }
    set { _age = value; }
}

When a postcondition attribute is declared on a method or declared on a return value (and that attribute implements the IPostconditioninterface), it will then be automatically used as a postcondition by the AttributeContractProvider. The NonNegativeAttribute is no exception. Since it is also an implementation of IPostcondition, it will be used as a postcondition since it is attached to the return value of the Age property, and it implements the IPostconditioninterface.

Invariant Attributes

Like the previous examples, the process for defining your own custom invariant attributes is fairly straightforward. First, you have to make sure that the attribute can only be used on type declarations. Secondly, the attribute must implement the IInvariant interface. In the examples above, our goal was to make sure that a BankAccount class never has a negative balance. With that in mind, let’s look at how the BalanceIsAlwaysNonNegativeAttribute invariant is defined:

[AttributeUsage(AttributeTargets.Interface | AttributeTargets.Class)]
public class BalanceIsAlwaysNonNegativeAttribute : Attribute, IInvariant
{
    #region IInvariant Members

    public bool Check(object target, InvocationInfo info, InvariantState callState)
    {
        BankAccount account = (BankAccount) target;
        return account.Balance >= 0;
    }

    public void ShowError(System.IO.TextWriter output, object target, 
        InvocationInfo info, InvariantState callState)
    {
        output.WriteLine("You cannot have a negative balance!");
    }

    #endregion

    #region IContractCheck Members

    public bool AppliesTo(object target, InvocationInfo info)
    {
        return target != null && target is BankAccount;
    }

    public void Catch(Exception ex)
    {
        // Do nothing
    }

    #endregion
}

Since the IInvariant interface is similar to other contract assertion interfaces, most of the code above should seem pretty familiar. The only significant part of this example that stands out is the use of the InvariantState enum. The InvariantState enum can be useful if you want to know when the invariant is currently being called, whether it is before or after the actual method call itself. It is simply defined as:

public enum InvariantState
{
    BeforeMethodCall = 1,
    AfterMethodCall = 2
}

As you can see, enum itself is very self-explanatory. Other than that, the rest of the IInvariant implementation is boilerplate code.

Inferred Contracts

If you prefer to separate your actual implementation code from the contract declarations, LinFu.DesignByContract2 supports the concept of “Inferred Contracts”. This means that you can declare all your contract assertions on an external interface type, and at runtime, LinFu.DesignByContract2 will take all of those assertions and merge them into your class implementations as if they were an actual part of the implementation code in the first place. This can be very useful if you have a situation where you don't have access to the original source code but you still want to be able to extend a particular type with a separate contract.

Externally Defined

For example, let’s suppose that I wanted to define an IContractForBankAccount interface that had all the contract assertions for the BankAccount class. Moreover, let’s also assume that the BankAccount class has no contracts defined on it at all. Here is what the contract interface would look like:

[ContractFor(typeof(BankAccount))]
[type: ShouldAlwaysHaveAnOwner]
[type: BalanceIsAlwaysNonNegative]
public interface IContractForBankAccount
{
    int Balance { [return: NonNegative] get; }
    [EnsureBalanceReflectsDepositAmount] void Deposit([NonNegative] int amount);

    [EnsureBalanceReflectsWithdrawalAmount,
    MinorsCannotWithdrawAnyMoney] void Withdraw([NonNegative] int amount);
}

Aside from intentionally lacking any actual implementation, the assertions declared on the IContractForBankAccount interface look identical to the same assertions declared on the BankAccount class. The next thing that we need to do is merge the contracts defined on the IContractForBankAccount interface with the actual BankAccount class itself. At the same time, it would be immensely useful if we didn't have to manually wrap every created object instance in a contract using the ProxyFactory class. This is where the Simple.IoC container comes in handy, and I'll show you how you can use it with LinFu.DesignByContract2 in the next section.

Using Inferred Contracts

Now that the contract for the BankAccount class is in place, here’s how you can use LinFu.DesignByContract2’s extensions to the Simple.IOC container to automatically wrap BankAccount instances using the least amount of code, in VB.NET:

Imports System
Imports LinFu.DesignByContract2.Injectors
Imports Simple.IoC
Imports Simple.IoC.Loaders

Module Module1
    Sub Main()
        Dim container As New SimpleContainer()
        Dim loader As New Loader(container)

        Dim directory As String = AppDomain.CurrentDomain.BaseDirectory

        ' Explicitly load the contract loader DLL
        loader.LoadDirectory(directory, _
            "LinFu.DesignByContract2.Injectors.dll")

        ' Load everything else
        loader.LoadDirectory(directory, "*.dll")

        ' Load the BankAccount contract that was written in C#
        Dim contractLoader As IContractLoader = _
            container.GetService(Of IContractLoader)()
        contractLoader.LoadDirectory(directory, "BankAccountContract.dll")

        ' Manually add a service for a BankAccount
        container.AddService(Of BankAccount)(New BankAccount())

        ' Withdraw money from an empty account, causing a PreconditionViolationException

        Dim account as BankAccount = container.GetService(Of BankAccount)()
        account.Withdraw(1000)

    End Sub

End Module

Behind the scenes, the IContractLoader instance does all the work of wrapping contracts around object instances for you. In fact, once that contract loader instance is instantiated inside the container, it will transparently wrap every newly created object instance around a contract (provided that the contract already exists, of course). By using the contract loader, an application can even dynamically add new contract implementations at runtime, all without having to recompile itself. All you have to do is copy the new contracts to a specific directory, and call the LoadDirectory() method:

Dim directory as String = "c:\YourDirectory"
Dim contractLoader As IContractLoader = _
    container.GetService(Of IContractLoader)()
contractLoader.LoadDirectory(directory, "YourNewContracts.dll")

This can be useful if you want to debug a large application (such as an ASP.NET site) without having to rebuild the entire application itself. Conceivably, one can even extend the contract loader’s abilities using a FileSystemWatcher class, but that’s an exercise I'll leave to the hands of the capable reader. Suffice to say, we have effectively run the gamut of all the possible ways LinFu.DesignByContract2 lets you create contract assertions, and next, I'll talk about some of the other important features in the following section.

Pervasive Contracts

Wrap One, Get One Free

Any return value from all methods of an object instance that is wrapped in a contract using the contract loader (provided that all of the object’s methods are marked as virtual) is also wrapped in its own separate contract. For example, you might have noticed in the previous examples above that we did nothing to wrap the Person class that was attached to the BankAccount object, and yet, there was a contract that defined the Person class. That’s because the Person instance was wrapped for free. The contract on the Person instance was defined as:

public class Person
{
    // ...
    public virtual int Age
    {
        [return: NonNegative] get { return _age;  }
        set { _age = value; }
    }
}

...and if we look at BankAccount itself, we'll also notice the Owner property:

public class BankAccount
{
    // ...
    public virtual Person Owner
    {
        get { return _owner;  }
        set { _owner = value; }
    }
}

The fact that BankAccount instance was wrapped in a contract makes its Owner property wrapped in its own Person contract as well. In addition, the wrapping process is recursive, meaning that almost every object reference returned from the Person class’ methods (except those that can't be proxied) will also be wrapped in their own contract, and so forth.

Contract Inheritance

LinFu.DesignByContract2 combines contracts together in the same way one would expect contracts to be combined in Eiffel. Inherited invariants and postconditions are logically combined using the AND operator, and inherited preconditions are successively combined and weakened using the OR operator.

Inheriting Contracts from Multiple Sources

Moreover, LinFu.DesignByContract2 supports inheriting embedded contracts from contracts defined on interfaces, and on base classes. For example, let’s suppose that I had the following contract definitions defined on a set of interfaces and base classes:

public interface IInterface1
{
   [SomePrecondition1] void DoSomething();
}
public interface IInterface2
{
   [SomePrecondition2] void DoSomething();
}
public class BaseClass : IInterface1, IInterface2
{
   public virtual void DoSomething() {}
}
public class Derived : BaseClass
{
   [SomePrecondition3] public override void DoSomething() {}
}

The AttributeContractProvider class will combine all of the assertions you see above into a single contract, using only the following code:

// Wrap the derived class in a contract
ProxyFactory factory = new ProxyFactory();
ContractChecker checker = new ContractChecker(new AttributeContractProvider());
checker.Target = new Derived();

derived = factory.CreateProxy(checker);

// Use the derived class with the contract itself
derived.DoSomething();

Alternatively, the same task can be done by the Simple.IOC container (when used with LinFu.DesignByContract2.Injectors.dll as the contract loader), using some of the examples that I mentioned earlier in this article. Nevertheless, whichever approach you decide to take, the resulting contract will be the same, and in both cases, the process for creating the actual contract is truly transparent—and that, ladies and gentlemen, is how LinFu does Design by Contract.

Points of Interest

Mixing Test Driven Development, and Design by Contract

Given that Design by Contract isn't in the mainstream at this point, it would be interesting to see how one could mix the two paradigms together. Conceivably, one could use DbC to write some of the same tests that TDD would write, however, in my own practice, TDD’s tests seem to be geared towards testing whether or not a piece of code semantically meets a particular application requirement (such as determining whether or not feature “x” works according to specification), while DbC’s assertions serve to be a pervasive sanity check that continuously checks the application for bugs as the program is running. Although the two paradigms seem to be performing the same function, in truth, it would seem that their features complement each other. Since this topic is both controversial and can be potentially cumbersome, I'll leave it as an exercise to the readers to explore on their own, in greater depth.

Sharing Your Contracts

Since contracts can be compiled as separate library files with LinFu.DesignByContract2, this opens up a whole realm of possibilities with reusable contracts. If you're interested in contributing some code to build a library of the most common contract assertions, contact me and I'll add you to the project member list. My goal for LinFu is to get the entire developer community involved, and this would be a great first step in doing so.

The DotNetRocks! Podcast

In DotNetRocks! Episode #242, Carl Franklin jokingly mentioned something about Design by Contract:

Carl Franklin: But all kidding aside. Well
anyway, we have some emails to read here. The
first is from Leon Bambrick, you might recall him
being a writer in previous versions of .NET
Rocks!

Richard Campbell: We have read an email from
him before, I am sure.

Carl Franklin: Yes, and this one says, sexy
Spec#...

Richard Campbell: Nice.

Carl Franklin: He says, "Hi, Richard and the
Seaman, great show on Spec#. I am really glad
you covered this topic as it is one of those
interesting research projects that none of us ever
have the time to look into personally. I hope that
simple, verifiable, pre and post conditions can be
included in a future version of C#. Won't that be
sweet?"
Richard Campbell:
Yes.

Carl Franklin: It will be sweet in VB too man.
Goddamn it! "Or is there something ironic about
Microsoft research, spending a lot of effort to
create not nullable reference types, while the
other teams have spent so much effort creating
nullable value types."

With those words in mind, LinFu.DesignByContract2 is dedicated to VB.NET developers out there who don't have Spec#, and it’s also dedicated to the C# programmers out there who are still waiting for Spec# itself to become a full-fledged product--this library was written just for developers like yourselves. So Carl, I'm a big fan of yours, and if you're reading this right now, you finally get your wish. Enjoy!

License

LinFu.DesignByContract2 is subject to the terms of the LGPL license, meaning that you are free to use it in your commercial applications without royalties, but if you modify the source code, you must publish it so that everyone else can benefit from those modifications. In addition, if you plan on using this in your commercial projects, contact me so that I can keep track of the list of applications that are using my library. I hope you enjoyed the series!