Tag Archives: code contracts

“Code Contracts, Pex and Chess” Peli de Halleux

[MS Techdays 2009] Summary “Code Contracts, Pex and Chess! Peli de Halleux”

My personal favorite of MS Techdays 2009

The presentation was basically a walkthrough introducing three upcoming tools from MS research labs: Code Contracts, Pex and Chess.

Code Contracts
For the moment contracts and interfaces only guarantee type safety. Code Contracts framework wants to do more. The functionality will become available in .NET 4.0 through the System.Diagnostics.Contracts namespace.

Code Contracts allow for checking pre- (Contract.Requires) and post-conditions (Contract.Ensures) during development and at runtime. The functionality of checking post-conditions is really cool. A runtime rewriter will move these checks after the code were the method returns a value.

An example:

string TrimEnd(string s, string suffix) {
    Contract.Requires(s != null);

There is the possibility to put the Contacts in a different assembly and at run-time doing only light-weight checks. The tool is capable of putting the two assemblies back together.

For the moment it supports static and dynamic checking (through Pex see below). In the near future an automatic documentation generator will be added.

Pex is an automated white box testing tool for .NET. It focuses on the problem that humans are not good at creating exhaustive test cases. The tool supports parameterized unit testing. This is nothing new and already available in a lot of test frameworks. What Pex adds is a separation of concerns: humans specify the tests and test-data is generated by the tool. We are good in finding the scenario’s to test and the computer is good at creating exhaustive test-data for the test we create. Exhaustive in the sense that all code-paths are followed at least once.

An example (see below): for the method on the left , the tool will generate for every branch it finds test-date, so every branch is covered. The first if clause imposes a condition on the variable a so we see a test appearing (in the table on the right) checking for the condition null and not null. For the not null condition the tool generates the most basic data to fulfill the case i.e. an empty array.


It is important to notice this is not boundary value analysis!

Pex is very handy for reverse engineering. It helps to build test-cases for legacy code. If you need to refactor the legacy code lather on, your effort is not lost. It is very easy to regenerate the tests.

Chess is a tool for finding and reproducing Heisenbugs in concurrent systems.

A Heisenbug (named after the Heisenberg Uncertainty Principle) is a computer bug that disappears or alters its characteristics when an attempt is made to study it. [Have a look at http://en.wikipedia.org/wiki/Unusual_software_bug for other unusual software bugs.]

Chess approaches these problems by taking over the thread scheduler to make the multithreading behavior deterministic. It creates fixed thread schedules that are added as attributes to your code. It is build upon Control Thread Scheduling (CAP) framework.