# Thursday, May 28, 2009

We’ve just released the Pex 0.13.40528.2 (Nikolai has all the details about the new features). In this release, a number of attributes were added to force Pex produce more friendly inputs.

The problem with Enums

When you apply Pex to code that uses Enumerations, you quickly learn something: the CLR does not constraints the enumeration values to be defined. This means than whenever you take an Enum as a parameter, you should validate it is properly defined:

void Test(SomeEnum e) {
    if (!Enum.IsDefined(typeof(SomeEnum), e)) throw new ArgumentException(“…”);

Look at the BCL code, they actually do this kind of validation. For good or bad, some of our users have been complaining that Pex should restrict the enumeration to defined values, in fact considering the generated failing test case as noise. To restrict generated enumartion values to be defined, you can add the [PexEnumValuesDefined(typeof(SomeEnum))] attribute on your test/fixture/assembly. Internally, this attribute attaches an invariant to the given enumeration type that tells Z3 the allowed values for that type.

What about multi-dimensional arrays?

Ever wakened a day wanting to iterate arrays starting from –12345? Well you can with multidimensional arrays… The Array.CreateInstance method has an overload that takes length and lower bounds to instantiate multidimensional arrays:

int[,] array = (int[,])Array.CreateInstance(typeof(int),
    new int[] {10, 10}, // lengths
    new int[] {–12345, – 789} // lower bounds
a[-12345, –789] = –1;

Of course, this feels a bit weird because most languages won’t allow to create such arrays, but the Array.CreateInstance method is still available nonetheless. It feels a bit weird but this behavior is perfectly valid from the runtime point of view. To restrict Pex from generating such bounds, you can add the [PexZeroMdArrayLowerBounds(0)] attribute (one attribute per dimension).

What about Booleans?

Booleans is another interesting citizen of the CLR. At the MSIL level, the Boolean type is really a byte, widened as an integer when on the stack. Compilers try really hard to keep Booleans as 0 or 1 but… it is possible to craft Boolean values anywhere the byte range using safe MSIL code (not from C# though or any BCL method I know of). The implication of this are quite disturbing, for example, consider the following parameterized test:

[PexMethod] {
void BooleanMadness(bool a, bool b) {
     if (a && b && a != b)
         throw new Exception(“this is madness!”);

Clearly, in a word of Booleans constrained to 0 or 1, the branch that throws the exception should be unreachable. If you execute Pex on this test, it will generate 4 test one of which raises the exception:


Notice the actual values (0x02, 0x03) of the Booleans in the pretty printing. If you want Pex to generate Boolean that are restricted to 0 or 1, use the [PexBooleanAsZeroOrOne] attribute. This attribute forces Z3 to pick boolean values as 0 or 1. Btw, there’s already a connect bug for this behavior.

posted on Thursday, May 28, 2009 5:06:06 PM (Pacific Daylight Time, UTC-07:00)  #    Comments [0]
# Monday, May 25, 2009

If you’ve been thinking about presenting Pex to your co-workers or your local .NET community, you can use our slide decks at http://research.microsoft.com/en-us/projects/pex/documentation.aspx . The slide decks are there to help you, don’t hesitate to shuffle them, cut them or pick whatever you need in them (and of course, tell us about it).

Cheers, Peli.

posted on Monday, May 25, 2009 10:54:47 PM (Pacific Daylight Time, UTC-07:00)  #    Comments [0]
# Wednesday, May 20, 2009

If you are (or you've been) blogging about Pex, let us know and drop the link in this following forum thread:


We are building a list of links that will be hosted our project web site.

posted on Wednesday, May 20, 2009 7:26:22 AM (Pacific Daylight Time, UTC-07:00)  #    Comments [0]
# Saturday, May 16, 2009

Not sure what’s going to come up at of this but you can find me on twitter at http://twitter.com/pelikhan.

posted on Saturday, May 16, 2009 6:06:55 AM (Pacific Daylight Time, UTC-07:00)  #    Comments [0]
# 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]
# Friday, May 01, 2009

We just made a quick release to fix another installer issue related to missing packages. Along the way, we’ve added an Exploration Tree View and Partial Stubs support.

Exploration Tree View

The exploration tree view displays the list of explorations to be executed, running and finished. It serves as a progress indicator but also as a smooth result explorer. When browsing through the tree, Pex will synchronize the exploration result view and the tree view.

The tree view populates each namespace with the fixture types and exploration methods, and provide a visual feedback on the progress of Pex.


When you browse through the exploration and generated test nodes, Pex automatically synchronizes the exploration result display. This makes it really easy to start from an high-level view of the failures and drill into a particular generated test, with stack trace and parameter table.


Partial Stubs

Stubs lets you call the base class implementation of methods as a fallback behavior. This functionality is commonly referred as Partial Mocks or Partial Stubs and is useful to test abstract classes in isolation. Stubs inheriting from classes have a “CallBase” property that can turn this mode on and off.

Let see this with the RhinoMocks example on partial mocks. Given an abstract ProcessorBase class,


we write a test for the Inc method. To do so, we provide a stub implementation of Add that simply increment a counter.



  • PexAssume/PexAssert.EnumIsDefine checks that a particular value is defined in an enum.
  • Missing OpenMP files in the installer break Pex.

Poll: should we skip 0.13 and go straight for 0.14? :)

posted on Friday, May 01, 2009 1:28:25 PM (Pacific Daylight Time, UTC-07:00)  #    Comments [0]