Code Contracts #2: Code transformation

In my first blog post about Code Contracts, I covered the origins of the project and the elementary pieces of programming by the DbC principle: pre-conditions, post-conditions and invariants. Now let’s dig a little deeper and look at more background information about how contracts on your code are evaluated…

At first, let’s look again at the example of the Deposit-method from the last blog post:

public void Deposit(int amount)
{
    Contract.Requires(amount > 0);
    Contract.Ensures(Balance == Contract.OldValue(Balance) + amount);

    Balance += amount;
}

As you can see, contracts on methods (pre- and post-conditions) are defined imperatively inside the method. But instead of this definition, in fact their behavior is declarative! Thus they are not called at runtime as it is expected through the imperative style. If you debug the method and set a breakpoint on the contract’s position, then the debugger will not break there. In truth there is a component of Code Contracts called Code Rewriter (ccrewrite), which is performing a post-compile process on the IL-code, that’s generated by the compiler. Thus, every Code Contracs definition is set to its correct location in the IL code. For example, pre-conditions are set to the beginning of a method, post-conditions to the end, just before the (every) method exit, regardless to the location, where they have been defined imperatively. A look through the .NET Reflector googles over the created assembly makes this clear, too. The reflected code of the Deposit-method looks as follows:

public void Deposit(int amount)
{
    __ContractsRuntime.Requires(amount > 0, null, "amount > 0");
    int Contract.Old(Balance) = this.Balance;
    
    this.Balance += amount;

    __ContractsRuntime.Ensures(this.Balance == (Contract.Old(Balance)
        + amount), null, "Balance == Contract.OldValue(Balance) + amount");
}

As expected, the pre-condition is evaluated at the beginning, the post-condition at the end of the method. Moreover, at the beginning of the method (after the pre-condition has been evaluated) the old value of Balance is stored into a temporary variable, thus enabling Ensures() to have access on it.

With the existing example of the Deposit-method, there are some questions that come into the programmer’s mind. For example, why are Code Contracts defined (not very intuitively) imperatively inside a method and not as attributes for the method as one would expect through their declarative nature, thus leading to code pollution? The answer is, that attributes are too limited in their expressiveness. To allow full flexibility, conditions would have to be declared as string and you would have no IDE-support (Intellisense, compiler support) any more. Furthermore, the strings would have to be parsed by Code Contracts, what’s error prone at all. If attributes in .NET (C#, VB, …) would be more expressive and allow more aspect oriented programming (AOP) features, then it would be possible to define contracts via attributation, but not until now. Ok, when not using attributes, why aren’t there additional keywords for definition of Code Contracts as in Spec#? For example, why aren’t there requires and ensures keywords that are defined between method head and body and thus making the sense much more clearer and separating contracts from core logic? Please have in mind, that keywords are language-based features! Instead, the Code Contracts library becomes an element of the .NET 4.0 CLR and thereby it covers all .NET based languages, from which it can be used consequently. It would be nice to have such keywords, but it’s not the task of the Code Contracts developer team, but of the C# (and other .NET languages) team. Perhaps we’ll see such keywords in C# 5.0? Who knows…

That’s it again for the moment. In this blog post I covered the topic of code transformation by the Code Rewriter a little bit and made some statements about the declarative nature of Code Contracts. In upcoming blog posts, I want to show you the evaluation elements (checkers) of Code Contracts and give more examples, how contracts on various code elements can be defined…