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.

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.