# Monday, May 24, 2010

Are you using Code Contracts ? or not? Give us 5 minutes of your time and fill up the survey that the BCL has put up…


posted on Monday, May 24, 2010 8:42:30 PM (Pacific Daylight Time, UTC-07:00)  #    Comments [0]
# Thursday, December 17, 2009

Je viens du publier une video en francais sur les Code Contracts et Pex avec Manuel.


posted on Thursday, December 17, 2009 8:35:26 PM (Pacific Standard Time, UTC-08:00)  #    Comments [0]
# Wednesday, December 16, 2009

I’ll be presenting the PDC talk on Code Contracts and Pex at on January 20th, 2010 in Celestijnenlaan 200A, Heverlee (Leuven). Things change fast, so there will probably a couple changes to the presentation as well. I’ll probably talk a little but more about the tools to mine Code Contracts, etc…


posted on Wednesday, December 16, 2009 3:22:06 PM (Pacific Standard Time, UTC-08:00)  #    Comments [0]
# Wednesday, September 16, 2009

We just released v0.16.40915.5 of Pex. The major highlights of this release are Moles, a lightweight detour framework, and better support for test frameworks.

  • Moles, a lightweight detour framework: Moles is a new extension of the Stubs framework: it lets you replace any .NET method (including static methods) with your own delegate.(sample outdated) 
    Want read more about this sample? here is the full walkthrough.
    The moles framework is not yet feature complete; moles does not support constructors and external methods. Some types of mscorlib cannot be moled as they interact too deeply with the CLR.
  • Pex gets its own HostType: A HostType is a feature for the Visual Studio Unit Test framework that lets specific unit tests be run under specialized hosts such as Asp.Net or VisualStudio iself. In order to create reproducible test cases using Moles, we had to implement a HostType that lets tests be run under the Pex profiler. This is very exciting because it also opens the door for many uses of Pex such as fault injection, dynamic checking, etc… in future versions of Pex. When generating test cases with Pex, all the necessary annotations will be created automatically. To turn the Pex HostType on hand-written (non-parameterized) unit tests, simply add [HostType(“Pex”)] on your test case.
    This feature only works with Visual Studio Unit Test 2008.
  • Select your test framework: the first time you invoke ‘Pex’ on your code, Pex pops up a dialog to select your test framework of choice. You can select which test framework should be used by default and, more importantly, where it can be found on disk.
    If you do not use any test framework, Pex ships with what we call the “Direct test framework”: in this “framework”, all methods are considered as unit tests without any annotation or dependencies.
    These settings are stored in the registry and Pex should not bug you again. If you want to clear these settings, go to ‘Tools –> Options –> Pex –> General’ and clear the TestFramework and TestFrameworkDirectory fields:
  • Thumbs up and down: We’ve added thumbs up and down buttons in the Pex result view. We are always looking for feedback on Pex, so don’t hesitate to click them when Pex deserves a thumbs up or a thumbs down.
  • Performance: Many other performance improvements under the hood which should avoid Pex hog too much memory in long running scenarios.
  • Miscellanous improvements and bug fixes:
    • Support for String.GetHashCode(): we now faithfully encode the hashing function of strings, which means Pex can deal with dictionaries where the key is a string.
    • Fewer “Object Creation” messages that are not actually relevant.
    • In VS 2010, the package used to trigger an exception when the solution loaded. This issue is now fixed.
    • In Visual Studio when an assembly had to be resolved manually (i.e. that little dialog asking you where an assembly is), Pex remembers that choice and does not bug you anymore.
    • And many other bugs that were reported through the forums.
posted on Wednesday, September 16, 2009 2:16:33 PM (Pacific Daylight Time, UTC-07:00)  #    Comments [0]
# Tuesday, June 02, 2009

Inversion of Control (IoC) is a very important practice to make code testable. It usually relies on defining interfaces for each external dependency. Various frameworks and techniques, i.e. Dependency Injection (DI), Service Locator, exist to bind the interface implementations to the components. In this blog post, we will *not* focus on this aspects of IoC but rather on it’s main building block: interfaces. This article describes how Contracts for interfaces improves IoC… regardless of which DI framework/technique you are using. The Contracts for interfaces are a feature of the Code Contracts for .Net tool.

Interfaces are not Contracts

Interfaces are often referred to as Contracts in the context of IoC: they define the methods and properties that a service should implement and are a key factor in achieving the loose coupling: one can build the code against the interface and can plug in various implementation with no risks.

Unfortunately, interfaces are not contracts: while they specify how the methods signatures should be, interfaces do not specify the functional behavior. To illustrate this, let’s take a look at a well-known simple interface of the BCL:


For this interface, I could naively implement as follows:


While my implementation is really really wrong, it fulfills all requirements of the IServiceProvider interface: a method GetService that returns object. Of course, if I would have read the MSDN documentation of GetService, I would have known that object should implement serviceType. Unfortunately, the interface did not tell me anything about that and compilers don’t understand MSDN documentation either.


Contracts for interfaces

Code Contracts provides an API for design-by-contracts (pre-condition, post-condition, etc…). It also supports defining contracts for interface or abstract classes. Contracts for interfaces can be used to specify the functional behavior of interface members. While they also serve as documentation, those contracts can also be turned into runtime checks or leveraged by static checkers.


  • since interface members cannot have method bodies, the contracts are stored in a ‘buddy’ type.
  • The [ContractClass]/[ContractClassFor] attributes bind the interface type and the contract type together.
  • Contract.Result<object>() is a helper method to refer to the result value, since this is not supported in C#.

Let’s take a closer look at the body of IServiceProviderContract.GetService. It contains a pre-condition (Requires) that the serviceType should not be null and a post-condition (Ensures) that the return value should be null or should be assignable to the serviceType:


In this simple case, the contracts captured precisely the specification that we found in MSDN. The critical difference is that they are stored in a format that compilers and runtimes know pretty well: MSIL byte code. The benefits are huge:

  • documentation: the contracts are stored in a programming-language agnostic format that mined and rendered for your favorite programming language,
  • static checking: static analysis tools can (and will) use contract to try to find bugs before you execute the code, or prove that it is correct with respect to the contracts,
  • runtime checking: the runtime checker will instrument all implementations of the interface with the interface contracts automatically. Once you’ve specified how an interface should behave, you do not have to repeat yourself when re-implementing it, the re-writer takes care of that.
  • automated white box testing: tools like Pex can leverage the runtime contract checks to try to find inputs that violate the contracts.
  • IoC/DI framework agnostic: It does not matter which DI framework you use, as soon as you use interface, you could also provide contracts for it.
posted on Tuesday, June 02, 2009 5:14:03 PM (Pacific Daylight Time, UTC-07:00)  #    Comments [1]
# Saturday, May 02, 2009

This is a cool new feature that builds on Stubs, Pex  and Code Contracts  (in fact, it is really just a consequence of the interaction of the 3 technologies): stubs that act as parameterized models while complying to the interface contracts.

  • Code Contracts provide contracts for interfaces. All implementations of that particular interface will be instrumented with the runtime checks by the rewriter at compile time.
  • Stubs is really just a code generator that provides a minimal implementation of interfaces and relies on the C# compiler to build the code. Therefore, if a stub implements an interface with contracts, it will automatically be instrumented by the runtime rewriter as well.
  • Pex choices (i.e. dynamic parameter generation) may be used as the fallback behavior of stubs. In other words, whenever a stubbed method without user-defined behavior is called, Pex gets to pick the return value. Since the stub implementation itself may have been instrumented with contracts, we’ve added special handling code so that post-condition violation coming from a stub are considered as an assumption. This effectively forces Pex to generate values that comply with the interface contracts.

Let’s see how this works with an example. The IFoo interface contains a single ‘GetName’ method. This method has one precondition, i should be positive and one postcondition, the result is non null. Since interfaces cannot have a method body, we use a ‘buddy’ class to express those contracts and bind both classes using the [ContractClass] and [ContractClassFor] attributes:


We then turn on runtime rewriting for both the project under test and the test project (Project properties –> Code Contracts –> Runtime checks). As a result, the stub of IFoo automatically gets instrumented with the contracts. We can clearly see that from the generated code of GetName in Reflector below:


The last step is to write a test for IFoo. In this case, we write a parameterized unit test that takes an IFoo instance and an integer, then simply call GetName.


Since the contracts of IFoo.GetName specifies that the result should not be null, we should not see any assertion violation in this test. Moreover, we should see a test for the precondition considered as an expected exception:


Note that all those behaviors rely on extensions to Pex that the wizard automatically inserted in the PexAssemblyInfo.cs file:



  • [PexAssumeContractEnsuresFailureAtStubSurface] filters post-condition violations in stubs as assumptions,
  • [PexChooseAsStubFallbackBehavior] installs Pex choices as the fallback behavior of stubs,
  • [PexStubsPackage] load the stubs package (this is a standard procedure for Pex packages),
  • [PexUseStubsFromTestAssembly] specifies to Pex that it should considers stub types when trying to test interfaces or abstract classes.
posted on Saturday, May 02, 2009 10:19:16 AM (Pacific Daylight Time, UTC-07:00)  #    Comments [0]
# Saturday, April 25, 2009

I recorded a Channel9 video last week with Manuel Fahndrich on the interaction of Code Contracts and Pex. The demo gives a glimpse at the nice interaction between Contracts (design by contracts) and Pex (automated white box).

Code Contracts gives you a great way to specify what your code is supposed to do. These contracts can be leverage for documentation, static checkers but also – tada – by Pex! Contracts can also be turned into runtime checks which Pex will try to explore. Pex will try to cover the post conditions, assertions or in other words, find inputs that violates of your contracts etc… By adding contracts to your code, you give Pex a ‘direction’ to search for (and a test oracle).


Drop me a note if you want more of those movies.

posted on Saturday, April 25, 2009 9:09:57 PM (Pacific Daylight Time, UTC-07:00)  #    Comments [0]
# Wednesday, April 15, 2009

For the last couple of weeks, I given on helping hand to Herman Venter to set up the open-source-MS-PL-super-cool-Common Compiler Infrastructure (CCI) project.

You’ve may have heard and probably used different incarnations of the CCI in the past: the FxCop introspection engine, ILMerge, Spec# or Code Contracts use CCI in same ways. CCI is a set of tools and components that are useful to build compilers: readers and writers for MSIL and symbol files, and more. With CCI, you can now easily write your own crazy aspect oriented programming framework, inspect assemblies without reflection etc…  Just sync the sources, build it, tweak it, etc… It’s all there on codeplex at http://ccimetadata.codeplex.com.

posted on Wednesday, April 15, 2009 8:51:23 PM (Pacific Daylight Time, UTC-07:00)  #    Comments [2]
# Friday, April 10, 2009

Download the new version!

Today we’ve released a new release of Pex on DevLabs and on our academic downloads. This highlights of this release are: NUnit, MbUnit and xUnit.net support out of the box, writing parameterized unit tests in VisualBasic.NET and F#, better Code Contracts support. As always, if we encourage you to send us feedback, bugs, stories on our forums at http://social.msdn.microsoft.com/Forums/en-US/pex/threads/ .

NUnit, MbUnit and xUnit.net supported out of the box

Pex now supports MSTest, NUnit, MbUnit and xUnit.net out of the box. Pex will automatically detect which framework you are using by inspecting the assembly reference list, and automatically save the generated tests decorated with the correct attributes for that framework.


The default test framework can also be specified through the global options (Tools –> Options –> Pex –> enter the test framework name in TestFramework).



Writing Parameterized Unit Tests in VisualBasic.NET

While the Pex white box analysis engine works at the MSIL level, Pex only emits C# code for now. In previous releases, this limitation made it impossible to use Pex parameterized unit tests from non-C# code. In this release, we have worked around this problem by automatically saving the generated tests in a ‘satellite’ C# project.

Let’s see this with an example. The screenshot below shows a single VisualBasic.NET test project with a Pex parameterized unit test:


We can right-click in the HelloTest.Hello method and select “Run Pex Explorations”:


At this point, Pex will start exploring the test in the background as usual. This is where the new support comes in: When a generated test comes back to Visual Studio, Pex will save it in a separate C# project automatically (after asking you where to drop the new project):


The generated tests are now ready to be run just as any other unit tests!

Writing Parameterized Unit Tests from F#

Similarly to VisualBasic.NET, we’ve made improvements in our infrastructure to enable writing parameterized unit tests in F#. Let’s see this with a familiar example. We have a single F# library that has xUnit.net unit tests and reference Microsoft.Pex.Framework (project Library2 below). In that project, we add a parameterized unit test (hello_test):


We can right-click on the test method name and Pex will start the exploration of that test in the background. Because of the limitations of the F# project system, you absolutely need to right-click on the method name in F# if you want contextual test selection to work. Because the project is already referencing xunit.dll, Pex will also automatically detect that you are using xUnit.net and use that framework. When the first test case comes back to VisualStudio, Pex saves it in a separate C# project:


The tests are saved in the generated test project and ready to be run by your favorite test runner!

PexObserve: Observing values, Asserting values

We’ve completely re-factored the way values can be logged on the table or saved as assertions in the generated tests. The following example shows various ways to log and assert values:


In the Observe method, we use the return value and out parameter output to automatically log and assert those values. Additionally, we add “view input” on the fly to the parameter table through the ValueForViewing method, and we add “check input” to be asserted through the ValueAtEndOfTest method. After running Pex, we get the following results:


As expected, input, ‘view input’, output and result show up in the parameter table.


In the generated test, we see assertions for the return value, out parameters and other values passed through the ValueAtEndOfTest method.

Code Contracts : Reproducible generated tests

When Pex generates a unit test that relied on a runtime contract, Pex also adds a check to the unit test which validates that the contracts have been injected into the code by the contracts rewriter. If the code is not rewritten when re-executing the unit test, it is marked as inconclusive. You will appreciate this behavior when you run your unit tests both in Release and in Debug builds, which usually differ in how contracts get injected.


Code Contracts:  Automatic filtering of the contract violations

When Pex generates a test that violates a Code Contract pre-condition (i.e. Contract.Requires), there are basically two scenarios: the precondition was on top of the stack and should be considered as an expected exception; or it is a nested exception and should be considered as a bug. Pex provides a default exception filtering that implements this behavior.

Stubs: simplified syntax

We’ve considerably simplified the syntax of stubs by removing the ‘this’ parameter from the stub delegate definition. Let’s illustrate this with a test that stubs the ‘ReadAllText’ method of a fictitious ‘IFileSystem’ interface. 

Stubs: generic methods

The Stubs framework now supports stubbing generic methods by providing particular instantiations of that method. In the following example, the generic Bar<T> method is stubbed for the particular Bar<int> instantiation:


Stubs and Pex: Pex will choose the stubs behavior by default

We provide a new custom attribute, PexChooseAsStubFallbackBehaviorAttribute, that hooks Pex choices to the Stub fallback behavior. To illustrate what this means, let’s modify slightly the example above by removing the stub of ReadAllText:


If this test was to be run without the PexChooseAsStubFallbackBehavior attribute, it would throw a StubNotImplementedException. However, with the PexChooseAsStubFallbackBehavior attribute, the fallback behavior calls into PexChoose to ask Pex for a new string. In this example in particular, on each call to ReadAllText, Pex will generate a new string for the result. You can see this string as a new parameter to the parameterized unit test. Therefore, when we run this test under Pex, we see different behavior happening, including the “hello world” file:


Note that all the necessary attributes are added at the assembly level by the Pex Wizard.

Miscellanous bug fixes and improvements

  • [fixed] Dialogs do not render correctly under high DPI
  • When a generic parameterized unit tests does not have any generic argument instantiations, Pex makes a guess for you.
  • When a test parameter is an interface or an abstract class, Pex now searches the known assemblies for implementations and concrete classes. In particular, that means that Pex will often automatically use the automatically generated Stubs implementations for interfaces or abstract classes.
  • Static parameterized unit tests are supported (if static tests are supported by your test framework)
  • Better solving of decimal and floating point constraints. We will report on the details later.

Breaking Changes

  • The PexFactoryClassAttribute is no longer needed and has been removed. Now, Pex will pick up object factory methods marked with the PexFactoryMethodAttribute from any static class in the test project containing the parameterized unit tests. If the generated tests are stored in a separate project, that project is not searched.
  • The PexStore API has been renamed to PexObserve.
  • Pex is compatible with Code Contracts versions strictly newer than v1.1.20309.13. Unfortunately, v1.1.20309.13 is the currently available version of Code Contracts. The Code Contracts team is planning on a release soon.


Happy Pexing!

posted on Friday, April 10, 2009 12:06:31 PM (Pacific Daylight Time, UTC-07:00)  #    Comments [12]
# Thursday, March 19, 2009

The videos of TechDays are up:

While attending TechDays Finland in Helsinki, I had the opportunity (thanks Vesa) to take a swim in the baltic frozen sea along with fellow Microsoftie Scott Galloway (i’ll spare you the video of the actual bath).

Great way to dust off the remaining of jetlag.


ps: Yes we are standing on the sea.

posted on Thursday, March 19, 2009 5:28:22 PM (Pacific Daylight Time, UTC-07:00)  #    Comments [1]
# Saturday, February 28, 2009


Ealier this week, we released the Code Contracts library for .NET. Since then, I’ve implemented a lot for contracts for the data structures in QuickGraph . In this post, I’ll talk about my experience with the contracts…


Walking through some contracts.

Let’s take a look at the contracts of AddEdge, a method that adds an edge to a graph. Adding an edge to a graph is certainly a fun adventure, when you write contracts for it. Let’s take a look:

public interface IMutableEdgeListGraph<TVertex, TEdge> : ...
    where TEdge : IEdge<TVertex>
    /// <summary>
    /// Adds the edge to the graph
    /// </summary>
    /// <param name="edge"></param>
    /// <returns>true if the edge was added, otherwise false.</returns>
    bool AddEdge(TEdge edge);

Interface contracts

Since IMutableEdgeListGraph is an interface, we need to store the contracts in separate class. To do so,  we ‘bind’ the interface and the contract class to each other using the ContractClassForAttribute/ContractClassAttribute.

    public interface IMutableEdgeListGraph<TVertex, TEdge> ...
    sealed class IMutableEdgeListGraphContract<TVertex, TEdge>
        : IMutableEdgeListGraph<TVertex, TEdge>
        where TEdge : IEdge<TVertex>

Once both types are bound, you can start implementing the contracts of the interface in the contract class. Note that the contract class must use explicit interface implementations for all methods.

Basic null checks

If you care about null references, the first contract will probably to ensure the edge is not null. To make it quick and painless, make sure you use the crn snippet. Note that since the method body of the contracts does not matter, we simply return the default value.

bool IMutableEdgeListGraph<TVertex, TEdge>.AddEdge(TEdge e)
    Contract.Requires(e != null);
    return default(bool);

More pre-conditions

One of the implicit requirement of AddEdge is that both vertices should already belong to the graph. We want to make this explicit as a pre-condition as well:

bool IMutableEdgeListGraph<TVertex, TEdge>.AddEdge(TEdge e)
    IMutableEdgeListGraph<TVertex, TEdge> ithis = this;
    Contract.Requires(e != null);

There are two things to notice here: (1) we had to cast the “this” pointer to the interface we are writing contracts for, IMutableEdgeListGraph<,>. Because the methods in a contract class must be explicit interface implementations, we do not have access to the members of this interface from the “this” pointer, (2) ContainsVertex had to be annotated with [Pure], as any method called from a contract must be pure:

bool ContainsVertex(TVertex vertex);

What about post-conditions

One of my favorite feature of Code Contracts is to be able to state post-conditions. This is done by calling the Contracts.Ensures method. For example, we start by expressing that the edge must belong to the graph when we leave AddEdge:

bool IMutableEdgeListGraph<TVertex, TEdge>.AddEdge(TEdge e)
    IMutableEdgeListGraph<TVertex, TEdge> ithis = this;

Result and Old

Since the method returns a boolean, we should also state something about the result value. To refer to the result, one has to use the Contract.Result<T>() method. In this case,  the method returns true if the edge was new, false if it was already in the graph. We can refer to a pre-state, i.e. the value of this.Contains(e) at the beginning of the method***:

== Contract.OldValue(!ithis.ContainsEdge(e)));

Lastly, we can also make sure the edge count has been incremented, if an edge was actually added (as you can see, we could use an implication operator in C#):

== Contract.OldValue(ithis.EdgeCount) + (Contract.Result<bool>() ? 1 : 0));

*** The OldState value is evaluated after the preconditions.

Where to go next?

In the next post, I’ll show how to leverage these Contracts with Pex

posted on Saturday, February 28, 2009 8:33:15 AM (Pacific Standard Time, UTC-08:00)  #    Comments [2]