Code Contracts | Mind-driven development

Code Contracts #5: Method purity

After getting some things done, now I’m returning to Code Contracts. In the first parts of this series I gave you some basic information about Code Contracts, the static and dynamic checker, the code rewriter and how implications can be modelled. This day’s blog post comes up with another interesting aspect: method purity. There seems to be some misunderstanding on this term – I want to clear some clouds and show you what method purity means and which implications it has.

Code Contracts come with an attribute called [Pure] for decorating class methods (and by which you can declare a method as being „pure“). Method purity is a quality, expressing that the method is free of observable side effects. This means, it does not change the observable state on any objects seen by callers in some way. For example, pure methods do neither modify properties of a class nor reference type method arguments. Even the modification of a private field (which is not seen by callers directly) is prohibited, if class methods work with this field and return values, that depend on it. In this case the change of the field is indirectly reflected by a changed method return value, thus the observable state has changed! To summarize, mostly pure methods are only allowed to change objects that have been created after method entry.

The following code shows the simple class Point and gives you a short example of how to use Pure in declaration and pure method calls in contracts. The static and dynamic checkers will both be very happy with that 🙂 :

public class Point
{
    public int X { [Pure] get; set; }
    public int Y { [Pure] get; set; }

    public Point() { }

    [Pure]
    public double GetDistance()
    {
        return Math.Sqrt(X * X + Y * Y);
    }

    public void SwapXY()
    {
        Contract.Ensures(Contract.OldValue<int>(X) == Y);
        Contract.Ensures(Contract.OldValue<int>(Y) == X);
        Contract.Ensures(Contract.OldValue<double>(GetDistance()) == GetDistance());

        int temp = X;
        X = Y;
        Y = temp;
    }
}

(Perhaps not the best example, because we have redundant information in code and contracts in SwapXY() – that should not be the goal in most cases, but in this simple scenario it’s quite ok for demonstration purposes)

All methods that are called within a contract (pre-/postcondition etc.) must be declared pure. But why?

First it has a very certain reason: contracts like the Contract.Requires() and Contract.Ensures() assertions will not be evaluated in every execution and build configuration. For example, you can choose just to check pre-conditions, thus stepping over the post-conditions. I don’t need to explain, that methods with side effects in those post-conditions would be a messy thing. The execution results of your code would depend on the configuration of Code Contracts and if the contracts are evaluated – this must be prohibited and that’s why all methods called in contracts must be pure. Remember that Code Contracts is declarative code. It should not influence the behavior of your code, but just decorate it in some way.

Second, declaring methods as pure is generally a good thing. Beside of allowing you to use those methods in contract declarations, it furthermore helps the static checker in its task. Since method arguments can not be changed arbitrarily in pure methods, the static checker can assume that those objects will be the same after the method call.

Third (and for me that raises Code Contracts to an even higher level), declaring a method as pure can yield to a better software design and just clarifies your intent. You as programmer are able to express explicitly that your method does not have side effects. The intention of the method is revealed to callers (intention revealing), who can rely on the fact, that the state of the method’s class will be the same after calling the method as before. Thinking about declaring as many methods as possible as pure quickly brings us to command-query-separation, where you are trying to have exactly two types of methods. On the one handside the commands, which change class state and on the other handside queries, which calculate some value from current class state, but don’t modify it. Thus, queries are pure methods and with the [Pure] attribute you are able to explicitly express this intention. Dividing commands/queries and expressing queries with [Pure] is often (while not everytime) a good thing, since it leads to clear design and distinct intention and let you avoid side-effecting methods, which can be horrible code smells indeed (think of deep-nested side-effecting methods, for example).

Currently there is no component of Code Contracts which checks if methods declared pure are pure indeed. Thus if a programmer decorated a method with [Pure], it’s just believed. The Code Contracts team is working heavy on that, thus to come up with a purity checker in a future release.

(Update: thanks to AJ, I clarified my intent with the following section) Moreover one may ask: Are there any implications to automatic parallelism? The answer is: not directly. Parallelism is a hot topic and one could think, that method purity brings automatic parallelism of calls to such methods to life. And purity is indeed a strong characteristic of a method, but it’s not sufficient for the auto-par task. It’s just a one-way road, since it declares, that a method is side-effect-free (thus it doesn’t write any shared state). But in general a method can also read shared objects and depending on this it could return another value. Thus, parallelism of those method’s calls could run into problems (returning non-expected values), if the state is changed by other methods between subsequent calls. Perhaps there will be more attributes similar to [Pure] for such use cases in the future or other structures to handle that? I’m a believer…

So far for now on this topic. As you can see, decorating your methods in a declarative way with attributes like [Pure] can express your intent in a very smooth way. It helps you to clarify your design and it helps other programmers to know your intent – not just by code comments, but by checked documentation via Code Contracts.

Code Contracts #4: Modelling implications

Hey guys. It’s me again on Code Contracts. Sorry for not posting something on this exciting topic during the last weeks, I’ve been busy with some other tasks. This day’s post will cover some more technical ascpect of Code Contracts: how can we model implications using Code Contracts?

Code Contracts bring the DbC principle into the .NET world as one feature of the upcoming .NET framework 4.0. It’s providing statements on the code, which can be used to define specifications of how this code should work. Software elements should be understood as implementations which satisfy those specifications – that’s a very systematic approch and the core idea behind DbC. Let’s take a class method. With DbC in general and Code Contracts in particular, you’re able to define a system of obligations and benefits on this method. Obligations for clients of this method can be modelled via pre-conditions (Code Contracts: Contract.Requires(...)) to express, which conditions have to be satisfied by the client to run the method properly. In return the client get’s some benefits from the supplier (the method itself), if it maintains the obligations. Those guaranteed benefits can be defined by post-conditions on the method (Code Contracts: Contract.Ensures(...)). This obligation/benefit-based approach is very similar to contracts between humans. Example: I give you some money (my obligation as client) and you give me in return a Toyota Prius (my benefit from you as supplier), but you’re not bound to give me a Ferrari or Mercedes or something.

Thus in normal contract cases (code or real-life) you say „I give you X and you give me Y in return“. For a code example: „I give you an integer X>0 and you give me some number Y between 0 and X in return“ (e.g. a random number). But other contracts can be imagined, where the benefit depends on what has been delivered by the client. Real-world example: „I give you 40.000 $ and you give me a Toyota Prius. But if I give you 75.000 $, you give me a Mercedes S-class.“ That’s an implication. „If I give you X, you give me Y“ or shortly „X => Y„. Cases can be imagined, where this could be useful in contracts on code. For example: „If you give me an empty list or null, I’ll return null. If you give me a non-empty list, I’ll return an element not equal to null.“ In this scenario, it depends if you would use a pre-condition to prohibit empty lists or null’s as parameter or not, but let’s assume those cases are normal and allowed by the method, thus shifting the responsibility to handle those in the supplier (the method) instead of the client.

Such implications are generally post-conditions on methods („I’ll give you something…“), but cannot defined directly through Code Contracts. But that’s no definite issue of Code Contracts. Implications are a special form of boolean expressions and every form of boolean expression can be used as input of a Contract.Ensures(...) call. Rather that’s a limitation of most .NET languages like C#. They don’t have an implication operator for boolean expressions and therefore don’t have direct implication support.

Solution for that is the decomposition of implications to primitive boolean expressions. Consider two boolean expressions a and b. Then the implication „a => b“ is semantically equivalent to „!a || b„, which can be used in this form in any program code.

Let’s take the example from above again: „If you give me an empty list or null, I’ll return null. If you give me a non-empty list, I’ll return an element not equal to null.“ This contract can be modelled with three implications: „list==null => null“, „list.Count==0 => null“, „list.Count > 0 => !null“. Using Code Contracts and boolean substitution, we end in the following code:

public string GetSomething(IList<string> list)
{
    Contract.Ensures(!(list == null) || (Contract.Result<string>() == null));
    Contract.Ensures(!((list != null) && (list.Count == 0)) || (Contract.Result<string>() == null));
    Contract.Ensures(!((list != null) && (list.Count != 0)) || (Contract.Result<string>() != null));

    if ((list == null) || (list.Count == 0))
        return null;

    return list[0];
}

Looks a little bit frightening, doesn’t it? Moreover, the static checker will be overwhelmed with that (doesn’t have a contract on the indexer of list and thus doesn’t know, that list[0] will return a value != null). Ok, that’s perhaps not the best example, but it shows one general problem: expressions can become very big and obscure, even in relatively simple cases. That raises the question where and when to use contracts, but that’s another story…

That’s it for the moment. As you can see, implications can be used not directly, but relatively easy by use of boolean expression substitution. One could call for direct support, but that’s a language feature (providing an implication operator) and need not to be considered by the Code Contracts team. More stuff to come as soon as I find some spare time.

Code Contracts #3: Contract checking

In my first two posts of this series, I covered some basic information about Code Contracts, their origins and core elements of DbC as well as the basic declarative nature of Code Contracts, the Contract Rewriter and why contracts are defined imperatively and not via attributation or additional keywords. In this blog post, I’ll dig even deeper to show the two main elements, how contracts on your code are checked…

The functionality of checking contracts/conditions on your code comes from two main components of Code Contracts: the dynamic checker (runtime checker) and the static checker. Those can be configured and activated after installation of the Code Contracts package through a new tab inside the project’s Properties window:

More information on that can be found e.g. on the Code Contracts User Manual.

The dynamic checker

The first component is the dynamic checker, which is even called runtime checker, what better implies its behavior. This type of contract checking is done at runtime of your program code. Everytime when the program execution hits a point, where contracts are defined, the Contracts runtime checks, if the contracts are fulfilled in the current context, that means with the current class state, current variable and parameter values etc. Thus the dynamic checker is searching for actual broken contracts in just the current context. Its behavior is very similar to a test (under the given context) resp. to a Debug.Assert(), leading to the term of validation of your code. If a contract check fails, then the default behavior is that a ContractException is thrown and the application terminates. This can be easily adopted to your own needs.

The static checker

So, dynamic checking ensures at runtime that no contracts are broken by current calls of your code. But it leads to the same problems as in unit testing: code coverage, choice of input/output pairs etc. Perhaps contract violations are not found during testing, because the checking with a chosen set of parameters fulfills those contracts. Problems occur, when you deliver your code and other developers use parameters that you didn’t consider and then contracts are not fulfilled any more.

The second and more interesting part of Code Contracts checking is the static checker. What’s the difference to dynamic checking? The static checker is able to check defined contracts at compile time of your code. Moreover, the static checker doesn’t only search for actual broken contracts, but for all possibilities where contracts could be broken by the defined code. For example, let’s imagine a method int Predecessor(int x), that returns the value x-1 and a post-condition on that method, that the return value is in every case ">= 0". With dynamic checking, perhaps you input some arguments for x: 1,5,100,13, … it would never lead to a situation, where the contract is broken. With static checking instead, the static checker would analyze the code at compile time and would recognize, that there are situations (every value for x < 1) where the post-condition of the method is not fulfilled. In this case, the static checker would output a warning to inform the developer of the possible contract breach.

With all this, the static checker is doing a formal verification of the defined contracts in contrast to the test-based validation of the dynamic checker. This is done by a complex algorithm that’s based on methods of formal logic and program verification and that’s why the static checker needs some time to perform the verification. The concrete algorithm is using abstract interpretation of the code, thus the code is being inspected, but not executed! By this process and with a basic rule-set on the CLR, facts about the code are generated and those facts are used to find out, if the code fulfills the defined contracts or not. The behavior of Code Contracts is very nice in comparison with the dynamic checking, but the complexity of this process may not be underestimated. Moreover, it’s heavily requiring contracts on most code pieces that you use in your contracted code, for example in the .NET framework. That’s why the Code Contracts team is currently working hard to introduce contracts all over the .NET libraries. Let’s do an example: if you have a string s and call s.Contains(), then you as programmer know that s.Contains() doesn’t change s or any other values. But if there would be no contracts on String.Contains(), then the static checker of Code Contracts could not know that Contains() is free of side effects and isn’t changing the value of s. Thus, it would warn on any post-condition of a method, that makes use of the value of s.

The following example shows a compiler warning, created by the static checker. The method WithDraw() for withdrawing money from an account has been understood and implemented as deposit (using the Deposit() method) with a negative amount. The static checker fails, because on deposit only positive values are allowed and that’s what the pre-condition on Deposit() declares. The warning is shown in the following picture. Furthermore you can see, that Code Contracts is suggesting a pre-condition on WithDraw(), by which the contract could be fulfilled.

Warning of the static checker at compile time

And that’s it again for the moment. In this blog post I’ve introduced the two core checking components of Code Contracts: the static checker and the dynamic checker. Where the dynamic checker is just doing a validation at runtime under the actual values context, the static checker is performing a complex formal verification at compile time, which finds all possible contract breaches. Those are two very different approaches and should be clear before using Code Contracts. Next blog posts will give you more examples on defining contracts and further insights.

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…

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.