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.