Schlagwort: post-conditions

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…

kick it on DotNetKicks.com

Code Contracts #1: Basic information

During the last days and weeks, I’ve had the chance to make my mind up on Code Contracts, validation vs. verification of code and code quality on the whole. I’ve made some examples with Code Contracts and want to start a basic blog post series here, which should give you some further information on this. Code Contracts as project are not baked, yet. Thus I don’t throw with mud about things, that will definitely work in the future. This makes no sense! I just want to share some knowledge and want to know what you think about this altogether.

„Code Contracts“ is a project from the Microsoft DevLabs (http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx) and can be downloaded and installed in a very early state at the moment. The origin of Code Contracts is the programming language Spec#, which is extending C# at aspects for definition of conditions, that have to be fulfilled by part of a programmer’s code (classes, methods, variables, …). Moreover, the „Code Contracts Library“ has been decoupled from Spec# for Code Contracts and has been modified to work with the .NET framework in general. Thus, Spec# as research project has served its time, but it’s living on with Code Contracts. The impact of Code Contracts is not to underestimate: the component is going to be an element of the .NET 4.0 class library and thus it’s making its way into all .NET based languages.

But what’s hiding behind Code Contracts? The idea is the same as in Spec#: taking your code under contract, that means setting conditions on it. The programmer then has to take care about fulfilling those conditions (contracts) with his code. This idea isn’t new at all, since it comes originally from the Eiffel programming language, which has been introduced in 1985 already. Therefore Eiffel supports the Design by Contract (DbC) principle, whereby the following aspects can be defined in the code:

  • pre-conditions: Those are declared on method level and define conditions, which have to be fulfilled at entrance of a method (that means which contracts have to be kept by the caller). Mainly, these are conditions on method parameters (e.g. prohibition of null-values).
  • post-conditions: Those are declared on method level, too and define conditions, that have to be fulfilled at exit of a method (meaning contracts, that the method’s code has to ensure). For example, one could make conditions on the return value, that callers of the method could rely on.
  • invariants: Those are definitions on class level, depicting conditions, that have to be fulfilled at exit of any method of the class. For example, one could define conditions on the value of fields or properties of the class (be not null, be positive, have a defined value range, etc.).

The following example of a method deposit for a banking account illustrates the use of pre- and post-conditions in their original language Eiffel:

deposit (amount: INTEGER) is
    require
        non_negative: amount > 0
    do
        balance := balance + amount
    ensure
        updated: balance = old balance + amount
end

Pre-conditions can be defined with require, ensure defines post-conditions, that have to be true at exit of the method. Those can also describe the value of class members as shown in this (trivial) example for the member balance. Thereby, Eiffel is checking at runtime if the contracts are fulfilled and if not it’s notifying with an error.

Just those definitions are possible with Code Contracts in .NET, too. With static methods on the newly introduced class Contracts, the programmer gets the possibility to define such contracts. The deposit method from the example above would look in .NET Code Contracts as follows:

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

    Balance += amount;
}

With Contract.Requires() one can define pre-conditions, with Contract.Ensures() post-conditions. Contract.OldValue() can be used in a post-condition and is a placeholder for the value of a variable on class level (property, field) at entrance of the method.

To use Code Contracts in your own projects and get first insights, you have to download the current package from http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx and install it. Then, if you add a reference to the Microsoft.Contracts.dll to your project, you can access the Contract class from the namespace System.Diagnostics.Contracts. But again as reminder: the Code Contracts project is in an early state at the moment, so don’t expect a perfect solution. The team is working hard to improve their code and thus everybody should appreciate their work. Many things have to be done until the rise of .NET 4.0, but I’m sure that they’ll do their job very well.

Those are first basic information about Code Contracts. Next blog posts will involve deeper knowledge about Code Contracts, the components of Code Contracts, more examples and information about why it makes a change and why one should care about.

kick it on DotNetKicks.com