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:

Configuring Code Contracts in the project's Properties windowMore 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.

kick it on

5 Gedanken zu „Code Contracts #3: Contract checking“

  1. Excellent series of posts, I don’t know what effect will all this have on testing methodologies, but code contracts seem like unit testing on steroids. What you also get is formal verification that your contracts have 100% coverage of all code variants, which is the strongest point of Code Contracts imo.

  2. Hi Pop,

    You’re right. Contracts are more expressive than unit tests in the sense, that with the static checker you have verification over all code parts and all value ranges. With unit tests you’ve just some test cases and need defined value pairs (input and expected output) for that. But often you forget something to test…

    Regarding the combination of TDD and DbC I want to make my mind up in the following days and weeks for myself. DbC has not only advantages! The behavior that you defined is guaranteed, but who says that this is the behavior that you or a user expected? It’s very likely that you forget contracts or define wrong contracts or have errors in your contracts… and then? Testing can do very well in this case, I think. Another problem is the complexity of defining contracs. Many not so advanced developers would be overwhelmed by that. Let me do a little bit more research on DbC+TDD, I hope to have some stronger ideas soon…

  3. Hi folks,

    sorry to contradict you somewhat, but IMO code contracts and unit testing have a somewhat more complex relationship than your comments indicated.

    Granted, there is a certain amount of overlap and some unittests could quite well be expressed as contracts (because soo far they were the only means to check those contracts). But then, contracts are about stating and ensuring certain guarantees about the code, while unittests are about behaviour or the correctness of the implemented algorithm.

    To make my point clear, have a look at this example (pseudo code!):

    double Sqrt(double x)
    requires: x>=0
    ensures: ret>=0
    ensures: ret<x || ret==0

    return x/2

    This would be formally correct and state all the sensible guarantess, but dividing by two is clearly not the same as a square root. To ensure the correctness, you would still need a unit test, checking if x==Sqrt(x)*Sqrt(x). And you would not want to dupplicate the logic of your code as a contract.

    Just my 0,02€

  4. Hi AJ,

    That’s a good point. As I stated, Code Contracts are no master solution. Contracts define behavior on code, but those definitions could be insufficient or incorrect as well. This brings unit tests to mind.

    And I see the problem you mentioned: duplicating program logic in contracts is not a suitable way. In limited cases this would work and you can model implications in the form of: „if input is x, output should by y“. But in more complex cases (take complex algorithms, for example a sorting algorithm), this would be no solution. I agree with you, that in this case a unit test is the correct answer. The problem of unit test remains: it can only test one input/output pair (or a limited set), but in the case of expressing semantic logic/behavior it is the right tool. Thank you for pushing in your ideas on that, I’ll further make my mind up on that and your opinions are welcome everytime.

    Cheers, Matthias

Schreibe einen Kommentar

Deine E-Mail-Adresse wird nicht veröffentlicht. Erforderliche Felder sind mit * markiert.