reportlogo.png Pex - Automated Exploratory Testing for .NET



Pex generates Unit Tests from Parameterized Unit Tests through Automated White box Testing based on Dynamic Symbolic Execution:


parameterzedtestsschema.png

  • The result is a small test suite with high code coverage.
  • Pex can be used with Test First or Test After development styles.
  • Pex emits tests and mocks for MSTest, MbUnit, NUnit, xUnit.Net,...
  • Pex integrates with Visual Studio 2008 enabling Exploratory Test Driven Development.
  • Pex builds on top of a managed profiling API, Extended Reflection, which allows to easily build .Net monitoring applications.

More links


Getting Started


Welcome to Pex, an Automated Whitebox Test generation tool for .NET.


More questions?

Frequently Asked Questions


Could you give me a brief comparison between Pex vs MSTest unit testing?

Think about Pex with VSTS unit testing rather than 'vs'. Pex acts as a plugin for unit test framework by providing parameterized unit tests, but it does not prevent the user from writing 'closed' unit tests.

In fact, in many situations, it will probably more adequate to write a 'closed' unit test rather than a parameterized one.

The following example shows how unit tests and parameterized unit tests can live together in the same test class:

  • a classic unit test
    // no parameters, using 'closed' unit tests
    [TestMethod]
    public void AddMoney() {
         Account account = new Account();
         account.Add(100);
         Assert.IsTrue(account.Amount == 100);
    }

  • a parameterized unit test,
    // adding money, we can write a parameterized unit test here
    [PexMethod]
    public void AddMoney(int amount) {
         Account account = new Account();
         account.Add(amount);
         Assert.IsTrue(account.Amount == amount);
    }

Do you support NUnit, MbUnit and xUnit.net?

Yes, extensions for these test frameworks can be downloaded from the Pex Extensions Project.

Can I mix Unit Tests and Parameterized Unit Tests in the same class?

Yes, both can live in the same class. In fact, that is what happends when Pex generates
unit tests.

[TestClass]
class Test {
    [PexMethod] void Foo(int i) {... }
    [TestMethod] void Bar() { ... }
}

Is this a random test generation tool?

No, Pex uses a constraint solver to generate new test inputs.

Is this a test stub generation tool like the MSTest Unit Test Wizard in Visual Studio?

No, from a parameterized unit test written by the user, Pex generates unit tests that call back that test.
In other words, Pex generates test inputs. See example above.

Pex also comes with a Wizard that can generate parameterized test stubs, but they are meant as a boiler
plate starting point, just like the Visual Studio unit test wizard.

Does Pex work with TypeMock?

Currently Pex and TypeMock do not work together.

Do I need to use the PexClassAttribute?

No, the PexClassAttribute is optional. It can be used to specify additional settings for Pex, such as the Test To Code Binding.


How do I load a Pex report in Visual Studio?

When you have run Pex from the command line, you can load the results in Visual Studio through the Pex Exploration Results view.

  • click on the Import Report icon,
importimage.png
  • locate the report.per file in the report folder and select it

Unit Testing


Unit Testing  is a procedure used to validate that individual units of source code are working properly. A unit is the smallest testable part of an application, i.e. a class or method in .Net.

Several frameworks  exist to automate the discovery, execution and result logging of the unit test.

Pex supports a large number of .Net test frameworks.

Parameterized Unit Testing


Parameterized Unit Tests (PUTs) are... tests that take parameters. Unlike traditional unit tests, which are usually closed methods, PUTs take any set of parameters. Is it that simple? Yes! From there, Pex will try to generate the (minimal) set of inputs that fully cover the code reachable from the test.

PUTs are defined using the PexMethod custom attribute in a similar fashion to MSTest (or NUnit, MbUnit, xUnit). PUTs are instance methods logically grouped in classes (tagged with PexClassAttribute). The following sample shows a simple PUT stored in the MyPexTest class:

[PexMethod]
void ReplaceFirstChar(string target, char c) {
    
    string result = StringHelper.ReplaceFirstChar(target, c);
 
    Assert.AreEqual(result[0], c);
}
where ReplaceFirstChar is a method that replaces the first character of a string:

class StringHelper {
    static string ReplaceFirstChar(string target, char c) {
        if (target == null) throw new ArgumentNullException();
        if (target.Length == 0) throw new ArgumentOutOfRangeException();
        return c + target.Substring(1);
    }
}

From this test, Pex can automatically generate inputs for a PUT that cover many execution paths of the tested code. Each input that covers a different execution path gets 'serialized' as a unit test:

[TestMethod, ExpectedException(typeof(ArgumentNullException))]
void ReplaceFirstChar0() {
    this.ReplaceFirstChar(null, 0);
}
...
[TestMethod]
void ReplaceFirstChar10() {
    this.ReplaceFirstChar("a", 'c');
}

For more details on getting started with PUTs, see


See Also

PexMethodAttribute, PexClassAttribute, PexAssume, Generic Parameterized Unit Testing

Automated White box Testing


Classic unit tests are methods without parameters, parameterized unit tests are methods with parameters. In fact, parameterized unit tests have been around for a while now. Referred to as data-driven tests, they were already supported by MSTest in VisualStudio and MbUnit (and previous frameworks) from version 1.

Yet, it used to be the case that the user had to provide the input parameters for those tests, as ranges, spreadsheet or database of some sort. Improper choice of inputs would lead to missed corner cases or a hugely redundant test suite.

With Pex, things change for the better: the user does not have to provide any input to the parameterized unit tests. By analyzing the program behavior at runtime, inspecting all the branch statements in the program, Pex can generate inputs that matter, i.e. inputs that will increase the code coverage of the test suite.

Whitebox Testing


White box Exploratory Testing is test design and test execution at the same time. As testing progresses, the tester learns more and more about the behavior of the code. Together with experience and creativity he can craft more and better tests.

Pex uses Dynamic Symbolic Execution, a technique that can be seen as an instance of Exploratory Testing. The tool executes the code multiple times and learns about the program behavior by monitoring the control and data flow. After each run, it picks a branch that was not covered previously, builds a constraint system (i.e. predicate over the test inputs) to reach that branch, then uses a constraint solver to come up with new test inputs, if any. The test is executed again with the new inputs, and this process repeats. On each run, Pex might discover new code and dig deeper into the implementation. In this way, Pex explores the behavior of the code. We also refer to this process as Automated Exploratory Testing.

Input Generation By Dynamic Symbolic Execution


Pex generates inputs for parameterized unit tests by analyzing the branch conditions in the program. Test inputs are chosen based on whether they can trigger new branching behaviors of the program. The analysis is an incremental process. It refines a predicate q: I -> {true, false} over the formal test input parameters I. q represents the set of behaviors which Pex has already observed. Initially, q := false, since nothing has been observed yet.

The steps of the loop:
  1. Pex determines inputs i such that q(i)=false using a constraint solver. By construction, the input i will take an execution path that we have not seen before. (And initially, this means i can by any input since we haven't seen any execution path yet.)
  2. Pex executes the test with the chosen input i, and monitors the execution of the test and the program-under-test takes.
  3. During the execution, the program takes a particular path which is determined by all the conditional branches of the program. The set of all conditions that determine the execution is called the path condition, written as the predicate p: I -> {true, false} over the formal input parameters. Pex computes a representation of this predicate.
  4. Set q := (q or p), i.e. we record that we have now seen the path represented by p.
  5. Go to 1.

Pex' constraint solver can deal with values of all types that may appear in .Net programs:

Pex filters out those inputs which violate stated assumptions.

Besides the immediate inputs (arguments to parameterized unit tests), a test can draw further input values from the PexChoose static class. The choices also determines the behavior of parameterized mocks.

Code Coverage Analysis


Code coverage is collected by on-the-fly code instrumentation. The collected information contains details information about the frequency of all explicit and implicit branching decisions. From that, edge and basic block coverage information is computed, and basic block coverage is visualized on the source files.

Pex uses an iterative test input generation algorithm which systematically enumerates all reachable execution paths of a program.

Supported Test Frameworks


Pex supports the following test frameworks:


Attribute Usage Table

Feature Visual Studio Unit Test xUnit.net Description
fixture [TestClass, PexClass] [PexClass] tests are logically grouped in a type
parameterized test [PexMethod] instance method tagged with PexMethod same
fixture setup [ClassInitialize] supported not supported
fixture teardown [ClassCleanup] supported not supported
test setup [TestInitialize] supported not supported
test teardown [ClassCleanup] supported not supported

All other attributes are copied to the generated unit tests but their function is not understood.

  • For VSTS, the ITestContext instance is always null.

Specifying up the test framework

Pex automatically guesses the test framework by walking the list of assembly references of the test project and looking for the unit test framework assembly. If Pex cannot guess the test framework you are using, you can set it with the TestFramework option of the PexAssemblySettingsAttribute. 

[assembly: PexAssemblySettings(TestFramework = "Repro")]

Microsoft.ExtendedReflection


Extended Reflection (ER) is a library that offers functionality that greatly extends the standard reflection library, and also lifts the unmanaged CLR profiling API into the managed world.

ExtendedReflection.png

Our Presentations and Screencasts contain an overview of how the managed profiling API works and how you can use it.

Extended Reflection consists of two assemblies:

  • The managed assembly has the following namespaces:
    • Metadata -- metadata model that can faithfully represent all entities that exist at runtime
    • DataAccess -- fast and type-safe accessors to "live" program data
    • Interpretation -- interpreter of all MSIL instructions, and symbolic representation of runtime values and entire states by terms
    • Reasoning -- interface for symbolic reasoning over MSIL instructions
    • Monitoring -- the managed counterpart of the ClrMonitor that receives callbacks from the instrumented code
    • Utilities -- a set of general utility classes (collections, for debugging, logging, etc)
  • The unmanaged CLR profiler called "ClrMonitor"; it instruments MSIL instructions, i.e. redirecting calls and inserting callbacks

Extended Reflection comes with a set of Code Substitutions to better handle calls to native code.

Reference Manual


Reference

WikiBook


This manual was rendered as a single HTML page at

Samples


Pex comes with a set of samples that you can open them from the program folder.

Requirements

  • Visual Studio 2008 Professional or higher,
    • Visual C#,
  • you can force the installation of the samples by using the 'Custom' selection of features in the installer.

Contents

If you want guidance at which sample is the right one for you to start, read here.


More Samples


The Pex Extensions Project contains additional extensions and samples:

  • DySy, advanced extensiblity sample

Screencasts


Tutorial


pextutorial.png

The Pex tutorial will help you get started with Pex in Visual Studio, and it explains the how Pex works.

Introduction


Pex generates Unit Tests from Parameterized Unit Tests through Automated White box Testing based on Input Generation:


All tools work on top of Pex' managed profiling API, Extended Reflection, which allows to easily build .Net monitoring applications. The managed profiling API is built on top of the CLR Profiling API.

How Pex Will Help You


If you want to ...



Writing Parameterized Unit Tests


When you are ready to write your own parameterized unit tests, we will show you how depending on the code you want to test:

  • Algorithms over primitive data, arrays of primitive data
    • Write parameterized unit tests. more...
  • Algorithms over interfaces
    • Use Pex' automatic mock object generation. more...
  • Algorithms over complex data, e.g. compiler
    • Let Pex generate an abstract representation of the data first, then feed it to the algorithm. more...
    • Let Pex build instances via custom object creation and data invariants, then invoke algorithm. more...
  • Data containers
    • Write parameterized unit tests. more...
    • Let Pex build instances via custom object creation and data invariants, then invoke a method of the container, and check invariants afterwards again. more...
    • Write parameterized unit tests which call different methods of the implementation depending on the parameter values. more...
  • Client / Server Architectures in a public environment, e.g. web service client, web service server
    • Generate interfaces for web services. more...
    • Use Pex' mock objects to simulate other side. more...

Cheat Page

important attributes in Pex: Print this page!

Getting Started

Add Pex reference Microsoft.Pex.Framework.dll
Bind test project [assembly: PexAssemblyUnderTest("UnderTest")]

Custom Attributes

PexClassAttribute marks a type containing PUT
PexMethodAttribute marks a PUT
PexAssumeNotNullAttribute marks a non-null parameter 

using Microsoft.Pex.Framework;
[..., PexClass(typeof(Foo))]
public partial class FooTest {
    [PexMethod]
    public void Bar([PexAssumeNotNull]Foo target, int i) {
        target.Bar(i);
    }
}

Static Helpers

PexAssume evaluates assumptions (input filtering)
PexAssert evaluates assertions
PexChoose generates new choices (additional inputs)
PexObserve logs live values to the report and/or generated tests 

[PexMethod]
void StaticHelpers(Foo target){
    PexAssume.IsNotNull(target);
    int i = PexChoose.FromCall(this).ChooseValue<int>("i");
    string result = target.Bar(i);
    PexObserve.ValueForViewing<string>("result", result);
    PexAssert.IsNotNull(result);
}

Instrumentation

PexAssemblyUnderTestAttribute binds a test project to a project
PexInstrumentAssemblyAttribute specifies to instrument an assembly 

[assembly: PexAssemblyUnderTest("MyAssembly")] // also instruments "MyAssembly"
[assembly: PexInstrumentAssembly("Lib")]

Pex Extensions Project


Pex is extensible! Many extension points are available to plugin into the Pex infrastructure. For example, you can build
  • custom test framework support,
  • custom language support,
  • custom exception filtering,
  • custom symbolic checking,
  • or even directly 'listening' to the instrumentation events.

Pex Extensions is an open source project that centralizes extensions for Pex. If you want to build a new extension (as open source), we would recommend you to join that project and develop it over there.


Support for NUnit, MbUnit or xUnit.net is provided through this project.

See Also

Community 

MSTest


Visual Studio Unit Test Framework

Pex can leverage already existing test suites, and can generate tests for MSTest.
Z3

Theorem Prover and Constraint Solver.

See http://research.microsoft.com/projects/Z3 .

PexClassAttribute


Attribute that marks a class that contains 'explorations'. It is the equivalent of MSTest's TestClassAttribute (or NUnit's TestFixtureAttribute). This attribute is optional.

The classes marked with PexClass must be 'default constructible':
  • publicly exported type,
  • default constructor
  • not abstract

If the class does not meet those requirements, an error will be proced in the report and the exploration will fail.

It is also strongly advised to make those classes 'partial' so that Pex can generate new tests that are part of the class, but in a separate file. This approach solves a lot of problems due to visibility and fits naturally into C#.

This attribute inherits from the PexSettingsAttributeBase and contains a lot of customization parameters.

  • additional suite and categories,
[TestClass] // VSTS test fixture attribute
[PexClass(Suite = "checkin")] // Pex fixture attribute
public partial class MyTests { ... }

[PexClass(typeof(Foo))] // this is a test for Foo
public partial class FooTest { ... }

The class may contain methods annotated with the PexMethod. Pex also understands SetUp and TearDown methods.


See Also

Settings Waterfall, PexMethodAttribute

Test To Code Binding


Pex lets specify the code under test for a particular assembly or fixture, i.e. the test to code binding.

This information is very interesting in many aspects:

  • for you,
    • it expresses explicitly the intent of the developer/tester,
    • it can be used through the command line to filter tests to run,
  • for Pex,
    • focus it's search on the code under test,
    • instrument the code under test,
    • tell the wizard where to add generated files,
    • provide coverage numbers with respect to the code under test,
  • for other tools
    • e.g. which tests to rerun after code has changed.

Assembly Under Test

The PexAssemblyUnderTest attribute can be used to specify that an assembly MyAssembly is tested by the current test project:

[assembly: PexAssemblyUnderTest("MyAssembly")]

Type Under Test


The type under test for a given fixture can be set through one of the PexClass constructors:

[TestClass, PexClass(typeof(Foo))]
public partial class FooTestClass
{ ... }




[assembly: PexAllowedExceptionFromTypeUnderTest(typeof(ArgumentException))]




[assembly: PexAllowedContractRequiresFailureAtTypeUnderTestSurface]

Coverage


Dynamic Coverage


As a side effect of the runtime monitoring, Pex computes collects dynamic code coverage data. We call it dynamic because Pex knows only about code that has been executed, therefore it cannot give absolute values for coverage such as other coverage tool usually do. For example, when Pex reports that the dynamic coverage as 5/10 basic blocks, then this means that 5 blocks out of 10 were covered, where 10 is the total number of blocks in all methods that have been reached so far by the analysis. (As opposed to all methods that exist in the assembly-under-test.) Later in the analysis, not only the nominator (here: 5), but also the denominator (here: 10) can increase, when the analysis discovered more reachable methods.

Coverage Domains


Pex partitions code into the following coverage domains: user code under test, user or test code or system code.
  • user code under test: this is the code under test for the current exploration. This code is included in the computation of the coverage numbers (block counts, etc...) and the source coverage will be rendered in the reports. Usually, this is the product code.
  • user or test code: this is code that is part of your projects or tests but that is not tested by the current exploration. This code is not included in the computation of the coverage numbers but the source coverage is still rendered in the reports (with different colors). Usually, this is the test code since you don't care about your test coverage but yet it is interresting to see the coverage of tests.
  • system code: any framework or third code for which you do not want to collect coverage data. This code is not included in the coverage numbers and source coloring.

To change the defaults, use attributes deriving from PexCoverageFilterAttributeBase or the Type Under Test feature.

Coverage Units


These are the different ways that Pex uses to characterize coverage:
  • blocks, basic blocks,
  • method touched, the number of methods that were touched at all.

Sample


Let's assume we have the following code given.

    class SystemCode {
        public void Run() {
            Console.WriteLine("I should show NOT show up!");
        }
    }
    class UserOrTestCode {
        public void Run() {
            bool b = true;
            if (b)
                Console.WriteLine("I should show up blue!");
            else
                Console.WriteLine("I should show up gray!");
        }
    }
    class UserCodeUnderTest {
        public void Run() {
            bool b = true;
            if (b)
                Console.WriteLine("I should show up green!");
            else
                Console.WriteLine("I should show up red!");
        }
    }
Let's consider the following simple exploration (without any parameter), to illustrate the coverage reports:
    [TestClass]
    [PexClass(
        // type under test is in UserCodeUnderTest domain
        typeof(UserCodeUnderTest), 
        Suite = "checkin")]
    // UserOrTestCode is the default domain
    // [PexCoverageFilterType(PexCoverageDomain.UserOrTestCode, typeof(UserOrTestCode))]
    [PexCoverageFilterType(PexCoverageDomain.SystemCode, typeof(SystemCode))]
    public partial class CoverageFilterTest {
        [PexMethod]
        public void CallExcludeMe() {
            new UserCodeUnderTest().Run();
            new UserOrTestCode().Run();
            new SystemCode().Run();
        }
    }

The resulting coverage is as follows:

coveragecolors.png

See Also

PexCoverageFilterTypeAttribute, TestClassAttribute, PexClassAttribute, PexMethodAttribute

PexMethodAttribute


This attribute marks a method as a parameterized unit test. The method must reside inside a class marked with PexClass attribute.

Pex will generate traditional, parameterless tests, which call the parameterized unit test with different parameters.

The parameterized unit test
  • must be an instance method,
  • must be visible to the test class into which the generated tests are placed according to the Settings Waterfall,
  • may take any number of parameters,
  • may be generic.

Example 

[PexClass]
public partial class MyTests {
     [PexMethod]
     public void MyTest(int i)
     { ... }
}

This attribute inherits from the PexSettingsAttributeBase and contains may named parameters for customization.

See Also

PexClassAttribute, Settings Waterfall, Generic Parameterized Unit Testing

The "Hello World" of Pex


Since Pex finds inputs relevant to the tested program, we can use Pex to generate the famous Hello World! string. We assume that you have created a C# MSTest Test Project and added a reference to Microsoft.Pex.Framework. If you are using another test framework, create a C# class library and refer to the test framework documentation on how to set up the project.

The example below creates a couple of constraints on the parameter called value so that Pex will generate the desired string.

using System;
using Microsoft.Pex.Framework; 
using Microsoft.VisualStudio.TestTools.UnitTesting; 
 
[TestClass]
public partial class HelloWorldTest {
    [PexMethod]
    public void HelloWorld([PexAssumeNotNull]string value) {
        if (value.StartsWith("Hello")
            && value.EndsWith("World!")
            && value.Contains(" "))
            throw new Exception("found it!");
    }
}

Once compiled and executed, Pex generates a set of tests such as the following:

Test Numbervalue
1""
2"\0\0\0\0\0\0"
3"Hellol"
4"HellolWorld!"
5"Hello World!"

We have a winner. In fact, the generated tests code should include a test like the following:

[TestMethod()]
[PexRaisedException(typeof(Exception))]
public void HelloWorld05()
{
    this.HelloWorld("Hello World!");
}

See Also

TestClassAttribute, PexClassAttribute, PexMethodAttribute

Assumptions and Assertions


Users can use assumptions and assertions to express preconditions (assumptions) and postconditions (assertions) about their tests. When Pex generates a set of parameter values and 'explores' the code, it might violate an assumption of the test. When that happens, Pex will not generate a test for that path but silently ignore it.

Assertions are a well known concept in regular unit test framework, so Pex already 'understands' the built-in Assert classes provided by each supported test framework. However, most framework do not provide an Assume class. In that case, Pex provides the PexAssume class. If you do not want to use an existing test framework, Pex also has the PexAssert class.

[PexMethod]
public void Test1(object o) {
    // precondition: o should not be null
    PexAssume.IsNotNull(o);
 
    ...
}

In particular, the non-nullness assumption can be encoded as custom attribute:

[PexMethod]
public void Test2([PexAssumeNotNull] object o)
// precondition: o should not be null
{
   ...
}

See Also

PexClassAttribute, PexMethodAttribute, PexAssumeNotNullAttribute

Generic Parameterized Unit Tests


Parameterized unit tests can be generic methods. In that case, the user has to specify the types used to instantiate the method using the PexGenericArguments attribute.

[PexClass]
public partial class ListTest {
    [PexMethod]
    [PexGenericArguments(typeof(int))]
    [PexGenericArguments(typeof(object))]
    public void AddItem<T>(List<T> list, T value)
    { ... }
}

See Also
PexMethodAttribute

Papers


Research Papers


  • Pex – White Box Test Generation for .NET link 
    • Nikolai Tillmann, Jonathan de Halleux, Proc. of TAP 2008, the 2nd International Conference on Tests and Proofs, LNCS, vol. 4966, pages 134-153, April 2008.
  • Parameterized Unit Testing with Pex (Tutorial) link 
    • Jonathan de Halleux, Nikolai Tillmann, Proc. of TAP 2008, the 2nd International Conference on Tests and Proofs, LNCS, vol. 4966, pages 171-181, April 2008.
  • DySy: Dynamic Symbolic Execution for Invariant Inference PDF 
    • Christoph Csallner, Nikolai Tillmann, Yannis Smaragdakis, Microsoft Research Technical Report MSR-TR-2007-151, November 2007.
  • Demand-Driven Compositional Symbolic Execution PDF 
    • Saswat Anand, Patrice Godefroid, Nikolai Tillmann, Microsoft Research Technical Report MSR-TR-2007-138, October 2007.
  • Unit Tests Reloaded: Parameterized Unit Testing with Symbolic Execution
    • Nikolai Tillmann, Wolfram Schulte, IEEE Software , vol. 23, no. 4, pp. 38-47, Jul/Aug, 2006.
    • Earlier version as Microsoft Research Technical Report MSR-TR-2005-153 PDF , March 2006.
  • Discovering Likely Method Specifications PDF 
    • Nikolai Tillmann, Feng Chen, Wolfram Schulte, Technical Report MSR-TR-2005-146, March 2006.
  • Mock-object generation with behavior link 
    • Nikolai Tillmann, Wolfram Schulte, Proc. of ASE 2006 , pp. 365-368, 2006.
  • Parameterized Unit Tests PDF 
    • Nikolai Tillmann, Wolfram Schulte, Proc. of FSE/ESEC 2005 . Earlier version as Microsoft Technical Report MSR-TR-2005-64, May 2005.


Other Papers


Attribute Glossary


By Namespaces



Inheritance Tree


PexAssume


Static class to express assumptions, i.e. a precondition, in parameterized unit tests. The methods of this class can be used to filter out undesirable test inputs.

If the assumed condition does not hold for some test input, a PexAssumeFailedException is thrown, which will cause the test to be silently ignored.

Example

The following parameterized test will not consider j=0.

public void TestSomething(int i, int j) {
     PexAssume.AreNotEqual(j, 0);
     int k = i/j;
     ...
}

Remarks


The code above is almost equivalent to
     if (j==0)
          return;
except that a failing PexAssume results in no test cases, whereas in the case of an if-statement, Pex would generate a separate test case to cover the then-branch of the if-statement.

PexAssume also contains specialzed nested classes for assumptions on string, arrays and collections.

See Also


PexAssert, PexSymbolicValue

MbUnit


Open Source Test Framework: http://www.mbunit.com 

Pex can leverage already existing test suites, and can generate tests for MbUnit.

Test Inputs


Pex generates test inputs.

Inputs to a test come from various sources:
Constraint Solver

Pex uses a constraint solver to determine what the relevant input values of a test and the program-under-test are.

Pex uses Z3 as a constraint solver.

Path Condition


During Input Generation, Pex runs a parameterized unit test multiple times to determine relevant test inputs. For each run, Pex computes the abstract condition over the inputs that characterizes the execution path the program takes. This abstraction condition is called the path condition. It is a boolean expression which may refer to the test inputs.

For example, for the method
  [PexMethod]
  public void Test(int i) 
  {
      if (i>0) 
          Console.WriteLine("positive");
  }
Pex will try to test inputs, which might be:
  • Test(-1), which can be characterized by the condition i<=0, and
  • Test(0), which can be characterized by the condition i>0.

Together, these two exemplary test inputs are representative for all different behaviors of the called method.

When you look at a test report, you have the option to view the path condition
PathCondition0.png

When you expand the [+], you see a code snippet, which represents a boolean-valued expression that involves the parameter names of the parameterized test.
PathCondition1.png

Pex simplifies and rearranges the conditions internally; here, you can see that instead of i<=0 Pex represented the condition as 0>=i.
Also, the code shown for the path condition might not be executable as is, or look suboptimal.

Generating Integers and Floats


Pex' constraint solver determines test input values of primitives types such as byte, int, float, ... in order to trigger different execution paths of the test and the program-under-test.

For integers, the constraint solver can reason about all arithmetic operations, treating integers as 32-bit or 64-bit values. Bitwise manipulations are supported as well.

For floating point number, the constriant solver approximates the behavior of linear arithmetic with rational numbers.

Enums are treated similar to their underlying integer type.

Generating Objects


Pex can either create instances of existing .Net classes, or you can use Pex to automatically create mock objects that implement a given interface and behave in different ways depending on its usages.


When Pex generates test inputs, it imposes certain bounds on the size of the inputs. Pex only considers a set of types when trying to build values which are assignable to the test parameters.

Generating Structs


Pex reasoning about struct-values is similar to how it deals with objects.

Arrays, Strings


Pex monitors the executed instructions when it runs a test and the program-under-test. In particular, it observes when the program depends on the length of a string or an array (and the lower bounds and lengths of a multi-dimensional array). It also observes how the program uses the different elements of a string or array. It then uses a constraint solver to determine which lengths and element values might cause the test and the program-under-test to behave in interesting ways.

Pex tries to minimize the size of the arrays and strings needed to trigger interesting program behaviors.

PexChoose


Static class which supplies auxiliary input values to a test, as well as the choices which determine the behavior of parameterized mocks.

(This choice provider does not decide whether a test passes for particular input values, it simply provides input values, i.e. choices. It is still up to the user to restrict the input values, and to write assertions to define when a test passes or fails.)

Modes of operation


The PexChoose class can operate in two modes:
  • While Pex is performing a symbolic analysis of the test and the tested code during Input Generation, the chooser returns arbitrary values, and Pex tracks how the value is used in the test and the tested code. Pex will generate relevant values to trigger different execution paths in the test and the tested code.
  • The generated code for particular test cases sets up the choice provider in a specific way, so that the reexecution of such a test case will make particular choices to trigger a particular execution path.

Usage


  • If you want to use the choice provider to determine the behavior of a method (e.g. of a mock object), you can call PexChooser.FromCall, which returns a chooser.
public int Foo() {
    var chooser = PexChoose.FromCall(this);
    return chooser.ChooseResult<int>();
}
  • If you want to draw an auxiliary input value (or a sequence of auxiliar input values), you can call PexChoose.CreateSession, which returns a choice session.
    • You can use the static PexChoose.DefaultSession if a single static session works for you.
public void Test() {
    ArrayList list = new ArrayList();
    while(PexChoose.DefaultSession.ChooseValue<bool>("next"))
        list.Add(null);
    ...
}


See Also

Parameterized Mocks, IPexChoiceSession

Parameterized Mocks


How to test a method which has a parameter of an interface type? Or of a non-sealed class? We don't know which implementations will later be used when this method is called! And maybe we don't even have any real implementation available at test time.

The conventional answer: mock objects with explicit behavior

A mock object implements an interface (or extends a non-sealed class). It does not represent a real implementation, but just a shortcut that allows the execution of tests using the mock object. It's behavior is manually written as part of the each test case where it is used. Many tools exist which make it easier to write such mock objects and their expected behavior. But it must still be written by hand.

Parameterized Mocks

Pex mocks have two different execution modes:

  • choosing, when exploring code, Pex mocks are a source of additional test inputs, and Pex will try its best to choose interesting values,
  • replay, when executing a previously generated test, Pex mocks behave like stubs with behavior (i.e. predefined behavior).

Example

Let's illustrate this with a simple mock of a toy interface INamed:

interface INamed {
    string GetName();
}

Writing the mock

The mock for this interface looks as follows:

class MNamed : INamed {
    public string GetName() {
        var call = PexChoose.FromCall(this);
        return call.Result<string>();
    }
}

So what did we do really... The mock implementation of GetName fetches a choice provider(i.e. an interface from which new values can be queried). 

    var call = PexChoose.FromCall(this);

The choice provider can be used to choose new values. It's like adding parameters to the test, but not through the signature. In this case, we ask Pex to get a new result value. 

    return call.Result<string>();

Let's try it!

The following test takes a INamed instance (which we assumed to be non-null) and displays a message on the console if the name is 'Marc'. Notice that the test was also tagged with the PexUseType to tell Pex that the MNamed type can be used, which will be needed to get a INamed instance.

[PexMethod]
public void GetName() {
    var name = new MName();
    if (name.GetName() == "Marc")
        Console.WriteLine("hello marc");
}

Generated tests

Pex generates 2 unit tests that cover that method.

The first test has GetName return a default value. The second generated test is more interesting as it shows how Pex sets up the behavior of the replay stub:

// test 2
MockTest.MNamed mn0 = new MockTest.MNamed();
var chooser = PexChoose.NewTest();
chooser.OnCall(0, "MNamed.GetName()")
      .Returns("Marc");
this.GetName();

The chooser instance is used to set up the result value on the first call to GetName:
// on the call '0' to the method GetName of MockType.MNamed,
choose.OnCall(0, "MNamed.GetName()")
// return "Marc"
      .Returns("Marc");

Adding behavior

Behavior can simply be added to mock as code since Pex will explore the mock code as well. For example, let's refine the MNamed implementation to always return the same name:

class MNamed : INamed {
    private string name;
    public string GetName() {
        if(this.name == null)
            this.name = PexChoose.FromCall(this).ValueNotNull<string>("name");
        return this.name;
    }
}

Note that we no longer choose a result value, but make a named choice (with the name 'name'). It doesn't matter much to Pex, it just changes the generated code that sets up the mock objects.

More on mocks

The following topics discuss how to mock particular elements:


See Also

Martin Fowler's Mocks Aren't Stubs , AppendFormat.

xUnit.Net


Unit test framework

In this mode, Pex emits a new file and entry point for each test. It duplicates all the necessary attributes so that there is no dependency on Microsoft.Pex.Framework.

NUnit


Open Source Test Framework: http://www.nunit.org 

Pex can leverage already existing test suites, and can generate tests for NUnit.

TestFramework


Option of the PexAssemblySettingsAttribute to specify the test framework to be used. Values for this parameter are built dynamically, please consult command line help.

See Also
Supported Test Frameworks

PexAssemblySettingsAttribute


This attribute can be set at the assembly level to override default settings value for all explorations. It inherits from the PexSettingsAttributeBase.

using Microsoft.Pex.Framework;
// overriding the test framework selection
[assembly: PexAssemblySettings(TestFramework = "Naked")]

Options specific to this attribute:

See Also

Settings Waterfall
This namespace contains a meta data model of the CLR. Parts of it are quite similar to the standard reflection library, but it goes further in many ways:

  • It describes the type system from the point of view of the execution engine, which includes explicit box types and information about memory layouts
  • It decodes the instruction stream, and provides a sequence of instructions as well as a basic-block representation
  • It decodes signature blobs
  • It can perform operations which are normally hidden by the execution engine, e.g. vtable-lookups
  • It includes facilities to create types which can be used to instantiate generic types whose type parameters have constraints
  • It aggressively caches data, and works around some quirks in the standard reflection implementation
  • In the following, the core concepts of the library are presented in more detail.

In order to reflect over instruction sequences, it also contains the concepts:

This namespace contains various utilities for fast and type-safe access to "live" program data without the overhead of boxing that is normally incurred when using standard reflection for this purpose. (Basically, it generates specialized code with Reflection.Emit for all types.)
This namespace contains an abstract model of the data-manipulating operations of the CLR, where all values are tracked as terms.

Concepts:



This namespace also contains visitors and pretty-printers for terms.
The Microsoft-branded version of CIL.
This namespace defines the notion of a formula, and the concept of a solver.
This namespace contains the Monitoring.Controller, which can be used to start and stop the monitoring callbacks, and to setup a process for monitoring.

This module also contains some other internal concepts:
  • Static callbacks which delegate to a user-provided Execution Monitor.
  • Substitutions which emulate the behavior of method calls but drive a user-provided Execution Monitor in addition.
Since all standard assemblies like mscorlib and System may be instrumented, interesting situations arise when the monitoring callbacks perform rather simple operations which in turn lead to calls into mscorlib or System.
Fortunately, Microsoft.ExtendedReflection provides a shield which deals with such re-entrance problems.

Still, this shield comes with a performance overhead.

The utilities of Microsoft.ExtendedReflection provide alternatives to methods of the standard libraries (just as the extended metadata is an alternative to the standard reflection library).

In particular:
  • Utilities.Safe.Collections contains a set of collection types which are safe from instrumentation (and therefore faster). This set of types include many commonly desired collection types which cannot be found in the standard System.Collections.Generic namespace.
  • Utilities.Safe.Diagnostics provide alternatives to the Debug and Debugger class of the standard System.Diagnostics namespace.

Overview


The ClrMonitor is an unmanaged COM component that implements the CLR profiling API. It uses this API mainly to rewrite MSIL instructions of selected methods, types or assemblies on-the-fly at JIT time. It can redirect calls and insert callbacks in the MSIL instruction sequence, enabling the observation of the execution of the program at a fine grained level:

  • (Static) calls can be redirected. The redirection target may call the original call target.
  • Similar to the standard CLR profiling API, the ClrMonitor monitors when a method is entered or exited.
  • It also monitors the concrete parameter values that are passed to a monitored method.
  • The execution of every instruction can be monitored.
  • The control flow is monitored, i.e. the evaluation of all explicit conditional branches, and of all implicit checks that can cause exceptions.
  • Every monitored event causes a callback into the core Microsoft.ExtendedReflection assembly, which can dispatch the callbacks to a user-provided Execution Monitor.

Code instrumentation


The instruction sequence of each instrumented method is rewritten. It starts by inserted instructions which check whether monitoring is currently on. If not, the original instructions are executed. It if it turned on, the instrumented version of the instructions is execution, starting with a callback to EnterMethod(m, c), and eventually finished by a callback to LeaveMethod(m), where m identifies the current method, and c is the number of branch identifiers that the instrumented code will refer to within the method body.

EnterMethod returns a Boolean value that indicates whether the monitor is interested in the concrete arguments to the method. If it returns true, a sequence of calls to Argument<T>(i, v), ArgumentPtr(i, v, t), ArgumentTypedReference(i, v) and ArgumentByRef<T>(i, a) is inserted, one for each argument, where i is the index of the argument, v is a value, t a type, and a a managed pointer.

Each exception filter starts with a callback to StartFilter(r) where r is the reference to the exception object that is currently being filtered. Each exception handler starts with a callback to StartExceptionHandler(r).

Each instruction that can throw a NullReferenceException, InvalidCastException, IndexOutOfRangeException, ArrayTypeMismatchException, DivideByZeroException or OverflowException is immediately followed by a callback that indicates that the instruction did not throw the exception. Also, all such instructions are surrounded by an exception handler, that catches the corresponding exception type, performs a callback to a method that indicates that the exception was thrown, and rethrows the exception.

See the file checks.def in the Microsoft.ExtendedReflection.ClrMonitor project for detailed information about which instructions may throw which exceptions.

In general, each instruction causes a callback named after the instruction itself. The callback is issued before the execution of the actual instruction.

In order to capture all relevant information to track the execution path taken by the program, some instructions get a special treatment.

Substitutions


Call instruction in instrumented MSIL code can be redirected. Read more here.

Setup


In order for code to be monitored, certain environment variables must be set before the process starts:

COR_ENABLE_PROFILING=1
COR_PROFILER={C1DAAFC4-10C6-4838-9F89-435E2120F5F1}


CLRMONITOR_FLAGS={flags that decide the extend of the instrumentation}


  • which types should be protected?
CLRMONITOR_PROTECT_TYPES={comma-separated list of type names; case matters; generic types must end in '`n' annotations; nested types are separated by '+'; <Module> stands for all module-level members}

  • which type and assemblies should be instrumented?
CLRMONITOR_INSTRUMENT_TYPES={comma-separated list of type names; case matters; generic types must end in '`n' annotations; nested types are separated by '+'; <Module> stands for all module-level members}
 
CLRMONITOR_INSTRUMENT_ASSEMBLIES={comma-separated list of display names of assemblies; case does not matter; use '*' for all assemblies}
 
CLRMONITOR_INSTRUMENT_TYPES_EXCLUSIONS={list of types which should not be instrumented, despite the above}
 
CLRMONITOR_INSTRUMENT_ASSEMBLIES_EXCLUSIONS={list of assemblies which should not be instrumented, despite the above}
 
CLRMONITOR_DISABLE_MSCORLIB_SUPPRESSIONS=1, disable mscorlib exclusions. Use with *Great* care.

  • which types and assemblies should be instrumented so that values can be injected at any place in the execution
CLRMONITOR_INJECT_TYPES={comma-separated list of type names; case matters; generic types must end in '`n' annotations; nested types are separated by '+'; <Module> stands for all module-level members}
 
CLRMONITOR_INJECT_ASSEMBLIES={comma-separated list of display names of assemblies; case does not matter; use '*' for all assemblies}
 
CLRMONITOR_INJECT_TYPES_EXCLUSIONS={list of types which should not be instrumented, despite the above}
 
CLRMONITOR_INJECT_ASSEMBLIES_EXCLUSIONS={list of assemblies which should not be instrumented, despite the above}

  • which method calls should be substituted (redirected)?
CLRMONITOR_SUBSTITUTIONS={comma-separated list of file names, pointing to assemblies containing substitutions}

  • which instructions should be monitored by inserted callbacks?
See here for a detailed description of possible CLRMONITOR_FLAGS.

The class Monitoring.Controller in the Microsoft.ExtendedReflection project provides support to check if code in the current process can be monitored, and to setup monitoring for a new process.

Activation


There are two ways to direct the instrumented code's callbacks to a user-written managed class:

  • In a running process, the Monitoring.Controller class provides Start and Stop methods to direct the callbacks to a particular Execution Monitor and to stop the redirection.
  • When the following environment variables are set, a user-provided Execution Monitor is loaded automatically into any monitored process. Note that in addition to setting up the environment variables, the Microsoft.ExtendedReflection assembly must either be in the monitored process' application directory, or in the GAC.

CLRMONITOR_USER_ASSEMBLY={file name of assembly containing [Execution Monitor]}
 
CLRMONITOR_USER_TYPE={type in assembly implementing [Execution Monitor]}

Logging (Only available in Debug-builds)


If compiled in Debug configuration, setting the environment variable

CLRMONITOR_LOGFILE={filename}
CLRMONITOR_VERBOSE=1

causes detailed information about the code instrumentation to be stored in the indicated file.


Debugging (Only available in Debug-builds)


If set, this environment variable will cause the ClrMonitor to break into the debugger when launched.

CLRMONITOR_BREAK=1


Loading your own profiler


When the environment variables are generated through the managed API, Extended Reflection sets the following environment variable with the profiler CLSID.

CLRMONITOR_CLSID={...}

In Pex, one can use the /AllowLoadingProfiler to authorize this kind of profiler 'chaining':
  • enable your own profiler by setting the COR_PROFILER environment variables,
    • do not turn on COR_PROFILER_ENABLED! Pex will enable it when launching the monitored process.
  • use the CLSID from CLRMONITOR_CLSID to create the Extended Reflection profiler and delegates the profiling APIs
  • in the pex command line, use the /AllowLoadingProfiler to enable this mode. In that case, Pex will not modify the value of COR_PROFILER.

Code Substitutions


Some methods are problematic for Pex' symbolic analysis:
  • methods implemented by native code (x86, X64)
  • method calls going through remoting
  • managed code which is not instrumented (e.g. some parts of mscorlib cannot be instrumented)

The Microsoft.ExtendedReflection library has several ways to deal with this problem.

Visual Studio Shortcuts


Pex Shortcut Description
Ctrl + E, E Run Explorations in Current context
Ctrl + E, P Run Explorations in Current project
Ctrl + E, Ctrl + E Run Explorations in the Last Pex Run

Limitations


This page contains a list of situations and problems that Pex does not handle currently:

Nondeterminism


Pex assumes that the analyzed program is deterministic. If it is not, Pex will go in cycles until it hits exploration bounds.

Concurrency


Pex does not handle multithreaded programs.
(It might work in a scenario where the main thread execution is deterministic, independent of the behavior of other spawned threads.)

Native Code, .NET code that is not instrumented


Pex does not understand native code, e.g. x86 instructions called through P/Invoke, i.e. Pex does not know how to translate such calls into constraints that can be fed to the constraint solver. And even for .Net code, Pex can only analyze code it instruments. Pex cannot instrument certain parts of mscorlib, including the reflection library. DynamicMethod cannot be instrumented. (The suggested workaround is to have a test mode where such methods are in types in a dynamic assembly.) Future versions of Pex will have support for some of these cases.

However, even if some methods are uninstrumented, Pex will still try to cover the instrumented code as much as possible.

Platform


At this time, we only support Pex on the X86, 32-bit .NET framework.

Language


In principle, Pex can analyze arbitrary .NET programs, written in any .NET language.
However, the VS AddIn and the code generation are only fully implemented for C#.

Symbolic Reasoning


Pex uses an automatic constraint solver to determine which values are relevant for the test and the program-under-test. However, the abilities of the constraint solver are, and always will be, limited.

(Slightly) incorrect stack traces


Because Pex catches and 'rethrows' exceptions in each instrumented method, the line numbers in stack traces will not be correct. This is a (by design) limitation of the 'rethrow' instruction.

.NET 1.0 and 1.1 modules


Pex injects generic callbacks when rewriting the IL method bodies. This has a side effect that it cannot instrument v1.0 and v1.1 .net module because their metadata models do not support generics.

Creating a Pex Project in Visual Studio


This quick start shows how to create an empty Pex test in a new test project in Visual Studio.

  • Start Visual Studio.
  • Create a new test project that uses your favorite test framework (see Supported Test Frameworks).
  • Add a reference to Microsoft.Pex.Framework:
addpexreference.png

Create a new PexClass


  • Click on the 'New Item' menu item
newpexitem.png
  • Select 'New Pex Test (xxx)' where xxx is you test framework. Choose a name, and you will get a PexClass with a PexMethod:
[TestClass]
[PexClass]
public partial class MyPexClass
{
    [PexMethod]
    public void Test(int i)
    {
        // add parameterized test here
    }
}

Tell Pex what to monitor 


// monitor types in MyProduct.dll
[assembly: PexInstrumentAssembly(typeof(SomeTypeInMyProduct))]

And then: Generate Tests!

Click Here to Continue

Generating Tests


We assume that you created a Pex project in Visual Studio.

Tutorial: Generating Tests with Pex on the Command-Line


This this tutorial shows you how to test code from the command-line.
We will generate test cases for the following little class:

public static class StringHelper
{
    public static string ReplaceFirst(string s, char c)
    {
        return c + s.Substring(1);
    }
}

Tell Pex what to monitor 


// monitor types in MyLibrary.dll
[assembly: PexInstrumentAssembly(typeof(StringHelper))]

Create a new PexClass


  • On the test-project, click on the 'New Item' menu item
newpexitem.png
  • Select 'New Pex Test (xxx)' where xxx is you test framework. We will name our test class StringHelperFixture:
[TestClass, PexClass]
public partial class StringHelperFixture
{
    [PexMethod]
    public void MyPutTest(int i)
    {
        // add parameterized test here
    }
}

  • Refactor MyPutTest to call StringHelper.ReplaceFirst.
[PexMethod]
public void ReplaceFirst(string value, char c)
{
    // invoke method under test with parameter values
    string result = StringHelper.ReplaceFirst(value, c);
 
    // verify assertions
    if (!String.IsNullOrEmpty(value))
    {
        // first character was replaced
        Assert.AreEqual(c, value[0]); 
        // the rest of the string is not modified
        Assert.AreEqual(value.Substring(1), result.Substring(1)); 
    }
}

Explore through the Command Line


  • Open a command window and move to your build folder
  • Execute the following command (the command line supports a rich set of flags, see Command Line for information).
"%programfiles%\microsoft pex\bin\pex.exe" MyLibrary.Tests.dll
Pex: Program Exploration Framework for .Net
Copyright (c) Microsoft Corporation. All rights reserved.
Microsoft Confidential - for Internal Use Only
 
instrumenting... launched Pex x86 Edition
(...)
15:08:55.04> MyLibrary.Tests
  15:08:55.05> MyLibrary.Tests.StringHelperFixture
    15:08:55.08> ReplaceFirst(String, Char)
      [test] ReplaceFirstStringChar_61102_150857_0, System.NullReferenceException: Object reference not set to an instance of an object.
      [test] ReplaceFirstStringChar_61102_150858_1, System.ArgumentOutOfRangeException: startIndexcannot be larger than length of string.
Parameter name: startIndex
(...)
15:08:59.21> Finished execution: 1 explorations, 0 failures, 2 generated tests (1 failures, 0 duplicates), 00:00:07.3567
(...)
  EXPLORATION SUCCESS

You can see that Pex generates 2 tests to cover our method, passing a null string and a string of length 0. This is sufficient to cover the 'buggy' implementation of ReplaceFirst. Later in this tutorial, we will fix the implementation, and see how pex generates new tests to cover the changes.

Using the exploration Reports


The pex command line automatically opened an HTML exploration report. This report contains all the information about the test generation, the explorations and the coverage.
reporttestdetails.png

Fixing the implementation and rerunning Pex


We add some parameter validing in ReplaceFirst and re-execute pex:

public static string ReplaceFirst(string s, char c)
{
   if (String.IsNullOrEmpty(s))
   throw new ArgumentNullException("s");
   if (s.Length == 1)
       return c.ToString();
   else
       return c + s.Substring(1);
}


"%programfiles%\microsoft pex\bin\pex.exe" MyLibrary.Tests.dll
Pex: Program Exploration Framework for .Net
(...)
15:12:44.78> MyLibrary.Tests
  15:12:44.80> MyLibrary.Tests.StringHelperFixture
    15:12:44.83> ReplaceFirst(String, Char)
      [test] ReplaceFirstStringChar_61102_151247_0, System.ArgumentNullException: Value cannot be null.
Parameter name: s
      [test] ReplaceFirstStringChar_61102_151248_1
      [test] ReplaceFirstStringChar_61102_151248_2
        [instrumentation] System.Char.ToString not instrumented
        [instrumentation] System.String.Concat not instrumented
(...)
15:12:49.61> Finished execution: 1 explorations, 0 failures, 3 generated tests (0 failures, 0 duplicates), 00:00:08.0440
940
(...)
  EXPLORATION SUCCESS

The generated tests look as follows (for 100% coverage!):

public partial class StringHelperFixture
{        
    [TestMethod]
    [ExpectedException(typeof(System.ArgumentNullException))]
    public void ReplaceFirstStringChar_61102_151247_0()
    {
        this.ReplaceFirst(((string)(null)), '\0');
    }
    [TestMethod]
    public void ReplaceFirstStringChar_61102_151248_1()
    {
        string s0 = "x";
        this.ReplaceFirst(((string)(s0)), 'x');
    }
    [TestMethod]
    public void ReplaceFirstStringChar_61102_151248_2()
    {
        string s0 = "xx";
        this.ReplaceFirst(((string)(s0)), 'x');
    }
}

Looking at code coverage in the reports


In the reports, you can verify that we actually fully cover ReplaceFirst by clicking on the 'coverage' link, and selecting StringHelper.cs:
replacefirstcoverage.png

See Also

PexInstrumentAssemblyAttribute, PexClassAttribute, TestClassAttribute,PexMethodAttribute

Test Generation


In traditional unit testing, it takes several ingredients to put together a test:

[Test]
void MyTest() {
    // data
    ArrayList a = new ArrayList();
 
    // method sequence
    a.Add(5);
 
    // assertions
    Assert.IsTrue(a.Count==1);
    Assert.AreEqual(a[0], 5);
}

The test consists of different aspects.


Pex can often automatically determine relevant argument values for more general Parameterized Unit Tests, which give the sequence of method calls and assertions.

Instrumented Assemblies and Types


Pex generates test inputs by monitoring executions of .Net applications. Pex requires the user to specify which parts of the code it should monitor. When a test (indirectly) calls an uninstrumented method, Pex might give a Uninstrumented Method Called warning.

Pex can only reason about the code it monitors. It is important to understand the trade-offs between monitoring enough code to capture the behavior of your application and not too much to avoid slowing down the execution too much:
  • monitoring requires an 'heavy duty' code instrumentation which increase jitting time and degrades performance. For example, if the List<> class is instrumented, all your collections will be monitored!
  • the more things we monitor, the more constraints we gather and hand to our constraint solver. This will increase exploration time.
    • Pex also provides an extended instrumentation mode that makes the code mockable. In that mode, method or constructor calls cannot be 'hijacked', constants can be replaced etc... This mode is even more impactfull on performance.
  • Pex does not know about things that happen in code that is not monitored. Therefore, it cannot generate test cases that thoroughly exercise code paths in unmonitored code.
  • The assemblies/types to instrument can be set through attributes and the command line. The default behavior is specify each assembly/type to instrument. However, it is possible provide wildcards such as * to specify all assemblies/types.

Attributes



Instrumented By Default


The following assemblies/types are instrumented by default for your convenience:

  • the assembly containing the Pex classes (You can disable this using the command line option /a-).
  • the assertion and assumption types of your test framework.

Native Code


Pex cannot instrument native (x86) code. However, Pex has a set of mechanisms to describe the behavior of native code by Code Substitutions.

Command Line


/instrumentedassemblies:<string> where <string> is a semi-column separated list of assembly names,

Extensibility


If you want to implement your own attributes to specify assemblies or types to instrument, you simply need to create attributes that inherit from PexInstrumentAssemblyAttributeBase for assemblies and PexInstrumentTypeAttributeBase for types.

See Also

PexInstrumentAssemblyAttribute, PexInstrumentNamespaceAttribute, PexInstrumentTypeAttribute, PexInstrumentMarkedByAttribute

Test Generators


Pex generates test cases by selecting a sequence of methods of the implementation-under-test to execute, and then generating inputs for the methods while checking assertions over the derived data.

A parameterized unit test directly states a sequence of method calls in its body.

When Pex needs to construct objects, calls to constructors and factory methods will added automatically to the sequence as needed.

The generation of inputs and assertion checking can be controlled with further decoration attributes.

See Also

PexClassAttribute, PexExplorationAttributeBase, PexMethodAttribute

Exploration of Existing Unit Test


Pex supports a special mode where it executes existing unit test suites, i.e. Pex will run an existing unit tests in a similar fashion as the test harness.

Applying Pex on an existing unit test suite has many applications:

Command Line 


pex.exe /erm:unittest myunittests.dll

One can also refer to another assembly that contains additional settings. This is particularly useful to specify coverage and user assemblies.

Limitations


  • MSTest is directly supported
  • Unit Test decorators such as ExpectedException are understood by Pex.

See Also

PexInstrumentAssemblyAttribute

Pruning By Assumptions


Pex provides a static class to express assumptions, i.e. pre-conditions, in parameterized unit tests, PexAssume.

If the assumed condition does not hold for some test input, a PexAssumeFailedException is thrown, which will cause the test to be silently ignored.

Example 

public void TestSomething(int i, int j) {
     PexAssume.AreNotEqual(j, 0);
     int k = i/j;
     ...
}

Remarks


The code above is almost equivalent to

     if (j==0)
          return;
except that a failing PexAssume results in no test cases, whereas in the case of an if-statement, Pex would generate a separate test case to cover the then-branch of the if-statement.

PexAssume also contains specialized nested classes for assumptions of string, arrays and collections.

See Also


PexAssert, PexChoose, PexObserve

Integers And Floats


Pex' constraint solver determines test input values of primitives types such as byte, int, float, ... in order to trigger different execution paths of the test and the program-under-test.

Objects


Pex can either create instances of existing .Net classes, or you can use Pex to automatically create mock objects that implement a given interface and behave in different ways depending on its usages.


When Pex generates test inputs, it imposes certain bounds on the size of the inputs. Pex only considers a set of types when trying to build values which are assignable to the test parameters.

Using Types


When Pex generates inputs, it uses an automatic constraint solver to determine what relevant input values are.

The constraint solver has certain built-in theories which can reason about how the program-under-test uses integer arithemtic and how it accesses memory. However, these theories handle only certain cases.

In order to create objects, Pex needs to know which types are available.

You can tell Pex which values to consider using the following attributes which derive from PexDomainAttributeBase.

Instantiating Existing Classes


What is the problem?
Pex monitors the executed instructions when it runs a test and the program-under-test. In particular, it monitors all field accesses. It then uses a constraint solver to determine new test inputs -- including objects and their field values -- such that the test and the program-under-test will behave in other interesting ways.

Thus, Pex needs to create objects of certain types set their field values.
If the class is visible and has a visible default constructor, Pex can create an instance of the class.
If all the fields of the class are visible, Pex can set the fields automatically.

If the type is not visible, or the fields are not visible, Pex needs help to create objects and bring them into interesting states to achieve maximal code coverage. (Pex could use reflection to create and initialize instances in arbitrary ways, but this is usually not desirable, since it might bring the object into a state which can never occur during a regular program execution. Instead, Pex relies on hints from the user to proceed.)

What can the user do to help Pex?
  • Explorables: You can use an attribute derived from PexExplorableAttributeBase.
    • Advantage: This attribute lets Pex create new objects by exploring its constructor or factory methods, which may validate arguments.
    • Disadvantage: This attribute does not yet support the creation of structs.
    • Disadvantage: Pex must explore more methods to create tests.
  • Creatables: If the object simply represents data, you can an attribute derived from PexCreatableAttributeBase to tell Pex how to create instances.
    • Advanced feature, it is not easy to configure creatable types correctly.
    • Disadvantage: There must be no restrictions on what data can be stored in the fields of the instance.
    • Advantage: When correctly configured, this attribute is very effective.
    • Advantage: This attribute can be used to create instances of structs as well as classes.

When Pex generates test inputs, it imposes certain bounds on the size of the inputs. Pex only considers a set of types when trying to build values which are assignable to the test parameters.

Creatables


Pex can reliably create values of all primitive types, arrays, and types with a visible constructors if all fields are either visible themselves, or can be unconditionally set via some visible property setter or method. However, if a value must be created in a more complicated way, e.g. by calling factory methods and setting properties that perform argument validation, then Pex needs more information.

Types representing data types are called 'creables'. This means that there is a direct mapping from a constructor or a factory method to the field of that type. Creatable types can be specified through attributes inherited from PexCreatableAttributeBase.

Note: Use this attribute only if Pex may set all fields of a class in any (type-correct) way. Consider using an attribute deriving from PexExplorableAttributeBase if in doubt.

  • creatable through public fields
public class Point {
    public int X,Y;
}
  • creatable through constructor
public class Point {
    public readonly int X;
    public readonly int Y;
 
    public Point(int x, int y) {
       this.X = x;
       this.Y = y;
    }
}
// binding
[PexCreatableByConstructor(typeof(Point), typeof(int), typeof(int))]
  • creatable through static method factory
public class Point {
    ...
    public static Point Create(int x, int y) {
       Point point = new Point();
       point.X = x;
       point.Y = y;
       return point;
    }
}
// binding
[PexCreatableByMethod(typeof(Point), "Create", typeof(int), typeof(int))]
  • creatable as singleton
public class Point {
     private Point() {...}
     public static Point Instance { get {...} }
}
// binding
[PexCreatableAsSingleton(typeof(Point), "Instance")]

Attributes

Pex comes with the following set of derived attributes:

Definining multiple creatables at once

If you want to specify that many types, which follow a common pattern, are creatable, such as Web Service data objects, see PexCreatableFactoryAttributeBase (and more specifically PexCreatablesAsXmlFromAssemblyAttribute).

See Also
IPexCreatable, IPexCreatableFactory

Explorables


Pex can reliably create values of all primitive types, arrays, and types with visible default constructors if all of their fields are visible. However, if an object must be created by calling a constructor or factory method that takes parameters, then Pex needs more information. (This way, Pex can even use types that are not visible.) In particular, Pex needs to know which constructor or factory method it should explore.

In general, a constructor might involve some control flow (parameter checking) or invoking different methods. Therefore, Pex needs to explore the constructor in addition to the actual test code. Types with constructors that involve control flow are called explorable because they need to be 'explored' in order to obtain interesting objects.

A classic example


Let's consider the following Account class; it has a money field which is not visible from the public context. In fact, the value of money is computed in the constructor of Account: 

public class Account {
    private float money;
    public Account(Bank bank, string name) {
        // control-flow in the constructor
        if (bank == null) throw new ArgumentNullException();
        if (name == null) throw new ArgumentNullException();
 
        // calls to other method
        this.money = bank.GetMoney(name);
    }
 
    public float Money { 
      get { return this.money; }
    }
}

We want to write a test that states that for any valid instance of Account, the value of money should be positive. With Pex, we can pass an Account instance as a test parameter:

// test that needs an instance of Account
[PexMethod]
public void NeedsAccount(Account a)  {
    Assert.IsTrue(a.Money >= 0);
}

To explore this test, Pex will need to create valid instances of Account. Since the state of Account cannot be set entirely from public fields, Pex needs to pick a constructor or a static method (or a sequence of constructor, methods, properties, etc...) to 'set' the state of Account to the value it has computed.

While Pex makes a smart guesses, you can configure yourself how Pex should create an instance of a type. (And configuring how to create a type yourself is the only way to suppress Pex' notifications about its guesses.)

// binding
[assembly: PexExplorableFromConstructor(typeof(Account), typeof(Bank), typeof(string))]

  • Using a method factory:
// load any factories from this assembly
[assembly: PexExplorableFromFactories]
...
// this type contains factories
[PexClassFactory]
public static class AccountFactory {
    // this is a factory that creates 'Account' instances
    [PexMethodFactory(typeof(Account))]
    public static Account Create(Bank bank, string name) {
       return new Account(bank, name);
    }
}

Attributes


Pex comes with the following set of derived attributes:

Restrictions


  • Pex will not explore all code paths of the constructor. In particular, it will suppress paths that throw an exception in the constructor. Therefore, separate parameterized tests should be written to exercise the constructor.
  • If another object is required by the constructor, Pex will first try to create that object, whose constructor might need another object, and so on.

See also


Creatables

Mocking Methods


This page gives guidance on how to properly mock methods using Pex. We will illustrate this page by mocking the following method:

public int Foo(object a, out string b, ref string c);

In order to mock a method, one has to do the following steps:
  • retrieve a choice session for the particular call,
var call = PexChoose.FromCall(this);
  • get values for the out parameters from the choice provider:
b = call.ChooseValueAtReturn<string>(2);
// you can also get a value for 'ref' parameters
  • get a result value and return it
return call.ChooseResult<int>();

The full (minimal) mock implementation of Foo looks as follow:

public int Foo(object a, out string b, ref string c) {
    var call = PexChoose.FromCall(this);
    b = call.ChooseValueAtReturn<string>(2);
    return call.ChooseResult<int>();
}

In general, only methods which pass out values should be mocked: methods that return something or have out parameters. This is the default behavior of the Pex Wizard.

Domain specific mocking

The method above is the boiler plate mock implementation for any method. In practice, you will probably want to simulate more accurately the behavior of the mocked class. Pex provides a couple of built-in implementations for domain specific methods:


See Also

PexChoose, Parameterized Mocks, Mocking Properties, Mocking Events, Mocking COM Interfaces

Mocking Properties


Properties have an expected behavior , which the mock property should try to follow:
  • properties do not throw,
  • the property setter stores the value, and the value should be returned by the property getter,
  • the property getter returns the same value in subsequent calls

To simplify this task, Pex provides two helper classes, PexOracleValue and PexOracleValueNotNull that works as a value holder that will lazily choose a value if queried.

Example

This example shows how to mock an interface IFoo which contains a readonly property Getter and a read-write property GetterSetter, which we assume is not null. 

// interface to be mocked
public interface IFoo {
    string Getter { get; }
    // assume is not null
    object GetterSetter { get; set; }    
}

the mock implementation:
public class MFoo : IFoo {
     private PexOracleValue<string> getter;
     private PexOracleValueNotNull<object> getterSetter;
 
     public MFoo() {
        this.setter = 
            new PexOracleValue<string>(this, "Getter");
        this.getterSetter = 
            new PexOracleValueNotNull<object>(this, "GetterSetter");
     }
 
     public string Getter {
          get { return this.getter.Value; }
     }
 
     public object GetterSetter {
          get { return this.getterSetter.Value; }
          get { this.getterSetter.Value = value; }
     }
}

See Also

Parameterized Mocks, Mocking Methods, Mocking Indexers, Mocking Events, Mock COM interfaces

Mocking Events


Pex does not make any special treatment for events currently.

Example 

interface IFoo {
   event EventHandler Boo;
}


class MFoo : IFoo {
   public event EventHandler Boo;
}

Mocking COM interfaces


Interfaces that back a COM interface (i.e. are marked with a ComImportAttribute) usually have methods that return HRESULT. The Wizard detects this patterns and adapts the mock body to generate a better behavior of the mock.

Example

Let's assume we have the following COM interface definition,

[ComImport]
interface IWorker
{
    // if returns S_OK, Foo is set    
    int GetValue(out Foo result);
}

This is a typical pattern for COM methods: if the method returns S_OK, the out parameter has been set with the result.

class MWorker : IWorker
{
    public int GetValue(out Foo result)
    {
        var call = PexChoose.FromCall(this);
        int hr = call.ChooseHResult();
        if (hr == PexChoose.HResults.S_OK)
            result = call.ChooseValueAtReturn<Foo>(1);
        else
            result = default(Foo);
        return hr;
    }
}

Structs


Pex reasoning about struct-values is similar to how it deals with objects.

Test Failures


When does a test case fail?

  1. If it does not terminate within the configured path bounds, it is considered as a failure, unless the TestExcludePathBoundsExceeded option is set.
  2. If the test throws a PexAssumeFailedException, it succeeds. (But it is usually filtered out, unless TestEmissionFilter is set to All.)
  3. If the test violates an assertion, e.g. by throwing an assertion violation exception of a unit testing framework, it fails.
  4. Otherwise, all registered IPexExceptionValidator are asked.
    • Every validator can decide to either let the test fail or pass.
    • One can use the common attributes which implement this the validator interface:
    • One can define it's own triage logic by definig a custom exception validator
If none of the above give a decision, a test succeeds if and only if it does not throw an exception. Assertion-violations are treated like exceptions.

Sometimes, when a test case fails, Pex can suggest a fix.

Diagnostic Messages


Allowing Exceptions


Pex provides numerous ways to help triaging exception into excepted exceptions and unexpected exceptions.

Expected exceptions generate negative test cases with the appropriate annotation (i.e. ExpectedException(typeof(xxx))), while unexpected exceptions generate failing unit test cases.

All validation attributes inherit from the PexAllowedExceptionAttributeBase and are used as regular exception decorators:

[PexMethod, PexAllowedException(typeof(ArgumentNullException))]
void SomeTest() {...}

Other validators are:

Common settings

  • AcceptExceptionSubtypes, determines whether subtypes of the allowed exception are valid,
  • AcceptInnerExceptions, determines whether the exception chain should be walked to find a valid instance,
  • Documented, determines whether the exception type should be documented in the xml documentation of the target site method,

Controlling the Test Output


When run inside of Visual Studio, Pex integrates the tests directly into the test project. When run using the command line, Pex drops the generated tests in the report folder.

Decision procedure

Pex uses the following informations to decide how and where to craft the generated tests: the test framework, the test language, the assembly root namespace , the output path and the test project.

Pex gets those values from different possible sources: an existing test project, the command line or the assembly settings. The most efficient way is specify the test project file. The following table describes which source can be used to provide pieces of information:

Name Default value Deduced from project Command Line Assembly setting
test framework test assembly references inspection no yes yes
test language C# yes no yes
assembly root namespace test assembly name yes no no
output path <report>\tests <test project path> no no

Generated files have the .g extension in the added to easily recognize them.

See Also

Providing The Test Project File

Settings Waterfall


Many aspects of Pex can be configured. Most settings are controlled by metadata in the form of custom attributes, and some options are available through the command line. Settings which control the exploration are set through the command line, while settings infrastructure information like path and file locations are set through the command line.

Metadata settings


PexSettingsAttributeBase is the base class for custom attributes that can be used to set settings in metadata.

Settings Waterfall


The concept of the settings waterfall means that the user can specify settings at the Assembly, Fixture and Exploration level. Settings specified at the assembly level, will impact all fixtures/exploration under that assembly, and so forth for fixtures. Child setting wins, i.e. If a setting is set at the Assembly and Fixture level, the fixture setting will win.


Note that some settings are specific to the Assembly level or Fixture level and some settings are also settable from the command line.

Example 


using Microsoft.Pex.Framework;
 
[assembly: PexAssemblySettings(MaxBranches = 1000)] // we override the default value of maxbranches
 
namespace MyTests
{
    [PexClass(MaxBranches = 500)] // we override the 1000 value and set maxbranches to 500 
    public partial class MyTests
    {
        [PexMethod(MaxBranches = 100)] // we override again, maxbranches = 100
        public void MyTest(...) { ... }
    }
}
 
// command line
pex.exe ... /maxbranches:50     // command line parameter overrides again, maxbramches = 50, final!

Testing Internal Types


Pex can 'test' internal types, providing that it can see them.
In order for Pex to see the types, add the following attribute to your product or test project:

[assembly: InternalsVisibleTo("Microsoft.Pex, PublicKey=76a274db078248c8")]

Visibility


.NET has a elaborate visibility model -- types, methods, fields, ... can be private, public, internal, etc.

When Pex generates tests, Pex will only attempt to perform actions (calling constructors, methods, setting fields,etc.) which are legal regarding .NET visibility rules from within the context of the generated tests. (Interestingly, this context depends on Pex' test output configuration.)

The rules are as follows:

  • Visibility of internal members: Pex assumes that the generated tests will have access to internal members that were visible to the enclosing PexClass; .NET has the InternalsVisibleToAttribute to extend the visibility of internal members to other assemblies.
  • Visibility of private and family (protected in C#) members of the PexClass:
    • Pex always places the generated tests either directly in the PexClass or into a subclass. Thus, Pex assumes that it may use all family visible members (protected in C#).
    • If the generated tests are placed directly into the PexClass (usually by using partial classes), Pex assumes that it may use all private members of the PexClass as well.
  • Visibility of public members: Of course, Pex assumes that it may use all exported members visible in the context of the PexClass.

PexPackages


Packages may customize the components that comprise Pex. A pex package may replace or configure any of the main Pex components.

See LogNewTestsAttribute in Samples.Pex for an example of pex package.


Attributes


Exploration Packages


Packages may customize the components that comprise Pex.

An exploration packages is only active during particular explorations. Packages are installed by special attributes that decorate test generators. They are designed to execute some code when Pex' exploration components are loaded, and before and after each test case Pex generates.

For example, such a package may check the resulting coverage.

By interacting with Pex' exception validator component, an exploration package may implement an effect similar to the ExpectedExceptionAttribute in other test frameworks.

Attributes



Examples


  • monitoring coverage,

// we'd like all explorations in the assembly to reach at least 70% coverage
[assembly: PexExpectedCoverage(70)]

  • monitoring test creation,

[PexClass]
[PexExpectedTests(NewCount = 0)] // notify my if any new test gets created
public class MyTest
{ ... }

  • Extensibility

You can implement your own exploration package by creating a custom attribute that inherits from PexExplorationPackageAttributeBase.

See Also

PexExpectedCoverageAttribute, PexExpectedTestsAttribute, PexClassAttribute, DySy

Path Packages


Packages may customize the components that comprise Pex.

A path package is only active during the execution and monitoring of a particular execution path. Packages are installed by special attributes that decorate test generators. They are designed to execute some code when Pex' path components are loaded, and before and after the execution path is execution.

See the DumpSolutionAttribute class in the Samples.Pex for an example of path package.

Attributes


Saving Current Behavior For Future Regression Testing


When a parameterized unit test returns a value, Pex explores the value public property graph and saves the current value as assertions in the generated test. When replaying the test, the assertion will ensure that the observable behavior has not changed.

[TestClass, PexClass]
public partial class CalendarTest {   
    [PexMethod]
    public string GetMonth(int i) {
        string month = Calendar.GetMonthName(i);
        // storing output, giving it a name
        return month;
    }
}

The resulting generated test call will contain code to ensure that the month names returned by GetMonthName do not change in the future.
Internally, Pex asserts that the value previously associated with the name "month" is equal to "January".

[TestMethod]
public void GetMonth01() {
    // invoke parameterized unit test, which associates names to computed values
    string result = GetMonth(1);
    // verifying that we received the expected named value
    // we expect "January", because that was the value Pex saw when generating this test
    Assert.AreEqual("January", result); 
}
...

TestCopyright


The TestCopyright setting from the PexAssemblySettingsAttribute can be used to specify a copyright header that will be insterted in every generated file.

  • in your PexAssemblyInfo.cs,
[assembly: PexAssemblySettings(TestCopyright = 
@" ----------------------
(c) Microsoft Corporation. All rights reserved.
 ------------------------")]

  • generated test,
// ----------------------
// (c) Microsoft Corporation. All rights reserved.
// ------------------------
...

Generated Unit Test Attributes


When Pex generates the unit tests, it also emits a number of attributes that give information about the test. These attributes can be used to build tools that will automatically apply transformation/maintainance to those tests.


Pex also emits other attributes that a test framework would expect:

Crafting Test Names


Naming unit tests is a controversial topic, where different trends fight each other over with convention is the best. With Pex it's even worse: Pex generates dozens of new unit tests and names them himself!

Crafting the meaningful generated unit test names is not an easy task, at least in an automated fashion. How can the machine translate a program trace to a higher level, consice, english correct, test name?

In Pex, we have default naming scheme that works in a simple fashion using timestamp. Because we understand that people will want to plug in their own logic, we've made sure that this mechanism is extensible.

Extensibility

Inherit from PexTestNamerAttributeBase attribute, and implement the IPexTestNamer interface.

See the Samples.Pex sample for an example of such extension.

Exception Injection


The goal of exception injection is to simulate error conditions that are otherwise hard to trigger. Examples include disk failures and network outages. Exception injection is sometimes also called fault injection.

Pex supports different kinds of systematic exception injection:

Debugging


Debugging with Pex can get a little tricky because Pex itself launches another process (where the profiler is attached).

Debugging from the command line


Pex provides command line arguments to break into the monitored process. Once the debug dialog shows up, simply click on Debug and attach it to your current Visual Studio instance.

The command line parameters are
  • /bos: breaks on start,
  • /boe: breaks on the first error
  • /boa: breaks on assert

Launching the monitored process through a debugger


Pex provides a command line argument to specify the driver of the monitored process, i.e. the application used to launch it. This is useful to launch the monitored process under windbg  for example:

    pex .... /driver=c:\debuggers\windbg.exe

Source Control Interaction


This section describes the different ways Pex can interact with a source control provider: Along the exploration, Pex might generate or modify existing files. Each new file should be added to the source control, while existing files should be checked out before modification.

There are basically 3 scenarios:

  • No source control available, Pex does not do any kind of special operations
  • Running inside of Visual Studio: if you are using the Visual Studio addin, we expect you to rely on the integrated source control.
  • Running from the command line: You need to register and select a source control provider.

Registering Source Control providers

  • use a built-in source control provider or an attribute from the Microsoft.Pex.Framework.SourceControl to define your own,
public sealed class SvnSourceControlAttribute :
    PexProcessSourceControlAttributeBase {
    public SvnControlAttribute (string toolPath)
        : base("svn", "svn.exe")
    { }
 
    protected override string GetAddArguments(string fileName) {
        return SafeString.Format("add \"{0}\"", fileName);
    }
 
    protected override string GetCheckOutArguments(string fileName) {
        return SafeString.Format("edit \"{0}\"", fileName);
    }
}
// assemblyinfo.cs
[assembly: SvnSourceControl]
  • specify the source control name in the command line
pex ... /sc:svn

Symbols And Sources


Pex uses symbols and sources in various situations so it is important to set up correctly the symbol path and sources through the command line. In Visual Studio, Pex picks up the symbol information from the Visual Studio symbol options.

Prequisites


symsrv.dll in the path (install debuggers from http://www.microsoft.com/whdc/devtools/debugging/debugstart.mspx  )

Symbol Server


Pex uses the Mdbg  SymbolStore, which itself calls symsrv.dll. This means that the usual syntax to set up symbol servers can be used in the Pex command line:

pex /sympath:srv*c:\symbols*http://msdl.microsoft.com/download/symbols

Tips


  • Pex understands _NT_SOURCE_PATH and _NT_SYMBOL_PATH.

Unit Test Frameworks Integration


Pex was designed to integrate seamlessly into test frameworks based on Custom Attribute, such as MSTest, NUnit, MbUnit, ....
This means that Pex generates test cases that are annotated with the specific attributes of any of those test frameworks.

  • Test classes and Pex classes can be identical. The Parameterized Unit Tests can live side-by-side with other unit tests inside the test fixture:
[TestClass] // this class contains unit tests
public partial class MyTestFixture {
    // this is a unit test
    [TestMethod]  
    public void UnitTest() {...} 
 
    // this is a parameterized unit test
    [PexMethod]  
    public void ParameterizedTest(int i) {...} 
 
    // this is a generated unit test
    // from ParameterizedTest
    [TestMethod, ...]
    public void ParameterizedTest_1() { 
        this.ParameterizedTest(0); 
    }
}


See Also

TestClassAttribute, PexClassAttribute

SetUp And TearDown (Exploration Life Cycle)


As part of the integration with test frameworks, Pex support running setup and teardown methods. Setup and teardown methods are used to refactor common code outside of the test/fixture (this is a feature supported by most unit test frameworks).

[TestClass]
public class MyFixture
{
    [TestInitialize] public void SetupStuffForMyTests() {...}
    [TestCleanup] public void SetupStuffForMyTests() {...}
}

The availability of setup and teardown methods depends on your test framework

Life Cycle

The following table gives the guaranteed execution sequence that Pex will apply. A couple things are worth precising:

  • assembly, fixture and test level setup and teardown methods are always optional.
  • assembly and fixture level setup and teardown methods will run unmonitored. This means that no constraints will be gathered when they are running.

  • assembly setup (optional - unmonitored)
    • if failed, the rest of the execution is skipped
    • fixture setup (optional - unmonitored)
      • if failed, fixture execution is skipped
      • for each exploration,
        • default constructor (always - monitored)
        • Setup (optional - monitored)
          • if failed, exploration execution is skipped
        • exploration (monitored)
        • TearDown (optional - unmonitored)
          • if failed, exploration is marked as failed
        • Dispose (optional - unmonitored)
    • fixture teardown (optional - unmonitored)
  • assembly teardown (optional - unmonitored)

Guarantees


Unless the process crashes catastrophically,

  • assembly teardown is always executed,
  • fixture teardown is always executed,
  • teardown and/or dispose is always executed if the fixture instance constructor returned successfully
  • the same fixture instance will be used for the setup and teardown of explorations
  • there is no guarantee that the same fixture instance will be used for the fixture setup/teardown. In fact, Pex will create a new instance on each test.

Example 


namespace MyTests
{
    using Microsoft.Pex.Framework;
    using MbUnit.Framework;
 
    [assembly: AssemblyCleanup(typeof(MyAssemblySetup))]
 
    public static class MyAssemblySetup {
         [SetUp]
         public static void SetUp() {
             Console.WriteLine("assembly setup");
         }   
    }
 
    [TestFixture]
    public partial class MyTests {
        [TestFixtureSetUp]
        public void FixtureSetUp() {
             Console.WriteLine("some fixture wide setup here");
        }
 
        [TestFixtureTearDown]
        public void FixtureTearDown() {
             Console.WriteLine("some fixture wide teardown here");
        }
 
        [SetUp]
        public void SetUp() {
             Console.WriteLine("monitored setup");
        }
      
        [PexMethod]
        public void MyTest(int i ) {...}
 
        [TearDown]
        public void TearDown() {
             Console.WriteLine("Clean up");
        }
    }
}

The above example will result in the following execution trace:
MyAssemblySetup.SetUp
MyTests.FixtureSetUp
MyTests.SetUp
MyTests.MyTest
MyTests.TearDown
...
MyTests.SetUp
MyTests.MyTest
MyTests.TearDown
MyTests.FixtureTearDown

See Also

PexClassAttribute, PexMethodAttribute

Ignoring Explorations


When you need to disable an exploration or a fixture (temporarily), you can use your unit test framework 'ignore' attribute. You can also the PexIgnore attribute to mark the method or type:

[PexMethod]
[PexIgnore("ignore reason")]
public void MyTest(int i) {...}

If the exploration is ignored because of a workitem, one can also specify the workitem id in the PexIgnore attribute constructor:

[PexMethod]
[PexIgnore("ignore reason", WorkItemId = 12345)]
public void MyTest(int i) {...}

See Also

PexIgnoreAttribute, PexClassAttribute, PexMethodAttribute

Generated Tests


On successful path exploration, Pex will generate the source code of a new test case. The test case will automatically be tagged with the custom attribute that your test framework supports.

Selecting the Test Framework


Similarly to the output language, the test framework is specified in the constructor PexAssemblySettings attribute. If your project already references the test framework main assembly, Pex will automatically resolve the framework from that assembly.

Where do the tests get generated?


By default, tests get generated in the report folder under tests. A much more appealing feature is to provide the test project, Pex can then place the generated files at the 'right' place and update the project file. See Providing The Test Project File.

generatedtests.png

File extension


The file containing the generated tests have a .g before the language extension:
    test123.g.cs

See Supported Test Frameworks.

See Also

PexAssemblySettingsAttribute, PexClassAttribute, PexMethodAttribute

Test Bookkeeping


Pex emits traditional unit tests. Pex manages the set of generated tests in order to only keep relevant tests around.

This management involves two aspects:
  • Preventing duplicate tests. Currently, when you run Pex, it always explores a program from scratch. Therefore, it might (re-)generate tests it had already generated before. Such tests should not be emitted again.
  • Removing tests which have become irrelevant. When the code of program under test changes, the relevant corner cases might change as well. Therefore, previously relevant tests might become irrelevant, and are replaced by new test cases.

Requirements


Pex' test bookkeeping only works if
  • the generated tests are placed in the Pex test assembly (i.e. the assembly which contains the generating PexClass),
  • Pex has access to the symbols (.pdb files) and sources for the generated tests, and
  • you do not manually edit the generated tests.

How it works


At first, Pex preprocesses existing tests: Pex starts by scanning the assembly containing the pex fixtures (see PexClassAttribute) for generated tests (it assumes that they are in the same assembly). Generated tests are recognizable from the Test attribute and PexGeneratedBy attribute.

For each test method, it fetches the source code from the symbols/sources. White spaces are trimmed from the source, and the resulting string is the 'hash' key of the generated test. Pex also uses the expected or unexpected exception information.

Once this is done, Pex has a dictionary of test 'hashes' that it can use to determine whether a newly generated test already exists. Duplicated tests are reported but not emitted since they are already present.

If a previously existing test case is not regenerated, it is deleted, unless you remove the PexGeneratedByAttribute attribute.

See Also

TestAttribute, PexRaisedExceptionAttribute, PexGeneratedByAttribute
Pex copies any unknown attribute that is marking the parameterized test to the generated test. Therefore, issue/project tracking attributes are automatically propagated to the generated unit test.

Example 


// fixture type
[TestClass, PexClass]
public partial class MyTest {
    [PexMethod]
    [CssProjectStructure("xxx"), CssIteration("yyy")]
    [WorkItem(1), WorkItem(2)]
    public void Foo(int i) {...}
}


// generated tests
public partial class MyTest {
    [TestMethod]
    [CssProjectStructure("xxx")]
    [CssIteration("yyy")]
    [WorkItem(1)]
    [WorkItem(2)]
    public void Foo_1234() { ... }
}

See Also

PexMethodAttribute, PexClassAttribute, TestClassAttribute, PexIgnoreAttribute

Propagation of Satellite Attributes


Test framework may have additional attribute used to annotate tests with domain specific data: bug ids, description, categories, suites, etc...

Each test framework knows about those 'satellite' attributes and propagates (i.e. copy) them to the generated test.

Example

The following example shows how the NUnit's CategoryAttribute can be applied to a parameterized test, and have Pex automatically propagate it to the generated tests:

[PexMethod, Category("very important")]
public void Important(int i) {...}

Then the generated test also have the CategoryAttribute:

[Test, ...]
[Category("very important")]
public void Important_1234_213_1() {...}

Supported Test Languages


Pex can analyze any MSIL code (that includes dynamic code as well).

Pex test emission only works for C#.

See Also

PexAssemblySettingsAttribute, TestLanguage
Pex' reports can be analyzed in order to tune Pex' settings, to determine the necessary scope code instrumentation, and to determine the quality of the implementation-under-test.
The Pex reports will display a variatey of logging events. These events have a level, a category and optinonaly a wiki page link.

Logging events are ranged from the following:

  • critical, an unexpected error occured in the Pex tool itself. This is most likely a problem in the tool itself and should be reported.

  • error, a expected event that denotes usually denotes an issue in the setup of Pex tests.

  • warning - you should probably look at it, an event that denotes an issue that would be worth taking a look at, e.g. uninstrumented calls, missing symbols.

  • message, a verbose message providing interresting information on the progress of the execution.

  • noisy, a very verbose message mostly used for diagnostics.
Pex generates a new report folder on each exection. This means that after some time, a lot of those (big) folder start to pile up. To tackle this problem, the pex command line comes with an auto-cleaning options.

When turned on, the auto-cleaning will keep the 25 latest report and trash the older ones.
  • turning on auto-cleaning
pex.exe /rc

  • keeping 10 reports only
pex.exe /rc /rmc 10
When Pex does not achieve high code coverage, it might be that the instrumentation is not set up correctly and a lot of methods do not get instrumented. As a result, Pex does not 'know about' the things that occur in those method and cannot generate relevant inputs.

The reports provide detailed information about executed methods that were not instrumented by Pex. The user should use the reports to troubleshoot instrumentation problems.

Uninstrumented Call Menu


The uninstrumented call menu will be displayed if uninstrumented calls occur, at the assembly, fixture and exploration level in the reports. Click to open/close the table.

uninstrumentedmenu.Png

Uninstrumented Call Table


The uninstrumented table displays the full list of uninstrumented managed methods.
uninstrumentedexpanded.Png
Pex may generate many tests which cause exceptions. The reports provide specialized visualization to explore where and which exceptions were thrown.
  • the frame tree provides a consolidated tree of stackframe, grouped by exception types.
  • the exception table provides a table of thrown exceptions and sources.

The exception frame tree groups the exceptions by type, and consolidates them in a stack frame tree. This view is very handy to quickly drill through the different exceptions and jump directly to the interesting tests.

Frame Tree Menu


The exception frame tree appears at the assembly level. Click on the menu item on open/close the table.

frametreemenu.Png

Frame Tree


The way to use the table below is to look for unexpected exceptions, such as NullReferenceException or InvalidCastException. Then look at the call stack that generated that failure. If one of the call stack look suspicious, click on the [] to expand the list of tests that triggered that exception.

frametreeexpanded.Png

Once expanded, the test list provides links to the fixtures and tests:

frametreeexpandedtests.Png
The exception table provides a compact view of which and where (assembly) exceptions were thrown. It is a handy view to detect unexpected exceptions, as Pex may trigger a lot of them.

Exception Table Menu


The exception menu will appear at the assembly, fixture or exploratin level if any occured. Click to open/close the table.

exceptionmenu.Png

Exception Table


The exception table gives the list of exception type that were raised. For each type, it provides the list of assembly in which they were thrown.

exceptionexpanded.Png

Click on the 'tests' link to display the list of tests that triggered that exception.

exceptionexpandedtests.Png

Coverage Filtering


When you want to analyze relative code coverage, it is important that you define the types and assemblies that should be considered in the analysis.

Pex provides a set of attributes to specify if methods of a type should be ignored, excluded or included. These settings can be set at different levels (see Settings Waterfall).

Attributes



Ignored By Default


  • Microsoft.Pex.Framework
  • the main assembly of the current TestFramework, to avoid having the coverage of the assertion/assumption classes

Extensibility


If you are not happy with the attributes that come with Pex, you can write your own by extending the PexCoverageFilterAttributeBase.
You can use PexObserve to log events and values computed during the test execution. The values are diplayed in Visual Studio and in the html reports.
parametervalues.png
parametervalues2.png


The exploration process in Pex is bounded by many gates. Depending on the type of application that Pex explores, different boundaries might be triggered. To increase the efficiency of Pex, the user might have to modify the default values of those boundaries.

The reports provide a table indicating which boundary was reached and how often. It can be used to efficiently tune the values.

Boundary Menu


The menu will display at the assembly, fixture or exploration level if any boundary was reached. Click to open/close the table.
boundarymenu.png

Boundary Table


The boundary table provides the kind of boundary and number of occurences. The boundary value can be updated through the settings attributes.
boundaryexpanded.png

Visual Studio Integration


Pex provides Visual Studio tools to help improve parameterized unit testing development.

Snippets


Pex installs the following expansion snippets:

C#, VisualBasic.NET



Command Line


Parameterized unit tests can be run using the pex.exe executable:

pex.exe mypexassembly.dll

The tool will discover all the pex classes and execute them. At the end, a report is generated. The command line supports a number of flags for filtering fixture or explorations, controlling the test generation or reports. The filters use a simple syntax.

Selecting What to Run


The command line supports wildcard filter to select tests by namespace, type or methods.
  • /nf: namespace filter
pex.exe ... /nf:MyTests.Current

  • /tf: type name filter
pex.exe ... /tf:MyTests

  • /mf: method name filter
pex.exe ... /mf:SquareTest

  • /cf: category filter
pex.exe ... /cf:data;web

  • /sf: suite filter
pex.exe ... /sf:checkin

  • /if ignore the 'ignore test' annotations,
pex.exe ... /if

Examples


  • selecting a particular test,
pex.exe ... /nf:<namespace> /tf:<type name> /mf:<method name>

See Also
Parameterized Unit Testing, PexMethodAttribute, PexClassAttribute

Command Line Filters Syntax


The Pex Command Line provides a range of filter that can be used to select explorations to run in various ways. All filters use the following syntax:

Syntax

All the filters use a simple grammar:

  • filters are case insensitive,
  • by default, filters perform a substring matching,
    • el matches hello,
  • adding ! to the end of the filter will make it a precise match,
    • el! does not match hello,
    • hello! matches hello,
  • adding * to the end of the filter will make it match the prefix of the string,
    • el* does not match hello,
    • he* matches hello,
  • multiple filters can be combined in a semi-column separated list,
    • el;wo matches hello and world

Pex Wizard


  • If you did not download Pex yet, Download Pex  to get the Pex Wizard.
  • The Pex Wizard is your "one-push button" solution to get started with Pex:

    pexwizard.exe <your assembly name>

The wizard does the following steps:

  • it generates Parameterized Test Stubs for all methods of the visible API,
  • compiles the generated project (containing parameterized tests), and
  • tells you how to launch Pex on the compiled assembly.

After the Wizard is done, you can launch Pex with a command-line similar to the following:
    pex.exe <generated parameterized test stubs.dll> [more options]
Pex will generate parameterless test cases from the parameterized test stubs.

At that point, Pex will generate inputs that may find violations of assertions in the code-under-test, or issues like a NullReferenceException.
We strongly recommend that you start to tweak the Parameterized Test Stubs which the Wizard generated, calling more functions, and adding test assertions.

See Also


Wizard Extensions


Extensibility


Pex and Extended Reflection provide many extensibility points to build new dynamic analysis tools or simply add some missing feature in Pex. The extensibility is generally done through custom attributes:

  • the extension developer implements an abstract base attribute,
  • the extension consumer references the new attribute to use it's functionalities

Disclaimer


Although we will try to avoid breaking changes in Pex internal APIs, we might (and will) change or remove parts of Pex internal API from version to version. This might occur without notice but we will try to give a heads up to the extension writer on important changes (through the extension project).

Wizard Extensions


under construction

The user can provider custom test framework or test generation templates by specifying additional assemblies in the command line. The types will be loaded through Reflection:

// MyCustomTestFramework.dll contains a custom test framework
pexwizard.exe ... /sa:MyCustomTestFramework.dll

Research Problems


A collection of open questions related dynamic code analysis. Using Pex component architecture, you can provide your own 'solution' to each of those problems.

Questions



Problems


Coding Guidelines For Extensions


This page contains guidelines for Pex extension writers.

Be aware of instrumentation
An important fact needs to stay in the mind of the implementor when doing so:
  • any BCL class used in the extension might be instrumented, which deteriorates it's performance.

To counter this effect, different solutions are possible:
  • Do not use that particular API.
  • Use the 'SafeXXX' counterpart of 'XXX' that ships with Extended Reflection.
    • (The name prefix 'Safe' has a historical reason: in the beginning, Extended Reflection had no mechanism to deal with re-entrance problems, and using any instrumented class by the monitoring code was fatal. This is no longer the case, but using any method that has been instrumented comes with a big performance penalty.)
    • When using a debug build of Extended Reflection, you can generate a log file and inspect the listings of calls to instrumented methods.
    • use the safe collections, e.g. SafeDictionary<,> instead of Dictionary<,>.
    • use the safe debug assertions and assumptions (pre-conditions), e.g. SafeDebug.AssumeNotNull(foo);
    • use SafeDebugger.Break() to break
    • use SafeString instead of String,
    • use SafeStringBuilder instead of StringBuilder
    • use SafeStringWriter instead of StringWriter; however, consider using StringBuilder instead since it is more lightweight
  • When your code might be called from instrumented code, and you don't want that your code is monitored, wrap it into a disposable _ProtectingThreadContext. This disables monitoring callbacks.
using (_ProtectingThreadContext.Acquire())
{
    // your code
}

More guidelines

  • test your extension using a debug build of Pex; it contains assertions that indicate early if you misused an API
  • prefer IIndexable<T>, ICountable<T> or ICopyable<T> to IEnumerable<T>
  • consider using IFiniteSet<T>, or IFiniteMap<T> to represent immutable data sets and maps
  • do not (implicitly) cast an array to IEnumerable<T> (or IList<T>, ICollection<T>), since enumerating over the array involving a helper class that gets instrumented!
  • use Indexable, Set, Map, Enumerable to create collections
  • use lazy allocations
  • use Extended Reflection metadata instead of System.Reflection, for example TypeEx t = Metadata<Foo>.Type;


Packaging Extensions


Extensions can be packaged in assemblies. Extension assemblies are loaded using a derived attribute of PexPackageAssemblyAttribute.

  • Create a custom attribute in the extension project that derives from PexPackageAssemblyAttribute,
// extension project
public sealed class MyExtensionsPackageAttribute 
  : PexPackageAssemblyAttribute
{}
  • If the extension contains services that should be loaded by default, add them as assembly level attribute,
[assembly: PexInstrumentAssembly("Foo")]
[assembly: PexFocusOnAssembly("Foo")]
...
  • In order to improve Pex startup time, most services can also be declared on a supporting type (instead of the assembly level) using the PexPackageTypeAttribute attribute:
[assembly: PexPackageType(typeof(MyLibrary))]
...
[PexFocusOnAssembly("Foo")]
static class MyLibrary {
}
  • Reference the extension package attribute in the target project,
// test project
[assembly: MyExtensionsPackage]

Graph Package


This package provides various visualization of the internal structures of Pex using Msagl .

Getting started

  • Add a reference to Microsoft.Pex.Graphs.dll
  • Add the PexGraphPackage attribute to the test project,
[assembly: PexGraphPackage]

Graphs

  • SearchGraph, renders the execution tree node,
  • TermGraph, renders term trees,

All Settings

Warnings And Errors



Other diagnostic messages



(For all other warnings and errors: Missing Wiki Topic)

Exit Codes


The following table gives a brief description of the different exit code that the pex console application could return.

  • General exit codes,
Exit Code Value Name
0 success
0xC000013A Control C
0x80131506 fatal execution engine error 1
0x800703E9 fatal execution engine error 2
0xE0434F4D CLR error


Exit Code Value Name
-666 assertion or assumption
-667 CLR Monitor failure

  • Pex exit codes,
Exit Code Value Name
-1 unknown
-999 user aborted
-1000 default failure
-1001 unknown pointer size
-1003 options parsing error
-1004 error in sandbox
-1005 no channel set
-1006 assembly load error
-1007 platform mistmatch
-1008 unexpected tool error
-1009 unexpected launch error
-1010 reflection error
-1011 unrecoverable error while reflecting tests
-1012 could not find the test assembly
-1013 could not find any test to run
-1014 instrumention driver configuration error
-1015 external profiler registered
-1016 monitoring of X86 code not enabled
-1017 monitoring of X64 code not not enabled
-1018 remoting connection could not be established
-2000 Visual Studio Build failed

Static Helper Classes


Pex provides a set of static helper class that can be used when authoring parameterized unit tests:
  • PexAssume, facilities to state assumptions on inputs, useful to filter out undesirable inputs,
  • PexAssert, simple assertion class in case your test framework does not provide one,
  • PexChoose, a stream of additional test inputs that Pex manages,
  • PexObserve, logs concrete values and optionaly validates them in the generated code,

More researchy,

Detecting Pex Installation With Wix

The following Wix fragment defines properties that can be used to detect which features of Pex are installed.

<?xml version="1.0" encoding="utf-8"?>
<Wix xmlns="http://schemas.microsoft.com/wix/2006/wi">
  <!-- indicates if Pex was installed -->
  <Fragment>
    <Property Id="PEX" Secure="yes">
      <RegistrySearch 
        Id="PexConsoleSearch" 
        Root="HKLM" 
        Key="Software\Microsoft\Pex\CurrentVersion"
        Name="InstallPath" 
        Type="raw" 
        Win64="no" />
    </Property>
  </Fragment>
</Wix>

Samples.Pex


A project that is part of the Pex distribution.

This project contains samples showing how to write parameterized unit tests with Pex. It also contains examples from the Tutorial.

Samples.Tracing


A project that is part of the Pex distribution.
This project contains a sample showing how to monitor the execution of .Net applications.

Instructions


Build the project

Use Sample.Tracer.EXE to launch your application

Run Sample.Tracer.EXE with your own application EXE as the command-line exe.
The sample will take care of setting up code instrumentation.

For example, if you run a program whose Main method only calls another method called Foo, the output of the sample monitoring might look as follows:

... tracer loaded
[1] <enter> ConsoleApplication.Program.Main
 [1] <enter>  ConsoleApplication.Program.Foo
 [1] <leave>
[1] <leave>

Background: What happens under the hood.

Execute the following steps in an elevated command prompt window.

Install Microsoft.ExtendedReflection

If you didn't install Pex with the regular installer, you have to install the Microsoft.ExtendedReflection assembly in the GAC, and register the unmanaged profiler COM component:

gacutil /i (proper directory)\Microsoft.ExtendedReflection.dll
regsvr32 /i (proper directory)\Microsoft.ExtendedReflection.ClrMonitor.X86.dll
(Make sure that gacutil.exe and regsvr32 are in your path.)

Set up environment

Then, before you run the .Net application you want to monitor, you have to set some environment variables. Call

RegisterTracer.cmd

Run your application

Now all applications .NET that you run in that command prompt window will be monitored.

Caveats under X64

If you use a 64-bit operating system, you need to install the dedicated 64-bit version of Pex.
The X86 version will not work seamlessly for application monitoring on 64-bit operating systems.

Samples.Reflection


A sample that shows how to use Extended Reflection metadata model.

The sample is a command line application that takes an assembly name, walks through the metadata of the assembly and emits C# code from it.

Samples.VisualStudio.Fixes


This sample describes how to create a tool that injects 'fixes' in to the Pex suggestion view.

DySy


DySy is a dynamic symbolic assertion inference tool as in the following technical report:


DySy source code is available in the Pex Extensions Project.

Chunker Screencast


chunkersnapshot.png Watch it! 

The screencast demonstrates how Pex can be used to design, implement and test a string chunker.

Before looking at the screencast,

As mentionned above, the chunker takes a string and cuts it into pieces:


Definition: A chunker cuts a string into pieces of a particular length (chunks) and returns them to the user.

One thing that the Chunker should verify is that the concatenation of the chunks should be equal to the original string:


Test: for any string value and for any chunk length, the concatenation of the chunks should be equal to value.

Storyboard

  • One starts by writing a parameterized unit test that translates Test in C#. Notice that, each time for any is used in the test description a parameter is added to the test method: 
[TestClass, PexClass]
public partial class ChunkerTest {
    [PexMethod]
    public void Chunk(string value, int length) {
        Chunker chunker = new Chunker(value, length);
        string result = null;
        for (string chunk = chunker.Next();
            chunk != null;
            chunk = chunker.Next())
            result += chunk;
        Assert.AreEqual(value, result);
    }
}
  • A minimal implementation of Chunker is written to have the code compile. 
public class Chunker {
    public Chunker(string value, int length) { }
    public string Next() {
        return null;
    }
}
  • Using the Visual Studio integration, Pex is invoked and starts exploring the test. Pex generates 2 unit test cases, one that passes null and succeeds, one that passes the empty string and fails. This was found by a systematic exploration of the program behavior, not by chance or randomness; when running Assert.AreEqual, Pex detected a branch on the string equality that guarded the assertion failure. Pex then computed the input parameters to explore the other branch... and fail the assertion. 
[TestMethod(), ...]
public void ChunkStringInt32_70312_151917_0_01() {
    this.Chunk(((string)(null)), -1);
}
[TestMethod(), ...]
[PexUnexpectedException(typeof(AssertFailedException))]
public void ChunkStringInt32_70312_151917_0_02() {
   string s0 = "";
   this.Chunk(((string)(s0)), -1);
}
Both tests get added automatically in the project.
  • A naive implementation of the chunker is written that would potentially fix the issue found. 
public class Chunker {
    string value;
    int length, index;
    public Chunker(string value, int length) {
        this.value = value;
        this.length = length;
    }
    public string Next() {
        string chunk = this.value.Substring(this.index, this.length);
        this.index += this.length;
        return chunk;
    }
}
  • Pex is run again. Pex finds the null reference issue because value is not validated and the ArgumentOutOfRangeException because index increases without bounds. More failures could have been found but Pex was configured to stop after 2 failures. In these particular cases where the input to a method breaks it's contract (triggers argument validation), Pex uses a precise data-flow analysis to deduce how and where an argument validation (i.e. pre-condition) should be added. In the screencast, although the error occurs in Next, the public constructor is the location where the argument should have been validated. 
public Chunker(string value, int length) {
    // <pex>
    if (value == null)
        throw new ArgumentNullException("value");
    if (length < 0 | value.Length < length)
        throw new ArgumentException("length < 0 | value.Length < length");
    // </pex>
    this.value = value;
    this.length = length;
}
  • Pex is run again and now reports the argument validation exceptions as failure. This occurs because Pex does not have any idea on how the user wants to triage the exceptions (expected or not?). The user can use a set of custom attributes to do this. In the screencast, the PexAllowedExceptionFromAssembly attribute is used to state that

exceptions that inherit from ArgumentException are expected.

  • Pex is run again and silently emits tests with the ExpectedException attribute for the argument validation cases. This iteration continues a couple more times...
    • Fix the zero length problem (<= instead of <) 
if (length <= 0 | value.Length > length)
    throw new ArgumentOutOfRangeException();
    • Fix the index out of range in Next()
string chunk;
if (this.index > this.value.Length)
    chunk = null;
else
    chunk = this.value.Substring(this.index, this.length);
    • Fix another index out of range in Next() 
string chunk;
if (this.index > this.value.Length)
    chunk = null;
else if (this.index + this.length > this.value.Length)
    chunk = this.value.Substring(this.index);
else
    chunk = this.value.Substring(this.index, this.length);
  • The last part of the screencast shows how generated tests integrate nicely into a existing unit test framework, in this case VSTS. Pex can also be used with NUnit or MbUnit.
See ICorProfilerCallback2  Interface.
The following samples come with Pex.

The following samples come with Pex.

The following samples come with Pex.

  • TinyLanguage
  • (TODO: bigger language)
  • (TODO: byte code verification)
The following samples come with Pex.

The following samples come with Pex.

  • Hashtable
The following samples come with Pex.

The following samples come with Pex.

  • (TODO: Queue)

Testing Web Services


This page describes how Pex can help the developer functionaly test web services, both from a server and client point of view. These pages are mostly targetted for classic web services.

Client Side

When one uses an external web services, that are not guarantees on the result besides the type safety provided by the SOAP specification. Therefore, since all input is evil, an application consuming web services should thorously check the results returned by those services.

Since Web Services are defined as .net classes, one can use Pex 'as usual' to get functional testing over those classes.

Tip: The project type "Web Application" which simplifies testing such web services.

PexAssumeNotNullAttribute


This attribute expresses that the governed value cannot be 'null'. It can be attached on 
// assume foo is not null
[PexMethod]
public void SomeTest([PexAssumeNotNull]IFoo foo, ...) {}
  • a field, 
public class Foo {
   // this field should not be null
   [PexAssumeNotNull]
   public object Bar;
}
  • or a type.
// never consider null for Foo types
[PexAssumeNotNull]
public class Foo {}

It can also be attached to a test assembly, test fixture or test method; in this case the first arguments must indicate to which field or type the assumptions apply. When the attribute applies to a type, then it applies to all fields with this formal type.

PexAssert


Static class to express assertions, i.e. a postcondition, in parameterized unit tests.

If the asserted condition does not hold for some test input, a PexAssertFailedException is thrown, which will cause the test to fail.

Example


Asserts that the absolute value of an integer is positive:

public void Test(int i) {
     int j = Math.Abs(i);
     PexAssert.IsTrue(j >= 0);
}

See Also


PexAssume, PexObserve, PexChoose

PexObserve


Static class to log named values. When Pex explores the code, PexObserve allows to record computed values using their formatted string representations. The values are associated to unique names. 

PexObserve.Value<string>("result", result);

Example 


// product code
public static class MathEx {
     public static int Square(int value) { return value * value; }
}


// fixture
[TestClass]
public partial class MathExTests {
     [PexMethod]
     public int SquareTest(int a) {
        int result = MathEx.Square(a); 
        // storing result
        return result;
     }
}

See Also

PexClassAttribute, PexMethodAttribute

PexAssemblyUnderTestAttribute


Attribute used to specify an assembly that is being tested by the current test project. 

[assembly: PexAssemblyUnderTest("MyAssembly")]

See Also

Test To Code Binding

PexInstrumentAssemblyAttribute


Attribute used to specify an assembly to be instrumented. This attribute implements PexInstrumentAssemblyAttributeBase.

Example 

using Microsoft.Pex.Framework;
 
// the assembly containing ATypeFromTheAssemblyToInstrument should be instrumented
[assembly: PexInstrumentAssembly(typeof(ATypeFromTheAssemblyToInstrument))]
 
// the assembly name can be used as well
[assembly: PexInstrumentAssembly("MyAssemblyName")]

See Also

Instrumented Assemblies and Types
Custom Attribute used to mark a class containing unit tests in MSTest.

[TestClass]
publi class FooTest
{
    [TestMethod]
    public void SomeTestOnFoo() {...}
}

See Also

TestMethodAttribute
Custom Attribute used to mark a clas containing unit tests in NUnit.
See Partial Class Definitions (C# Programming Guide) .

PexSettingsAttributeBase


This is the abstract base class for settings attributes. See Settings Waterfall for an overview of settings in Pex.

You can modify the following settings using named properties of this and its derived attributes:

[PexClass(MaxRuns = 10)]
public partial class FooTest {...}

Constraint solving bounds


Exploration Path Bounds

  • MaxBranches - Maximum number of branches that may be taken along a single execution path
  • MaxCalls - Maximum number of calls that may be taken during a single execution path
  • MaxStack - Maximum size of the stack at any time during a single execution path, measured in number of active call frames
  • MaxConditions - Maximum number of conditions over the inputs that may be checked during a single execution path

Exploration Bounds

  • MaxRuns - Maximum number of runs that will be tried during an exploration
  • MaxRunsWithoutNewTests - Maximum number of consecutive runs without a new test being emitted
  • MaxRunsWithUniquePaths - Maximum number of runs with unique execution paths that will be tried during an exploration
  • MaxExceptions - Maximum number of exceptions that may be found over all discovered execution paths combined
  • MaxExecutionTreeNodes - Maximum number of conditions over the inputs that may be checked during all discovered execution paths combined
  • MaxWorkingSet - Maximum size of working set in megabytes
  • TimeOut - Seconds after which exploration stops

Test Suite Code Generation Settings

cases which are marked as disabled

The following attributes derive from PexSettingsAttribute:
As part of the integration with test frameworks, Pex support detecting and running setup and teardown methods.

Life Cycle


  • assembly setup (optional - unmonitored)
    • if failed, the rest of the execution is skipped
    • fixture setup (optional - unmonitored)
      • if failed, fixture execution is skipped
      • for each exploration,
        • default constructor (always - monitored)
        • Setup (optional - monitored)
          • if failed, exploration exection is skipped
        • exploration (monitored)
        • TearDown (optional - unmonitored)
          • if failed, exploration is marked as failed
      • Dispose (optional - unmonitored)
    • fixture teardown (optional - unmonitored)
  • assembly teardown (optional - unmonitored)

Guarantees


  • assembly teardown is always executed,
  • fixture teardown is always executed if setup or exploration was attempted,
  • fixture teardown and/or dispose is always executed if the fixture instance constructor returned successfully
  • the same fixture instance will be used for the setup and teardown of explorations
  • there is no guarantee that the same fixture instance will be used for the fixture setup/teardown.

Example 


namespace MyTests
{
    using Microsoft.Pex.Framework;
    using MbUnit.Framework;
 
    [assembly: AssemblyCleanup(typeof(MyAssemblySetup))]
 
    public static class MyAssemblySetup
    {
         [SetUp]
         public static void SetUp()
         {
             Console.WriteLine("assembly setup");
         }   
    }
 
    [TestFixture, PexClass]
    public partial class MyTests
    {
        [TestFixtureSetUp]
        public void FixtureSetUp()
        {
             Console.WriteLine("some fixture wide setup here");
        }
 
        [SetUp]
        public void SetUp()
        {
             Console.WriteLine("monitored setup");
        }
      
        [PexMethod]
        public void MyTest(int i ) {...}
    }
}

See Also

PexClassAttribute, PexMethodAttribute

PexCoverageFilterAttributeBase


Abstract base attribute used to provide coverage filters. Such filters are used to ignore, include or exclude covered code from the coverage reports. This is useful when one wants to exclude the coverage of the tests.

Implementations

PexCoverageExcludeTypeAttribute


Attribute that specifies a type to be ignored, excluded or included from the coverage reports.

This attribute is a decoration attribute, i.e. it can be set at the Assembly, Class or Test level.

Example


The example below shows how to exclude the type MyTest:

// exclude MyTest type
[assembly: PexCoverageFilterType(PexCoverageDomain.Excluded, typeof(MyTest))]

Extensibility


This attribute inherits from the PexCoverageTypeAttributeBase attribute. User can inherit from that attribute to write custom coverage exclusion logic.

Precondition


A precondition of a method expresses the conditions under which the method will succeed.

Usually, the precondition is enforced by checking the parameters and the object state, and throwing a ArgumentException or InvalidOperationException if it is violated.

With Pex, a precondition of a parameterized unit test is expressed with PexAssume.

Postcondition


A postcondition of a method expresses conditions which should hold during and after the execution of the method, assuming that its preconditions held initially.

Usually, postcondition are enforced by calls to 'Assert' methods.

With Pex, a postcondition of a parameterized unit test is expressed with PexAssert.

PexGenericArgumentsAttribute


Attribute used to provide a type tuple for instantiating a generic parameterized unit test.

See Also

PexGenericTest, PexGenericArgumentsProviderAttributeBase

PexAssumeUnderTestAttribute


Attribute used to specify that a parameter from a parameterized test is the instance under test. Under this assumption, Pex ensure that the parameter is not null and it matches the type precisely:

void Test([PexAssumeUnderTest]Foo target, int value) {
// precondition: target is under test, we don't care about a null value
    target.Bar(value);
}

See Also

PexAssumeNotNullAttribute

PexPackageAssemblyAttribute


Attribute used to specify an assembly that contains additional packages. This attribute is used to load bundle multiple packages into a single assembly and load on the test assembly with a single attribute. See Packaging Extensions for an example of usage.

See Also

PexPackageTypeAttribute

PexPackageTypeAttribute


Attribute used to specify an type is annotated with additional packages. See Packaging Extensions for an example of usage.

PexUseTypesAttribute


This attribute is derived from PexUseTypesAttributeBase. It tells Pex that it can use a particular type to instantiate (abstract) base types or interfaces.

Example:

[PexMethod]
[PexUseType(typeof(A))]
[PexUseType(typeof(B))]
public void MyTest(object testParameter)
{
     ... // Pex will consider types A and B to instantiate 'testParameter'
}

PexIgnoreAttribute


Attribute used to mark a test as ignored. Pex will not execute the test and emit a warning with the specified message. This attribute can be set at the class and method level.

Example

  • test level,
public partial class MyTest {
    [PexMethod]
    [PexIgnore("Blocked by bug", WorkItem = 123) ]
    public void SomeTest(int i ) {...}
}

  • fixture level, all tests are ignored,
[PexClass]
[PexIgnore("Not implemented yet") ]
public partial class MyTest {
    [PexMethod]
    public void SomeTest(int i ) {...}
}

See Also

PexClassAttribute, PexMethodAttribute, PexIgnoreAttribute

PexSuppressStackFrameFromNamespaceAttribute


Attribute to specify namespaces that should be filtered out from the stack traces. This option is useful for extension writers, such as test framework integration, where the stack frames of the test framework code is not relevant to the user and can be stripped out.

[assembly: PexSuppressStackFrameFromNamespace("Microsoft.VisualStudio.QualityTools.UnitTestFramework")]

PexSuppressUninstrumentedMethodFromAssemblyAttribute


Attribute that suppresses uninstrumented method warnings coming from a given assembly.

[assembly: PexSuppressUninstrumentedMethodFromAssembly("MyAssembly")]

Tip: In Visual Studio, Pex automatically suggests and inserts this attribute.

PexSuppressUninstrumentedMethodFromNamespaceAttribute


Attribute that suppresses uninstrumented method warnings coming from a given assembly.

[assembly: PexSuppressUninstrumentedMethodFromNamespace("System.Collections")]

Tip: In Visual Studio, Pex automatically suggests and inserts this attribute.

PexCrossProductExplorableStrategyAttribute


This attribute is derived from PexExplorableStrategyAttributeBase. It tells Pex to try creating objects by calling a constructor or factory method, followed by all possible sequences of mutator methods.

For example, the following parameterized unit test will (2^^3)=8 different sequences, i.e. all the combinations of Add and Remove up to length 3.

[TestClass, PexClass]
public partial class ArrayListTest {
    [PexMethod]
    [PexCrossProductExplorableStrategy(MaxLength=3)]
    [PexExplorableMutator(typeof(ArrayList), "Add")]
    [PexExplorableMutator(typeof(ArrayList), "Remove")]    
    public Insert([PexAssumeNotNull]ArrayList list, int index, object elem) {
          list.Insert(index, elem);
          PexAssert.True(list.Contains(elem));
    }
}

PexExplorableFromConstructorAndSettersAttribute


This attribute is derived from PexExplorableAttributeBase.

It tells Pex how to create an instance of a class by
  • exploring one of its constructors
  • by assigning visible mutable fields
  • and by assigning properties with visible setters.

This attribute is a generalization of the PexExplorableFromConstructorAttribute which could only handle a single constructor call.

  • For example, the following classes have private fields, and Pex should not create arbitrary instances. Moreover, the Node class has state (Left and Right) that cannot be set through the constructor and requires calling property setters.

public class Node {
    public Node() {}
    public int Left;
    public Node Right { get; set; }
}

  • The following assembly-level attribute tells Pex how to create instances of Nodeclasses by using it's constructors, fields and property setters:

[assembly: PexExplorableFromConstructorAndSetters(typeof(Node))]

See PexExplorableFromConstructorAttribute for an example on how to use this attribute.

PexExplorableFromConstructorAttribute


This attribute is derived from PexExplorableAttributeBase.

It tells Pex how to create an instance of a class by exploring one of its constructors, which may take arguments that Pex has to create by exploring other constructors...

  • For example, the following classes have private fields, and Pex should not create arbitrary instances.

public abstract class Tree {
    public sealed class Leaf : Tree { 
        private int value;
        public Leaf(int value) {
            this.value = value;
        }
        public int Value {
            get { return this.value; }
        }
    }
    public sealed class Node : Tree {
        private Tree left, right;
        public Node(Tree left, Tree right){
            PexAssume.NotNull(left);
            PexAssume.NotNull(right);
            this.left = left;
            this.right = right;
        }
        public Tree Left {
            get { return this.left; }
        }
        public Tree Right {
            get { return this.right; }
        }
    }
}

  • The following assembly-level attribute tells Pex how to create instances of these classes by using their constructors:

[assembly: PexExplorableFromConstructor(
    typeof(Tree.Leaf),           // class can be explored from its constructor which takes
    typeof(int))]                // one parameter of type int
[assembly: PexExplorableFromConstructor(
    typeof(Tree.Node),           // class can be explored from its constructor which takes
    typeof(Tree), typeof(Tree))] // two parameters of type Tree

  • Then Pex can create instances of the subtypes of Tree in the following test. Note the PexUseTypeAttribute, which tells Pex which types it may use.

[PexMethod]
[PexUseType(typeof(Tree.Leaf))]
[PexUseType(typeof(Tree.Node))]
public void TestTree(Tree t) {
   Tree.Node n = t as Tree.Node;
   if (n != null) {
      Tree.Node nl = n.Left as Tree.Node;
      if (nl != null) {
          Tree.Node nlr = nl.Right as Tree.Node;
          if (nlr != null) {
              Tree.Leaf nlrr = nlr.Right as Tree.Leaf;
              if (nlrr != null && nlrr.Value == 42)
                  throw new Exception("found it");
          }
      }
   }
}

  • Pex finds a minimal tree that triggers the exception immediately. The following is a test case Pex generates.
Tree.Leaf l0 = new Tree.Leaf(42);
Tree.Node n0 = new Tree.Node(l0, l0);
Tree.Node n1 = new Tree.Node(l0, n0);
Tree.Node n2 = new Tree.Node(n1, n1);
this.TestTree(n2); // throws Exception

PexExplorableFromFactoriesAttribute


This attribute is derived from PexExplorableAttributeBase.

This attribute has Pex scan an assembly for explorable factory methods, i.e. static method marked with PexFactoryMethodAttribute contained in a static type.

  • attribute declaration in PexAssemblyInfo.cs,

[assembly: PexExplorableFromFactories("MyAssembly.Tests")]

  • an example of type that is hard to create: Account has no public constructor; one has to call the static method Create and set the Money property to set fully set the state of Account:

class Account {
    public int Money {get; set;} // can't be set publicaly
    public readonly int ID; // can only be set through the ctor
 
    private Account(int ID) { this.ID = id; } // private .ctor
 
    // this is the factory we'll need to call
    // in general, this can be a non-trivial guess for Pex
    static Account Create(int id) {
        return new Account(id);
    }
}

  • an example of factory method:
public static class AccountFactory {
     // factory for the Account type that
     // sets the ID and Money field
     [PexFactoryMethod(typeof(Account))]
     public static Account CreateAccount(int id, int money) {
         return Account.Create(id) { Money = money; }
     }
}

PexExplorableFromMethodAttribute


This attribute is derived from PexExplorableAttributeBase.

It tells Pex how to create an instance of a class by exploring a visible factory method returning an object of the desired type. The factory method may take arguments that Pex has to create by exploring other constructors...

For example, the following class has private fields, and Pex should not create arbitrary instances. The only way to create instances is by calling one of the two factory methods, MakeLeaf and MakeNode.

public abstract class Tree {
    public sealed class Leaf : Tree { 
        private int value;
        internal Leaf(int value)  {
            this.value = value;
        }
        public int Value  {
            get { return this.value; }
        }
    }
    public sealed class Node : Tree
    {
        private Tree left, right;
        internal Node(Tree left, Tree right) {
            PexAssume.IsNotNull(left);
            PexAssume.IsNotNull(right);
            this.left = left;
            this.right = right;
        }
        public Tree Left {
            get { return this.left; }
        }
        public Tree Right {
            get { return this.right; }
        }
    }
    public static Tree MakeLeaf() { return new Leaf(); }
    public static Tree MakeNode(Tree left, Tree right) {
        return new Node(left, right);
    }
}

The following assembly-level attribute tells Pex how to create instances of these classes by using the factory methods:
[assembly: PexExplorableFromConstructor(
    typeof(Tree.Leaf),                    // class that we create instances of
 
    typeof(Tree),                         // declaring type of factory method
    "MakeLeaf",                           // name of factory method
    typeof(int))]                         // parameters of factory method
[assembly: PexExplorableFromConstructor(
    typeof(Tree.Node),                    // class that we create instances of
 
    typeof(Tree),                         // declaring type of factory method
    "MakeNode",                           // name of factory method
    typeof(Tree), typeof(Tree))]          // parameters of factory method

Then Pex can create instances of the subtypes of Tree in the following test. Note the PexUseTypeAttribute, which tells Pex which types it may use.

[PexMethod]
[PexUseType(typeof(Tree.Leaf)), PexUseType(typeof(Tree.Node)), PexUseType(typeof(Tree))]
public void TestTree(Tree t) {
    Tree.Node n = t as Tree.Node;
    if (n != null) {
        Tree.Node nl = n.Left as Tree.Node;
        if (nl != null) {
            Tree.Node nlr = nl.Right as Tree.Node;
            if (nlr != null) {
                Tree.Leaf nlrr = nlr.Right as Tree.Leaf;
                if (nlrr != null && nlrr.Value == 42)
                    throw new Exception("found it");
            }
        }
    }
}

Pex finds a minimal tree that triggers the exception immediately. The following is a test case Pex generates.
Tree.Leaf _r0 = Tree.MakeLeaf(42);
Tree.Node _r1 = Tree.MakeNode(_r0, _r0);
Tree.Node _r2 = Tree.MakeNode(_r0, _r1);
Tree.Node _r3 = Tree.MakeNode(_r2, _r2);
this.TestTree(_r3); // throws Exception

PexExplorableMutatorAttribute


An attribute that specifies a method as an 'mutator', i.e. a method that modifies the state of an object. Mutators will be used by an explorable strategy to build method sequences.

Example

The following test inserts an element in the System.ArrayList collection. Since the collection contains special code to rescale the array, one needs to generate different method sequences to hit certain codepaths.

[TestClass, PexClass]
public partial class ArrayListTest {
    [PexMethod]
    [PexExplorableMutator(typeof(ArrayList), "Add")]
    [PexExplorableMutator(typeof(ArrayList), "Remove")]    
    public Insert([PexAssumeNotNull]ArrayList list, int index, object elem) {
          list.Insert(index, elem);
          PexAssert.IsTrue(list.Contains(elem));
    }
}

See Also

IPexExplorableMutator, IPexExplorableMutatorFactory, IPexExplorableStrategy
Internal use only.

PexInjectExceptionsOnUnverifiableUnsafeMemoryAccessAttribute


Attribute that instructs Pex to check all usages of pointers, i.e. all indirect memory reads and writes.

Overview


If Pex cannot trace back a pointer to a valid memory region on an indirect memory access, it injects a an exception at the point of the indirect access. By default, the injected exception is the special uncatchable PexUnverifiableUnsafeMemoryAccessException; you can pass a different type of the constructor of this attribute, e.g. a NullReferenceException, as specified in the ECMA-335 standard.
If the pointer depends on the test inputs, Pex will even try to compute test inputs which will bring the pointer out of its memory region.

A test case generated by Pex in this way may not reproduce the error when run by itself. You have to analyze the test case and the provided stack-trace.

Example


Pex will find several interesting corner cases for the following test:
  • An invalid memory access.
  • A valid memory access that does not find the 'l' character
  • A valid memory access that does find the 'l' character

[PexMethod]
[PexInjectExceptionsOnUnverifiableUnsafeMemoryAccess]
unsafe public void TestWithPointers(int i)
{
    fixed (char* p = "Hello")
    {
        if (*(p + i) == 'l')
            Console.WriteLine("l");
    }
}

PexAllowedExceptionAttribute


Attribute extending PexExceptionValidatorAttributeBase.

If this attribute is attached to a PexMethod (or to a PexClass), then it changes the default logic of Pex to decide when tests fails: The test will not be considered as failed even if it throws the specified exception.

Example


The following test says that the constructor of Stack may throw an ArgumentOutOfRangeException:
class Stack {
  int[] _elements;
  int _count;
  public Stack(int capacity) {
    if (capacity<0) throw new ArgumentOutOfRangeException();
    _elements = new int[capacity];
    _count = 0;
  }
  ...
}

The filter is then attached to a fixture as follows (it can also be defined on the assembly or test level):

[PexMethod]
[PexAllowedException(typeof(ArgumentOutOfRangeException))]
class CtorTest(int capacity) {
  Stack s = new Stack(capacity); // may throw ArgumentOutOfRangeException
}

See also

PexExpectedExceptionAttribute, PexMethodAttribute

PexExpectedCoverageAttribute


Exploration package attribute that specifies expected coverage values. This attribute implements PexExplorationPackageAttributeBase.

Example 

using Microsoft.Pex.Framework;
...
 
[TestClass]
[PexExpectedCoverage(100)] // we expect to cover 100%, on each test
public partial class MyTest
{
    ...
}

See Also

TestClassAttribute, PexClassAttribute

PexExpectedExceptionAttribute


Attribute extending PexExceptionValidatorAttributeBase.

If this attribute is attached to a PexMethod (or to a PexClass), then it changes the default logic of Pex to decide when tests fails: The test will be considered a as failed if it does not throw the specified exception.

For example, the following test says that no matter what the initial capacity of a stack is, Pop called on the empty stack must always throw InvalidOperationException.
class Stack {
  int[] _elements;
  int _count;
  public Stack(int capacity) {
    _elements = new int[capacity];
    _count = 0;
  }
  public void Pop() {
    if (_count==0) throw new InvalidOperationException(); 
    ...
  }
}


[PexMethod]
[PexExpectedException(typeof(InvalidOperationException))]
void PopFailureTest(int capacity) {
  Stack s = new Stack(capacity);
  s.Pop(); // should throw InvalidOperationException
}


See also
PexAllowedExceptionAttribute

PexExpectedTestsAttribute


Exploration package attribute that specifies expected test production values. This attribute implements PexExplorationPackageAttributeBase.

Example 
using Microsoft.Pex.Framework;
...
 
[TestClass]
[PexClass]
[PexExpectedTests(TotalCount = 5)] // we expect to create 5 tests
public partial class MyTest
{
    ...
}

Note


This attribute is mostly designed to test Pex itself.

See Also

TestClassAttribute, PexClassAttribute

PexInstrumentMarkedByAttribute


Attribute used to specify types from a given assembly, marked with a particular attribute to be instrumented. This class implement PexInstrumentTypeAttributeBase.

This attribute is useful to be able to define a custom attribute that specifies types to instrument, without requiring a reference to the Pex assemblies.

Example


This examples shows how to define an attribute to mark types to be instrumented, then use the PexInstrumentMarkedByAttribute attribute to tell Pex to instrument them.

// in the product
[AttributeUsage(AttributeTargets.Class, AllowMultiple = false)]
public sealed class MyInstrumentedAttribute : Attribute {}
 
// marking types
[MyInstrumented]
public static class MyAssert { ... }


// loading types in pex
using Microsoft.Pex.Framework;
 
[assembly: PexInstrumentMarkedBy(typeof(MyAssert), typeof(MyAssert))]

PexInstrumentNamespaceAttribute


Attribute used to specify that all types of a given namespace should be instrumented. This attribute implements PexInstrumentTypeAttributeBase.

Example 

// we want to instrument all types in the namespace MyNamespace.Sub contained in the assembly that contains the type SomeTypeOfAnAssembly.
[assembly: PexInstrumentNamespace(typeof(SomeTypeOfAnAssembly), "MyNamespace.Sub")]

PexInstrumentTypeAttribute


Attribute used to specify a type to instrument. This attribute implements PexInstrumentTypeAttributeBase.

Example 

// we want to instrument a custom assertion type
[assembly: PexInstrumentType(typeof(MyCustomAssert))]

PexSubstitutionAssemblyAttribute


An attribute used to specify an Assembly that contains additional Code Substitutions.

Example 

// MySubstitutionType is a type of the assembly that contains
// the substitutions
[assembly: PexSubstitutionAssembly(typeof(MySubstitutionType))]

PexFocusOnAssemblyAttribute


This attribute derives from PexFocusOnAttributeBase. It defines where Pex should focus its search. Also, focused code is included in the coverage analysis.

This attribute lets Pex focus on all types defined in the assembly given by an exemplary type of that assembly.

Example 

[assembly: PexFocusOnAssembly(typeof(SomeTypeDefinedInTheProductAssembly))]

PexFocusOnNamespaceAttribute


This attribute derives from PexFocusOnAssemblyAttribute. It defines where Pex should focus its search. Also, focused code is included in the coverage analysis.

This attribute lets Pex focus on all types defined in the given namespace of the assembly given by an exemplary type of that assembly.

Example 

[assembly: PexFocusOnNamespace(typeof(SomeTypeDefinedInTheProductAssembly), "MyProduct.SomeSubnamespace")]

PexFocusOnTypeAttribute


This attribute derives from PexFocusOnAttributeBase. It defines where Pex should focus its search.

This attribute lets Pex focus on all types defined in the assembly given by an exemplary type of that assembly.
Also, focused code is included in the coverage analysis.

Example

The following example will test the interactions between the types A, B and C.

[PexMethod]
[PexFocusOnType(typeof(A))]
[PexFocusOnType(typeof(B))]
[PexFocusOnType(typeof(C))]
public void EqualsTest(object a, object b) 
{
    PexAssume.IsTrue(a!=null && a.Equals(b));
    PexAssert.AreEqual(a.GetHashCode(), b.GetHashCode());
}

PexCreatableAsSingletonAttribute


This attribute is derived from PexCreatableAttributeBase.
It indicates that a type is implemented using the singleton pattern, and it tells Pex how to obtain the singleton instance by
  • calling a parameterless static method, or
  • calling a static property getter, or
  • reading a static field.
The accessor must be visible.

For example, if you have defined the following type,

public class MySingletonType {
     private MySingletonType() {}
     
     public static readonly MySingletonType TheInstance = new MySingletonType();
     
     public static bool IsMySingletonType(object o) {
           if (o is MySingletonType)
                return true;
           else
                return false;
     }
 
     ...
}

The creatable definition:
[assembly: PexCreatableAsSingleton(typeof(MySingletonType), "TheInstance") ]

Then the test
[PexClass]
public class MyPexTest {
     [PexMethod]
     public void Test(object o) {
          PexAssert.IsTrue(
               IsMySingletonType(o) == (o is MySingletonType)
          );
     }   
}

Will produce two test cases which give full code coverage:
Test(MySingletonType.TheInstance);
and
Test(null);

See Also

PexClassAttribute, PexCreatableAsSingletonAttribute, PexMethodAttribute

PexCreatableAsXmlAttribute


This attribute is derived from PexCreatableByConstructorAttribute, designed for type that have been automatically generated from an XSD schema using xsdgen.

More specifically, Pex expects

  • a public default constructor,
  • for each field fooField, a public property Foo with a setter/getter.

See Testing Web Services for an example.

Bulk define web data objects


Pex also provides a specialized attribute that will define all xml data types from an assembly that match a particular xml namespace, tool name or namespace (see PexCreatablesAsXmlFromAssemblyAttribute).

PexCreatableByClassFactoryAttribute


This attribute is derived from PexCreatableAttributeBase.

It tells Pex how to create an instance of a data type T as follows. The attribute points to a factory class written by the user. The factory class must implement IPexClassFactory<T>, and it must contain one property per field of the data type T. These properties are linked to the fields of the data type T by the PexFieldBindingAttribute. Pex will set all the properties according to how Pex would like to initialize the fields of the data type T. Then Pex will call the method IPexClassFactory<T>.Create() which will then create a properly initialized instance of the data type T.

Example:

The following BigNumber class has a couple of private fields.

public class BigNumber {
    // there is no direct way to set these private fields
    private int low, high;
    public BigNumber(ulong x) {
        this.low = (int)x;
        this.high = (int)(x>>32);
    }
 
    public ulong Value {
        get { return ((ulong)(uint)this.low) | (((ulong)(uint)this.high) << 32); }
    }
}

Since the constructor sets all fields without parameter validation, we can create a IPexClassFactory for BigNumber. Pex will set the properties of the factory class and then call the Create method to create the desired instance.

public class BigNumberFactory : IPexClassFactory<BigNumber> {
    int low, high;
    [PexFieldBinding("low")] 
    public int Low { set { this.low = value; } }
    [PexFieldBinding("high")] 
    public int High { set { this.high = value; } }
 
    public BigNumber Create() {
        // here we heave to do the 'reverse' of how the Point encodes its data
        return new BigNumber(((ulong)(uint)this.low) | (((ulong)(uint)this.high) << 32));
    }
}

We have to tell Pex about the factory class, e.g. by the following assembly level attribute:

[assembly: PexCreatableByClassFactory(typeof(BigNumber), typeof(BigNumberFactory))]

Now Pex knows how to create instances of BigNumber, for example for the following parameterized unit test.

[PexClass]
public class ClassFactoryTests {
    [PexMethod]
    [PexExpectedTests(TotalCount = 3)]
    public void BigNumberTest(BigNumber n) {
        if (n!=null && n.Value == 0x0500000007u)
            Console.WriteLine("gotcha");
    }
}

Pex will create three tests:

this.BigNumberTest(null);

BigNumberFactory bnf0 = new BigNumberFactory();
bnf0.Low = -1;
bnf0.High = -1;
this.BigNumberTest(bnf0.Create()); 

BigNumberFactory bnf0 = new BigNumberFactory();
bnf0.Low = 7;
bnf0.High = 5;
this.BigNumberTest(bnf0.Create()); 
// prints gotcha

Note: The properties and the Create method of the factory class must not throw exceptions. Not even ArgumentException. They should make 'best effort' to create an instance. Consider using an attribute deriving from PexExplorableAttributeBase.

PexCreatableByConstructorAndSettersAttribute


This attribute is derived from PexCreatableByMethodAndSettersAttribute.

It tells Pex how to create an instance of a data type by calling a constructor to create a raw instance, and then calling a sequence of property setters or setter methods.

For example, the following class has private fields.

public class Point
{
     private int _x, _y, _color;
     public Point(int x, int y) {
          _x = x; _y = y;
     }
 
     public int Color {
          get { return _color; }
          set { color = value; }
     }
 
     public int X {
          get { return _x; }
     }
     public void MoveX(int deltaX) {
          _x += deltaX;
     }
}

The following assembly-level attribute tells Pex how to create instances of this type with particular field values:
[assembly: PexCreatableByConstructorAndSetters(
     typeof(Point),         // type we want to create instances for
 
     // mapping of fields to properties
     "^_(.*)$",             // regex pattern applied to all field names, selecting the part of the name after the initial underscore character
     "$1",                  // expression that yields name of property corresponding to field name; "$1" gets instantiated with the part of the field name that falls into the parenthesis above
     true,                  // we want case-insensitive property name matching
 
     // mapping of fields to constructor arguments
     "_x", "_y")            // two fields must be passed to the constructor and don't have backing property setters
]

Then Pex can create instances of the type Point in the following test:

[PexClass]
public class PointTestClass
{
     [PexMethod]
     public void Test(Point p, int deltaX)
     {
          int oldX = p.X;
          p.MoveX(deltaX);
          PexAssert.IsTrue(oldX + deltaX == p.X);
     }   
}

For example, a generated test could look as follows.

Point p = new Point(0, 0);
p.Color = 0;
Test(p, 0);

Note: The parameter types of the constructor must match the field types exactly. Also, neither the constructor nor the setters should throw an exception under any circumstances. Consider using an attribute deriving from PexExplorableAttributeBase instead.

See Also

PexClassAttribute, PexCreatableByConstructorAndSettersAttribute

PexCreatableByConstructorAttribute


This attribute is derived from PexCreatableByConstructorAndSettersAttribute.

It tells Pex that an instance of a data type can be created by just calling one of its constructors. For this to work it is necessary that the constructor receives the values of all fields as arguments.

See PexCreatableByConstructorAndSettersAttribute for an example that can also deal with fields which are not passed to any constructor but can be set by a property.

PexCreatableByMethodAndSettersAttribute


This attribute is derived from PexCreatableByMethodAndSettersAttributeBase.

It tells Pex how to create an instance of a data type by calling a constructor or method to create a raw instance, and then calling a sequence of property setters or setter methods.

For example, the following class has private fields.

public class Point {
     private int _x, _y, _color;
     private Point() {}
 
     public static Point Make(int x, int y) {
          Point p = new Point();
          p.x = x; 
          p.y = y;
          return p;
     }
 
     public int Color {
          get { return _color; }
          set { color = value; }
     }
 
     public int X {
          get { return _x; }
     }
     public void MoveX(int deltaX) {
          _x += deltaX;
     }
}

The following assembly-level attribute tells Pex how to create instances of this type with particular field values:

[assembly: PexCreatableByMethodAndSetters(
     typeof(Point),         // type we want to create instances for
 
     // mapping of fields to properties
     "_{0}",                // string format like pattern applied to all field names, 
                            // selecting the part of the name after the initial underscore character
     true,                  // we want case-insensitive property name matching
 
     // indicating creation method and mapping fields to arguments
     typeof(Point), "Make", // declaring type and name of static creation method
     "_x", "_y")            // two fields must be passed to the creation method and don't have backing property setters
]

Then Pex can create instances of the type Point in the following test:

[PexClass]
public class PointTestClass {
     [PexMethod]
     public void Test(Point p, int deltaX) {
          int oldX = p.X;
          p.MoveX(deltaX);
          PexAssert.IsTrue(oldX + deltaX == p.X);
     }   
}

For example, a generated test could be the following.

Point p = Point.Make(0, 0);
p.Color = 0;
Test(p, 0);

Note: The parameter types of the creation method must match the field types exactly. Also, neither the creation method nor the setters should throw an exception. Consider using an attribute deriving from PexExplorableAttributeBase if in doubt.

The following derived attributes provide shortcuts for common cases:

See Also

PexCreatableByMethodAttribute


This attribute is derived from PexCreatableByMethodAndSettersAttribute.

It tells Pex that an instance of a data type can be created by just calling a creation method. For this to work it is necessary that the creation method receives the values of all fields as arguments.

See PexCreatableByMethodAndSettersAttribute for an example that can also deal with fields which are not passed to the creation method but can be set by a property.

PexCreatablesAsXmlFromAssemblyAttribute


Attribute used to specify a set of web data type that should be created as creatable. The attribute loads the data type automatically from an assembly, given the xml namespace, tool name or namespace:

// web data type (code generated)
[GeneratedCodeAttribute("System.Xml", "2.0.50727.42")]
[SerializableAttribute]
[XmlTypeAttribute(Namespace="http://foo")]
public partial class MyRequest  {        
    private string appIDField;
        
    public string AppID {
       get { return this.appIDField; }
       set { this.appIDField = value; }
    }
}


// tell pex to load all data types from that namespace
[assembly: PexCreatablesAsXmlFromAssembly("SearchAssembly", XmlNamespace = "http://foo")]

See Also
PexCreatableAsXmlAttribute

PexFieldBindingAttribute


Used in factories defined by PexCreatableByClassFactoryAttribute.

PexGeneratedByAttribute


Attribute attached to test cases generated by Pex which identifies the exploration that generated the test. This attribute is used by Pex to do test bookkeeping.

Excample 
[PexClass, ...]
public class MyTests {
  [PexMethod]
  public void SomeTest(int i) {...}
 


    ...
    [TestMethod, ...]
    [PexGeneratedBy(typeof(MyTests)")]
    public void SomeTest_Int_12345() 
    {...}
}

See Also

Generated Unit Test Attributes

PexInjectedExceptionAttribute


Attribute used to specify the type and reason of an injected exception in a generated test. This attribute is added by Pex when generating the unit test.

Example 

[TestMethod, ...]
[PexInjectedException(typeof(ThreadAbortException))]
public void SomeTest_1234_1() {...}

PexNotReproducibleAttribute


Attribute used to specify that a generated unit test may not reproduce the failure. This can occur when fault injections was used.

Example 

// the bug was found by injecting some exception 'artificially'
[TestMethod]
[PexNotReproducible]
...
public void SomeGeneratedTest(){...}

PexRaisedExceptionAttribute


Attribute used in the generated test to specify the exception that Pex caught while executing the test.

Example 

// this test throws a NullReferenceException
[TestMethod, ...]
[PexRaisedException(typeof(NullReferenceException))]
public void MyTest_123456_123_0_2
{...}

See Also

Generated Unit Test Attributes

PexCoverageFilterAssemblyAttribute


Attribute that specifies an assembly to be ignored, excluded or included from the coverage reports. This attribute is useful to exclude the test assembly.

This attribute is a decoration attribute, i.e. it can be set at the Assembly, Class or Test level.

Example


The example below shows how to exclude the assembly that contains the type MyTest:

// exclude assembly containing the tests, i.e. containing the MyTest class
[assembly: PexCoverageFilterAssembly(PexCoverageDomain.Excluded, typeof(MyTest))];

Extensibility


This attribute inherits from the PexCoverageFilterAttributeBase attribute. User can inherit from that attribute to write custom coverage exclusion logic.

PexCoverageFilterMarkedByAttribute


Attribute that selects types tagged with a specifed attribute to be ignored, excluded or included from the coverage reports. This attribute is useful to exclude coverage of code that was auto-generated, etc....

This attribute is a decoration attribute, i.e. it can be set at the Assembly, type or exploration level.

Example


The example below shows how to excludes namespace ending in 'Tests':

// exclude all types marked with GeneratedCodeAttribute
[assembly: PexCoverageFilterMarkedBy(PexCoverageDomain.Excluded, typeof(GeneratedCodeAttribute))]


Extensibility


This attribute inherits from the PexCoverageFilterAttributeBase attribute. User can inherit from that attribute to write custom coverage exclusion logic.

PexCoverageExcludeNamespaceAttribute


Attribute that specifies a namespace to be ignored, excluded or included from the coverage reports. This attribute is useful to exclude coverage of code that was auto-generated, etc....

This attribute is a decoration attribute, i.e. it can be set at the Assembly, PexClass or Test level.

Example


The example below shows how to excludes namespace ending in 'Tests':

// exclude all types in namespace ending with 'Tests'
[assembly: PexCoverageFilterNamespace(PexCoverageDomain.Excluded, "Tests")]


Extensibility


This attribute inherits from the PexCoverageFilterAttributeBase attribute. User can inherit from that attribute to write custom coverage exclusion logic.
to be deleted

PexFactoryMethodAttribute


Attribute that specifies that a static method is a explorable factory method. See PexExplorableFromFactoriesAttribute for an usage example.

See Also
PexExplorableFromFactoriesAttribute, PexFactoryClassAttribute

PexCreatableAttributeBase


Abstract base attribute for defining Creatables Types.

PexCreatableByMethodAndSettersAttributeBase


This attribute is derived from PexCreatableAttributeBase.

It tells Pex how to create an instance of a data type by calling a constructor or method to create a raw instance, and then calling a sequence of property setters or setter methods.

Use one of the following derived attributes, which implement convient ways to describe the relationship between public methods and private fields:

PexDomainAttributeBase


This is an abstract base attribute. It maintains information about which values Pex should consider as inputs for the analyzed test.

In general, attributes derived from this attribute can be attached at the following places:

  • On the test assembly, test fixture, and test method. Attributes on the test method get precedence over those on the test fixture, and so on. The first arguments to the constructor indicate to which type or field the domain applies. When only a type is given, then it applies to all fields and parameter which have that type as the formal field or parameter type. When in addition to the type a field name is given, then it applies to that field of the type only. A number of special fields exist to make statements about array elements, array lengths, string elements, string lengths, and so on.

  • On a field of a class. The specified domain applies to this field.
// we assume Foo's name is not null
public class Foo  {
    [PexAssumeNotNull]
    public string Name;
}
 
[PexMethod]
public void SomeTest(Foo foo) { ... }


// we assume that foo is not null
[PexMethod]
public void SomeTest([PexAssumeNotNull] IFoo foo) { ... }

A set of derived attributes can be used to state assumptions over test inputs.

Another set of attributes can be used to give hints to Pex' constraint solver about which types and values it should consider when computing interesting test inputs.

See Also

PexAssumeNotNullAttribute, PexMethodAttribute

PexExceptionValidatorAttributeBase


Abstract attribute extending PexDecoratorAttributeBase and implementing IPexExceptionValidator.

Subclasses:

PexExplorableAttributeBase


Abstract base attribute for defining Explorable Types.

PexExplorableStrategyAttributeBase


This is an abstract base attribute. It tells Pex how to create instances of a class by calling a constructor, and a sequence of mutator methods.

Pex comes with the following set of derived attributes:

PexFocusOnAttributeBase


Abstract attribute class that defines where Pex should focus it's search.

When exploring execution paths, Pex may choose to explore some code areas more thoroughly than others. Using the PexFocusOn attribute family, one can specify where Pex should spend more cycles. Also, focused code is included in the coverage analysis.

The following attributes derive from this attribute:

PexInstrumentAssemblyAttributeBase


Abstract Attribute base class for specifying instrumented assemblies.

The attribute has an InstrumentationLevel property.

The following attributes derive from this abstract attribute:


See Also

PexInstrumentTypeAttributeBase

PexInstrumentTypeAttributeBase


Abstract attribute used to instruct Pex to instrument certain types.

The attribute has an InstrumentationLevel property.

The following attributes derive from this abstract attribute:

PexTestFrameworkAttributeBase


Assembly level attribute to register a custom test framework implementation.

This attribute is used to register a custom implementation of the ITestFramework interface, which is used by Pex to control the generation and detection of unit tests.

Additional examples are available in the Pex Extensions Project.

Example 

public sealed class MyUberTestFrameworkAttribute : 
    PexTestFrameworkAttributeBase {
    protected override ITestFramework CreateTestFramework(
        IPexComponent host) {
        return new TestFramework(host);
    }
 
    class TestFramework : AttributeBasedTestFrameworkBase {...}
}


// this attribute should be in the test assembly or test settings assembly
[assembly: MyUberTestFramework]
 
// now you can tell Pex to emit tests for this framework
[assembly: PexAssemblySettings(TestFramework = "MyUberTestFrameworkName")]

PexExplorationAttributeBase


Abstract base class to define new test attributes. PexMethodAttribute inherits from this attribute.

See Also

Abstract Attribute Pattern

PexAssumeFailedException


Exception thrown by PexAssume.

An execution path which terminates with this exception is silently ignored by Pex and does not cause the generation of a test case whose execution would trigger this path.

Custom Assumption Exceptions

Additional exception can be registered as 'assumptions' using the PexAssumptionViolationExceptionAttribute. Note that if your unit test framework has one, it will be automatically registered.

PexSymbolicValue


Static class to ignore constraints on parameters, and to print the symbolic information associated with values.

Usages


Normally, Pex tries to cover all execution paths of the code during. However, especially when computing assumption and assertion conditions, we do not want to explore all possible cases.

Example


This example shows the implementation of the PexAssume.Arrays.ElementsAreNotNull method. In the method, we ignore the constraints on the lengh of the array value, to avoid Pex trying to generate different sizes of array. The constraints are only ignored here. If the tested code would behave differently for different array lengths, Pex would still generate differently sized arrays from the constraints of the tested code.

public static void AreElementsNotNull<T>(T[] value)
    where T : class
{
    PexAssume.NotNull(value);
    // the followings prevents the exploration of all array lengths
    int len = PexSymbolicValue.Ignore<int>(value.Length);
 
    // building up a boolean value as follows prevents exploration
    // of all combinations of non-null (instead, there are just two cases)
    bool anyNull = false;
    for (int i = 0; i < len; ++i)
        anyNull |= value[i] == null;
 
    // was any element null?
    if (anyNull)
        PexAssume.Fail("some element of array is a null reference");
 }

See Also


PexAssume, PexAssert

Term Pretty Printing


In some cases, Pex shows information it learned from observing the program's execution as code snippet, for example when it suggests fixes and when it display the path condition.

These code snippets are derived from Pex' internal abstract representation of the program's behavior, and they might not be executable as is, and they might contain artefacts which look unnecessary complicated.

In the case of such code snippets shown in C# syntax, the following artefacts might be present:
  • A purely boolean expression may use the idiom x != false, or x == false instead of simply x, or !x. This is because in MSIL, booleans are represented as bytes, and there is no unique true value.
  • Pex interprets subexpressions which would normally throw an exception as undefined. Pex uses a three-valued logic to deal with undefined values. Thus, Pex might build an expression of the form 10/x & x!=0, which corresponds to x!=0 && 10/x in a regular C# program.
  • Pex analyzes arbitrary .Net, and some MSIL constructs cannot be represented in C#. As a result, you might see the following expressions.
    • methodof(<methodname>, queries the token of a method
    • methodof(object.<methodname>, performs a vtable lookup
    • fieldof(<fieldname>), queries the token of a field
  • Pex tracks the heap of the program, but it uses a representation which can sometimes not be expressed directly in C#. In particular:
    • The expression fill(x) represents a value array of infinite size whose values are x.
    • The expression m{[i0]=x1, [i1]=x2, ...} represents a modified version of the value array m that has been updated at various positions.
    • The expression s{.f1=x1, .f2=x2, ...} represents a modified version of the struct value s that has been updated at various fields.
  • An object which is different from all other objects, but whose precise way of creation does not matter, may be represented as new.
  • ...

IPexChoiceSession


Interface which can be used to draw auxiliary input values.
Instances of this interface can be obtained from the PexChoose.

Usage


While it is possible to draw a huge number of auxiliary input values from a single session, it is often better for Pex if you partition the input values into different sessions.
This is especially important if the test of the tested application are not exactly deterministic, i.e. if it may behave slightly differently on every run. If the input values are drawn from differently named sessions, then Pex might still be able to relate they usage to earlier runs.

Example


The following test obtains values are necessary to continue execution from the default PexChoose session.

public sealed class Key {
    public int Value;
    public override int  GetHashCode() { return this.Value; }
    public override bool  Equals(object obj) { return obj is Key && ((Key)obj).Value==this.Value; }
}
public enum Action { Add, Remove }

[PexMethod]
public void HashtableAddRemoveTest()
{
    IPexOracleSession s = PexChoose.DefaultSession;
    
    Hashtable h = new Hashtable();
    int len = s.ValueFromRange("len", 0, 4);
    int count = 0;
    for (int i = 0; i < len; i++) {
      switch (s.ChooseFrom("action", Action.Add, Action.Remove)) {
          case Action.Add: {
                  Key k = s.ValueNotNull<Key>("addKey");
                  PexAssume.IsTrue(!h.Contains(k));
                  h.Add(k, new object());
                  PexAssert.IsTrue(h.Contains(k));
                  count++;
                  break;
                }
          case Action.Remove: {
                  Key k = s.ValueNotNull<Key>("removeKey");
                  PexAssume.IsTrue(h.Contains(k));
                  h.Remove(k);
                  PexAssert.IsTrue(!h.Contains(k));
                  count--;
                  break;
             }
        }
    }
    PexAssert.AreEqual(h.Count, count);
}

See Also

PexChoose, Parameterized Mocks

AppendFormat


This sample comes with Pex.

This tutorial shows how to
  • do parameterized unit testing with mock objects to implement interfaces,
  • test that an API does not throw unspecified exceptions.

The AppendFormat method of the StringBuilder class takes, besides other arguments, a value of an interface type.

... 
void AppendFormat(IFormatProvider provider, String format, params Object[] args) {
     if (format == null || args == null) {
          throw new ArgumentNullException((format == null) ? "format" : "args");
     }
     char[] chars = format.ToCharArray(0, format.Length);
     int pos = 0;
     int len = chars.Length;
     char ch = '\x0';
     ICustomFormatter cf = null;
     if (provider != null) {
          cf = (ICustomFormatter)provider.GetFormat(typeof(ICustomFormatter));
     }
     ...

With Pex, we can write a parameterized model for the IFormatProvider interface:

class PFormatProvider : IFormatProvider {
     public object GetFormat(Type formatType) {
          var chooser = PexChoose.FromCall(this);
          return chooser.ChooseResult<object>();
     }
}

After writing a simple test, which just states that the AppendFormat method should not throw any exception that has not been documented

[PexMethod]
public void TestAppendFormat(IFormatProvider formatProvider, string format, object[] args) {
     var sb = new StringBuilder();
     ... AppendFormat(... formatProvider, format, args);
}

Pex immediately finds a test which throws an exception:

InvalidCastException: Unable to cast object of type 'MFormatProvider' to type 'System.ICustomFormatter' 

var recorder = PexChoose.NewTest();
var mfp0 = new PFormatProvider();
recorder.OnCall(0, "MFormatProvider.GetFormat(Type)").Returns(mfp0);
string s0 = "";
object[] os0 = new object[0];
this.TestAppendFormat(mfp0, s0, os0);

The test parameter values are automatically logged by Pex. The result value also gets logged by Pex. Additionally, Pex add code in the generated test case to ensure that the resulting formatted strings does not change. This technique is useful for future regression testing using the generated test suite.

[PexMethod]
[PexAllowedException(typeof(ArgumentNullException))]
[PexAllowedException(typeof(FormatException))]
public string TestAppendFormat(string format, object[] args) {
    var formatProvider = new PFormatProvider();
    var sb = new StringBuilder();
 
    StringBuilderWrapper.AppendFormat(sb, formatProvider, format, args);
    
    return sb.ToString();
}

See Also

PexMethodAttribute, PexChoose

CoveragePublisher


Option of the PexAssemblySettingsAttribute.

Possible values:
  • None
  • NCover

TestLanguage


Option of the PexAssemblySettingsAttribute.

Sets the language of the emitted code for the generated test cases.

Possible values:
  • cs

See Also

Supported Test Languages

TestRootNamespace


Assembly settings that provides or override the root namespace of the generated test project. This setting is used in the process of building the generated test file tree.
The execution engine tracks the nature of the values that it deals with. However, it only tracks an abstraction of the rich .Net type system. We call this abstraction the “memory layout”, or short, “layout”. Each value is associated with one of the following layouts.


  • I, I1, I2, I4, I8 represents a native integer / unmanaged pointer, or a 1/2/4/8 byte long integer value. The layout does not indicate whether a value is signed; only instructions interpret a value as signed or unsigned.
  • R4, R8 represents a floating point value that is 4/8 byte long
  • Ref represents an object reference
  • ManagedPointer(l) where l is a “managed layout” represents a managed pointer to a memory layout with layout l
  • Struct(t) where t is a proper struct-type represents a struct-value

There are several auxiliary layouts, which do not exist in the real execution engine, but make a uniform representation of a program’s state and values easier:

  • Uniform(l, m) where l and m are “managed layouts” represents a mapping from l-values to m-values. In particular, the elements of an array are represented by a mapping from I4-values (in the 32-bit CLR) to some other layout. With the following MdIndex(r) layout, multi-dimensional arrays can be represented by mappings from MdIndex(r) to some other layout.
  • MdIndex(r) represents a r-tuple of I4-elements. This layout can represent a full index into a multi-dimensional array.
  • Type represents a TypeEx
  • Method represents a (possible abstract) Method
The following metadata entities exist; they are all subtypes of Microsoft.ExtendedReflection.Metadata.MetadataEntity.

  • TypeEx represents a fully instantiated type.
  • TypeDefinition represents a type definition, which might be a generic type definition.
  • Method represents a fully instantiated method that belongs to a fully instantiated type.
    • MethodBodyEx a type’s method body offers access to the decoded instruction sequence and exception handlers.
    • Instruction represents a decoded instruction that can be applied to an interpreter.
  • GenericMethod represents a generic method in a fully instantiated type.
  • MethodDefinition represents a method definition, which might be a generic method, and/or a method defined in a generic type. A method’s definition abstracts from the instantiation of its generic declaring type, and from the instantiation of a generic method. Method definitions are a useful concept to track code coverage that abstract from generic type instantiations.
    • MethodDefinitionBody contains information about a method body that is independent of the instantiation of the method.
  • Field represents a field that belongs to a fully instantiated type.
  • FieldDefinition represents a field definition, which might be defined in a generic type.
Metadata information can be obtained in a variety of ways. The following static classes contain facilities to this end.

  • MetadataFromRuntimeHandles Given a (or in some cases, a combination of) RuntimeTypeHandle, RuntimeMethodHandle or RuntimeFieldHandle, the corresponding meta data entities can be obtained. (Such runtime handles result from the ldtoken instruction, and represent the meta data information that is available to the execution engine at runtime. In some cases, this information is only partial, and complete meta data information can only be obtained by providing additional runtime type handles that indicate some context.)
  • MetadataFromGlobalIndices Each meta data entity in Microsoft.ExtendedReflection.MetaData has a GlobalIndex property that is assigned an index on the first use of the property. The first index of an entity is one, the second assigned index is two, and so on. Thus, the indices are dense, and allow an efficient implementation of a mapping over meta data indices in the form of arrays.
  • Metadata<T> By instantiating this generic class, one can obtain access to static meta data types.
  • MetadataFromReflection Given reflection meta data, i.e. instances of System.Type, System.Reflection.MethodBase or System.Reflection.FieldInfo, the corresponding meta data entities of the Microsoft.ExtendedReflection.Metadata library can be obtained.
  • MetadataForArrays This class allows to retrieve meta data definitions that correspond to some magic array functions, e.g. multi-dimensional arrays getters and setters.
  • SystemTypes This class offers convenient access to frequently used meta data entities.
If you have the token of a metadata entity defined in a particular module, you can use methods of ModuleEx to retrieve the metadata definitions.
The meta data factory contains facilities to synthesize new types that fulfill certain constraints. In particular, this allows to generate instantiations of generic types. Also, it can synthesize method bodies that can be used to create instances of arbitrary delegate types.
Memory regions is a concept to deal with unmanaged memory, and unmanaged pointers. The idea is that each non-null unmanaged pointer must point into some previously allocated memory region, and can thus be identified with the pair of the base address of the memory region plus an offset into the region. The static class MemoryRegions allows to track unmanaged memory regions.
The IThreadExecutionMonitor interface contains one method for each MSIL instruction. The abstract ThreadExecutionMonitorBase class simplifies the set of MSIL instructions, and introduces some abstractions. The IExecutionMonitor interface manages a set of threads.


There are two drivers for execution monitor:
  • The Method Body Executor executes the body of a method, instruction for instruction.
  • The ClrMonitor can instrument existing code to perform callbacks for each instruction in addition to the normal operation.
The executor drives an Execution Monitor.
A term in Microsoft.ExtendedReflection is a symbolic representation of computations or conditions over values of any .Net type.

Conceptually, a term is similar to a sequence of MSIL instructions, since they represent the manipulation of data. However, terms implemented are differently in mainly two points:
  • The term language is minimal, e.g. no term could be omitted without compromising completeness. Compare this to MSIL where many shortcuts exists for common operations.
  • Subterms can be shared in memory. This is similar to the concept of subroutines.

Terms are constructed and inspected with the TermManager.

This abstract class is the gateway to all data-manipulation operations. It allows to build terms from primitive (concrete) values and by combining terms, and it allows to decompose terms into their components. The TermManager distinguishes the following kinds of terms:

  • Constants:
    • Integer-constants (I, I1, I2, I4, I8)
    • Floating-point constants (R4, R8)
    • Object-reference constants (Ref)
    • (Fully instantiated) types (Type)
    • (Fully instantiated) methods (Method)
    • Struct-field identifiers (StructField)
    • Empty compound (Struct/Uniform)
    • A distinguished “undefined” value for every layout
    • Symbols that represent any value of a layout
  • Managed pointers (ManagedPointer) to
    • nowhere
    • static field
    • object field map of an instance field
    • argument of a stack frame of a thread
    • local variable of a stack frame of a thread
    • stack-top of the evaluation stack of a stack frame of a thread
    • an element of a compound value (struct or map)
  • Compound-related:
    • Selection of a value stored in a compound at a particular index
    • Update of a value stored in a compound at a particular index
  • Multi-dimensional array-related:
    • An index into a multidimensional array is described by a tuple of integers.
  • Type-system related:
    • Vtable-lookup given an object-reference and a virtual method
    • Selection of the element type of an array type
    • Check if values of one type are assignable to locations of another type
    • Selection of a property of an object, e.g. retrieving the type of an object, or the length of an array, or the content of a string
    • Invocation of a pure method
  • Arithmetic and other integer- and floating-point computations
    • Unary and
    • Binary computations
    • Conditional values
    • If-then-else

Compounds are used to represent different concepts:

  • A struct-value is represented as a mapping of the struct’s fields to the fields’ values
  • An instance field of a class type is associated with a mapping of object-references to the field’s values.
  • Conceptually, each array has an instance fields which holds a mapping of integer indices (or MdIndex-values in the case of multidimensional arrays) to the array’s elements.
This interfaces describes a program’s state abstractly. The state maintains different kinds of variable locations:

  • Static fields
  • Object field maps
  • Thread-local storage:
    • Stack frames, each containing a list of arguments, local variables, and an evaluation stack
The instruction interpreter implements the semantics of every MSIL instruction by performing the appropriate memory operations on a given State, using the TermManager to perform data manipulation. It also defines the conditions that determine how control flow will continue.
The Common Intermediate Language: The language of the instructions of .Net.
A class in Microsoft.ExtendedReflection which provides support to check if code in the current process can be monitored, methods to start and stop monitoring in the current process if enabled, and facilities to setup monitoring for a new process.


mscorlib


mscorlib is a .NET assembly which is tightly coupled with the .NET runtime system. Pex has limitations which prevent it from exploring certain classes present in this core runtime library.

CLRMONITOR_SUBSTITUTIONS


The environment variable CLRMONITOR_SUBSTITUTIONS may be set to a comma-separated list file names. Each file must contain an assembly, containing method substitutions. In a monitored process, call, callvirt, newobj, ldftn, ldvirtftn instructions in instrumented code will be redirected matching method substitutions.

  • A method substitution is a public, static method in a method substitution type.
  • A method substitution type is a type in a namespace with the prefix
    __Substitutions.
(including the final period).

Calls are redirected to method substitutions based on name-matching. I.e., a call to the method MyNamespace.MyType.MyMethod will be directed to __Substitutions.MyNamespace.MyType.MyMethod, if such a method substitution exists in any of the assemblies specified in the CLRMONITOR_SUBSTITUTIONS environment variable.

Rules and conventions


Three kinds of substitutions: (plain), ___redirect, ___latedirect


  • By default, method substitutions do not trigger any further callbacks in the same thread. Only if the name is appended with '___redirect', then the usual callbacks (if any have been requested) are issued.
  • By default, calls in the caller are rewritten. This makes only sense for non-virtual methods. Only if the name is appended with '___lateredirect', then the body of the callee is rewritten.
  • Only references to or the body of the methods in the exactly matching declaring type is replaced. (In particular, when replacing the body of a method with ___lateredirect, only the body in a particular type is replaced. When derived classes override the method again, that body is unaffected.) With one exception: All "void Finalize()" instance methods may be replaced by writing a substitution for System.Object.Finalize.

Naming Rules


  • Methods are matched based on names only. This means that if two assemblies are loaded into the same process, and these assemblies both define a method with the same namespace name, type name, and method name, then all calls to these methods are redirected to the same method substitution.

Visibility Rules


  • A method substitution must be a public, static method, in a public type.
  • As a consequence of the substitution method having to be public, all argument types must be public. There is a workaround if only the implicit 'this' argument is not public: Decorate the substitution with an attribute called __Substitutions.__NonPublicReceiverAttribute, and declare the receiver simply as 'object' (or 'UIntPtr' in case of structs).
  • If a private method is substituted, then the method substitution must be decorated with an attribute called __Substitutions.__NonPublicAttribute.

(Explanation: Even though ExtendedReflection makes some quite drastic changes to the program behavior, the code resulting from the instrumentation must still pass through the JIT pipeline, and somewhere in this pipeline are visibility checks, that cannot be suppressed. (At least I didn’t find a way.) Since the substitution methods reside in a different assembly than the original code, they can only be called if they are public, i.e. public methods in public types.)

Overloading Rules:


  • If a method is substituted, then all its public overloads must be substituted as well.
  • If any private method is substituted, then all private methods with the same name must be substituted as well.

(Explanation: The current implementation triggers substitutions only by matching names, not signatures.)

Rules for instance methods and constructors:


  • If an instance method is substituted, then the method substitution gets an additional first parameter: The (formerly implicit, and now explicit) instance parameter 'this'.
    • It will be a fresh instance when the constructor method substitution '___ctor_call' is called (see below).
    • If the method is an instance method or constructor of a value type ('struct' in C#), then the first parameter must by a managed pointer to the value (a 'ref' parameter in C#).
    • After the instance parameter (if any), a method substitution must have the exact same result type, parameters types and modifiers as the original method. (Their signatures must match.)
  • Instance constructors get a special treatment:
    • Their method substitutions are named '___ctor_call' and/or '___ctor_newobj' (instead of '.ctor').
    • Since constructor can be called like instance methods (e.g. when the constructor of a subtype calls the constructor of the supertype), a method substitution may exist named '___ctor_call' which gets an additional first parameter, just like all method substitutions of instance methods. This version has a void result type. (This version might not be necessary for special sealed classes, e.g. System.String, whose constructors are never called like instance methods.)
    • Since constructors can be invoked with the special newobj instruction, another method substitution may exist named '___ctor_newobj' which does not take an additional first parameter, but which instead returns a value of the declaring type of the original method.

GACing rules:


  • While the CLRMONITOR_SUBSTITUTIONS must refer to file names, the assemblies containing the substitutions also must be installed in the GAC.

Limitations:

  • At the time of writing, methods in generic types cannot be substituted (generic methods are supported, though). There is no conceptual problem, this feature is just not implemented yet. Please issue a feature request to pexdev@microsoft.com if desired.
  • Since a method substitution is public and must mention all parameters of the original method, it is not possible to substitute methods with non-public parameter or result types. Please issue a feature request to pexdev if desired.
  • If the static target of a callvirt instruction is redirected, the call is replaced by a non-virtual call. Note that the method substitution must match the method that statically appears in the callvirt instruction. Consider using the ___lateredirect suffix.
  • Methods invoked by calli and through delegates will not be redirected; however, the target of the ldftn instruction will be.

Other notes:

  • Be careful that the method substitutions do not get instrumented, unless you know what you are doing.

TODO

Move away from naming conventions, and use attributes instead.

NullReferenceException


An exception thrown by the program when an attempt is made to access memory with an invalid reference or pointer.
The following is a list of instructions which are instrumented in a special way.

Nop


Nop instructions do not cause a callback.

Localloc n


Before this instruction, a callback to BeforeLocAlloc(n) is inserted, where n is the number of bytes to be allocated, and after the instruction a callback to AfterLocAlloc(p) is inserted, where p is the address of the allocated memory.

Throw r


Before this instruction, a callback to DereferenceCheck(r, l) is inserted, where r is the reference to the exception about to be thrown, and l is an identifier of the code position of this instruction.

Bxx


After all conditional branches, a callback to either ConditionalBranchFallthrough(l) or ConditionalBranchTarget(l) is inserted, where l is an identifier of the taken branch, i.e. each conditional branch instruction is associated with two branch identifiers.

Switch


After each switch instruction, a callback to AtSwitchFallthrough(l) or AtSwitchTarget(i, l) is inserted, where i is the index of the switch target and l is an identifier of the taken branch, i.e. each switch with n targets is associated with (n+1) branch identifiers.

Callxxx


All kinds of call-instructions involving variable number of arguments (i.e. a call of a method with varargs calling convention) is preceded by a callback to VarArgTypes(types) where types is an array of the types of the additional arguments.

Calls to magic array methods that manipulate multi-dimensional arrays are turned into special callbacks V_Array_New, V_Array_Get, V_Array_Set and V_Array_Addr. (References to these methods which do not have regular metadata definitions are used to account for otherwise missing multi-dimensional array instructions.)

Calls to methods which have a corresponding method in the __Substitutions namespace of the Microsoft.ExtendedReflection.Monitoring assembly are redirected.

After regular calls, a callback to AtCallFallthrough is inserted that informs the monitorer that the callee did not throw an exception; in addition, if the method returns a value, a callback to CallResult<T>(v), CallResultPtr(v, t), CallResultTypedReference(v) or CallResultByRef<T>(a), where v is a value, t a type, and a a managed pointer.

When an instance method is called, a callback to CallReceiver announces the receiver object.

Callvirt


Before a virtual call, a callback to CallVirtType(t) is inserted, which indicates the type of object which decides to which method the call dispatches. If a virtual call is attempted on a null-reference exception, a NullReferenceException is thrown before execution reaches this point.

Unbox


After this instruction, a call to AfterBox(r) is inserted, where r is a reference to the object that holds the boxed value, if any.

Unbox.any


Before this instruction, a call to BeforeUnboxAny(r) is inserted, where r is the object reference that is about to be unboxed.

Ldfld, Ldsfld, Ldelem, VArrayGet


A callback to LoadedValue<T>(v), LoadedValuePtr(v, t), LoadedValueTypedReference(v) or LoadedValueByRef<T>(a) is inserted, where v is a value, t a type, and a a managed pointer.

Ldfld, ldflda, stfld


When special callbacks on field accesses are enabled, then the receiver object of the instance field is announced by a call to FieldReceiver. At this time, only receiver objects of fields of reference types are supported.

CLRMONITOR_FLAGS


If the environment variable CLRMONITOR_FLAGS is set, only some aspects of the monitored program will cause callbacks.
The value of the variable can be a sequence of the following characters:
  • 'M': EnterMethod / LeaveMethod callbacks
  • 'E': Callbacks for the exeptional behavior of all instrumented instructions (see 'c', 'f', 'o')
  • 'F': Callbacks for all normal behaviors of all instrumented instructions (see 'c', 'f', 'o')
  • 'A': Passes all arguments of method calls to the monitor
  • 'e': Callbacks for all exception handlers
  • 'p': Callbacks at all join points of the method, i.e. points which can be reached from more than one instruction
  • 'j': Callbacks for all branch instruction
  • 'c': Callbacks on all instructions which call methods (or get their addresses)
  • 'f': Callbacks on all instructions that access fields (or get their addresses)
  • 'o': Callbacks on all other instructions
  • 'L': Special callbacks on localloc
  • 'T': Special callbacks on throw
  • 'J': Special callbacks on branch instructions (e.g. whether they fall through or jump to a target)
  • 'C': Special callbacks on calling instructions (target method for virtual calls, receiver object for instance calls)
  • 'v': Special callbacks on instance field access instructions (ldflda, ldfld, stfld)
  • 'R': Special callbacks to pass all results of method calls to the monitor
  • 'G': Special callbacks to pass all values read from fields or array elements to the monitor
  • 'P': Special callbacks to pass all addresses (of non-locals) from which values are read or written to the monitor
  • 'V': Special callbacks to pass all addresses (of non-locals) from which values are read or written to the monitor, if the instruction has a 'volatile' prefix
  • 'B': Special callbacks after unbox instructions

In managed code, users can use the MonitorInstrumentationFlags enumeration and MonitorInstrumentationFlagsHelper helper class to create flag string.

Method Substitution


A call is substituted by a call to an atomic method call.

The target method can approximate the behavior of the original method such that it is compatible with the monitoring framework that is trying to observe the program. For example, System.Environment.Exit shouldn't simply terminate the process without telling the monitoring infrastructure.
  • This method can also call the original method.
  • This method can also compute an explicit symbolic representation of the behavior of the original method.

In short, this is a mechanism to deal with low-level issues.
Example: System.Environment.Exit

See Also
Code Substitutions

Method Redirection


A call is redirected to another method.

This method usually calls the original method, which cannot be instrumented, and another method, which is instrumented. The instrumented method is written in a way to resemble the behavior of the original method, such that the symbolic behavior induced by monitoring and exploring the instrumented method give an approximation of the behavior of the original method.
In short, this is a good mechanism to deal wth regular but complicated uninstrumented methods.
Example: System.String.StartsWith

See Also
Code Substitutions

Late Method Redirection


The body of a callee is redirected to another method.

This method usually calls the original method (in a protection context to avoid an infinite chain of redirections), which is not instrumented, and another method, which is instrumented. The instrumented method is written in a way to resemble the behavior of the original method, such that the symbolic behavior induced by monitoring and exploring the instrumented method give an approximation of the behavior of the original method.
In short, this is a good mechanism to deal wth regular but complicated uninstrumented methods.
Example: ToString

See Also
Code Substitutions

Method Interpretation


In addition to the regular execution of the uninstrumented method, the symbolic behavior of a method can be given explicitly.
In short, this is a good mechanism to deal with regular and simple uninstrumented methods. Method interpreters are written on a high abstraction level and can capture a set of methods.
Example: operator== for all types.

(A set of method interpretations is implemented directly in Microsoft.ExtendedReflection, and it is currently not user-extensible.)

See Also
Code Substitutions

Nondeterminism


For Pex, a program is non-determistic if it relies on inputs which Pex cannot control. Pex controls inputs given to parameterized unit tests and obtained from the PexChoose. In that sense, results of calls unmanaged or uninstrumented are also considered as 'inputs' to the instrumented program, but Pex cannot control them. As soon as the control-flow of the program depends on the particular values coming from those external sources, Pex is not able to 'steer' the program towards previously uncovered areas. The program becomes non-determistic if furthermore the values from external sources change when rerunning the program. In such cases Pex loses control over the execution of the program and its search becomes very inefficient.

It is sometimes not obvious which this happens. Consider the following examples:
  • The result of the GetHashCode() method is provided by unmanaged code and not predictable.
  • The System.Random class refers to the current time to deliver truely random values.
  • The System.DateTime class provides the current time, which is obviously not under the control of Pex.
  • ...
A method that can be defined, compiled, executed and reclaimed. This is part of the Lightweight Code Generation infrastructure added in .Net 2.0.


See Also

Limitations

Warning: Limitation 'xxx'


Pex computes test inputs by constraint solving. However, there are some operations that are beyond the scope of the constraint solver.

This currently includes
  • most floating point operations (only some linear arithmetic is support on floating point numbers)
  • conversions between floating point numbers and integers
  • all operations on the System.Decimal type

This warning appears because the executed code performed an operation or called a method that Pex cannot reason about.

See also: Observed Call Mismatch, Uninstrumented Method Called, Uninstrumentable Method Called, External Method Called, Testability Issue

Warning: Uninstrumented method 'xxx' called


Pex computes test inputs by monitoring the program execution. It is essential that the relevant code is properly instrumented so that Pex can monitor its behavior.

This warning appears because the instrumented code called methods in another, uninstrumented assembly. If you want Pex to explore the interaction of both, you have to instrument the other assembly (or parts of it) as well.

See also: Observed Call Mismatch, External Method Called, Uninstrumentable Method Called, Testability Issue, Limitation
Code Instrumentation

Pex monitors the execution of a test or program by inserting callbacks into the executed instruction sequence.

This is done by the component Microsoft.ExtendedReflection.ClrMonitor.

Custom Attributes


See MSDN 'Extending Metadata Using Attributes': http://msdn.microsoft.com/library/default.asp?url=/library/en-us/cpguide/html/cpconExtendingMetadataUsingAttributes.asp 

Browse the Pex Attribute Glossary to see a list of all custom attributes that Pex defines.

Pex Decoration Attribute


Decoration Attributes inherit from the abstract PexDecoratorAttributeBase attribute. Decorator attributes can be applied at three levels: assembly, class, and method.

There are several kinds of decorators:

For example, in the context of code coverage, a user might want to know the coverage that each test fixture has on its targetted code: What is the coverage of Foo and FooHelper produced by FooTest, what is the coverage of Bar and BarHelper produced by BarTest, etc... This can be done by setting the coverage inclusions attribute at the class level on FooTest and BarTest for helper types, and by adding an argument to PexClass for the main type-under-test. Here, PexCoverageFilterTypeAttribute is a decorator.

public class Foo {...}
public class Bar {...}
...
 
using Microsoft.Pex.Framework;
 
[TestClass]
[PexClass(typeof(Foo))]
// decorator attribute, applies to FooTest only
[PexCoverageFilterType(PexCoverageDomain.UserCodeUnderTest, typeof(FooHelper))]
public partial class FooTest 
{...}
 
[TestClass]
[PexClass(typeof(Bar))]
// decorator attribute, applies to BarTest only
[PexCoverageFilterType(PexCoverageDomain.UserCodeUnderTest, typeof(BarHelper))]
public partial class BarTest 
{...}

See Also

Fix It


Sometimes, when a test run fails, Pex can suggest a potential change to the source code to prevent the same failure from happening again.

Pex tries to locate the failure cause as follows.

  1. Pex determines the point in the execution of the test case where the failure manifested itself.
  2. Pex looks back in the execution trace what the last public method call was.
  3. Pex computes a condition under which the failure happened, relative to the last public method call.
  4. If the condition only involves parameters, Pex will suggest the negation of the condition as a missing precondition.
  5. Otherwise, Pex will try to express the condition in terms of the fields of the class of the last public method call. Pex will suggest the negation of the condition as a missing invariant. Furthermore, Pex will execute the test again, and try to find which public method of this class first left the object behind in a state which violates the proposed missing invariant. If Pex finds such a method, Pex will start over at 3.

This algorithm terminates because in each iteration Pex tries to find the failure cause at an earlier point in the execution trace.
If Pex suggests a missing precondition or invariant, following Pex' advice is guaranteed to prevent the same failure from happening again, under the assumption that Pex could monitor all relevant parts of the program. However, in the worst case, Pex could suggest a precondition or an invariant which is inconsistent, which basically means that Pex suggests to not run this code again.

Settings Assembly


A separate assembly containing assembly level attribute can be provided through the command line. This mode is useful to provide extensive settings for automated exploration mode such as unit test.

Examples 

pex.exe /mode:unittest /settingsassembly:MySettings.dll myunittests.dll 


// settings assembly, where MyUserAssembly.dll is the assembly under test.
[assembly: PexInstrumentAssembly("MyUserAssembly")] // make sure it is instrumented
[assembly: PexCoverageIncludeAssembly("MyUserAssembly")] // get some coverage data for MyUserAssembly
[assembly: PexUserAssembly("MyUserAssembly")] // useful to filter out ArgumentException issues
// injecting exception on field write
[assembly: PexInjectsExceptionOnWrite]

TestExcludePathBoundsExceeded


Execution paths which exceed the configured path bounds MaxCalls, MaxBranches, MaxStack, MaxConditions are ignored

This is an option of the PexSettingsAttributeBase and its derived types.

The motivation behind this exploration bound is to deal with (likely) non-terminating tests. When Pex hits an exploration bound like MaxCalls, MaxBranches or MaxConditions, it assumes that the test will not-terminating or cause a stack-overflow later on. Such test cases may pose problems to other test frameworks, and this attributes provides a way prevent Pex from emitting test cases for potentially non-terminating or stack-overflow causing test cases.

TestEmissionFilter - Indicates what kind of tests Pex should emit


This is an option of the PexSettingsAttributeBase and its derived types.

Possible values:
  • All - Emit tests for everything, including assumption violations
  • FailuresAndIncreasedBranchHits (default) - Emit tests for all unique failures, and whenever a test case increases coverage, as controlled by TestEmissionBranchHits
  • FailuresAndUniquePaths - Emit tests for all failures Pex finds, and also for each test input that causes a unique execution path
  • Failures - Emit tests for failures only

IPexExceptionValidator


Interface to customize Pex' treatment of tests which throw exceptions.

See Test Failures for more information.

Test Failure Explanation: Assertion violation


An assertion of the unit testing framework for which Pex generates tests was violated, and an assertion violation exception was thrown as the result.

See Also

Test Failures

Test Failure Explanation: MaxBranches exceeded


Pex limits the length of any execution path that it explores during Input Generation. This feature prevents Pex from getting stuck when the program goes into an infinite loop.

Each conditional and unconditional branch of the executed and monitored code is counted towards this limit, including branches which do not depend on the inputs of the parameterized test.

For example, the following code consumes branches in the order of 100:

for (int i=0; i<100; i++) { }



[PexMethod(MaxBranches=int.MaxValue)]
public void MyTest(...) {
    // ....
}



for (int i=0; 
    PexSymbolicValue.Ignore(i<100); // Pex will 'forget' about this path condition
    i++) 
{ }

See Also

Test Failures

Test Failure Explanation: MaxCalls exceeded


Pex limits the length of any execution path that it explores during Input Generation. This feature prevents Pex from getting stuck when the program goes into an infinite loop.

Each call (direct, indirect, virtual, jump) of the executed and monitored code is counted towards this limit.

The following example practically removes this bound:

[PexMethod(MaxCalls=int.MaxValue)]
public void MyTest(...) {
    // ....
}


See Also

Test Failures

Test Failure Explanation: MaxConditions exceeded


Pex limits the length of any execution path that it explores during Input Generation. This feature prevents Pex from getting stuck when the program goes into an infinite loop.

Each conditional branch which depends on the inputs of the parameterized test is counted towards this limit.

For example, each path in the following code consumes n+1 conditions:
[PexMethod]
void ParameterizedTest(int n) {
    // conditions are "0<n", "1<n", ..., "!(n<n)"
    for (int i=0; i<n; i++)  
    { ... }
    // irrelevant for MaxConditions, since conditions do not depend on input
    for (int i=0; i<100; i++) 
    { ... }
}



[PexMethod(MaxConditions=10000)]
void ParameterizedTest(int n) {
    // ...
}



[PexMethod]
void ParameterizedTest(int n) {
    int nshadow = PexSymbolicValue.Ignore(n); // Pex looses tack of 'n'
    // irrevelant for MaxConditions, since nshadow is not related to input
    for (int i=0; i<nshadow; i++)  
    {...}
}

See Also

Test Failures
If one specifies the location of the test project, Pex can resolve the output language, where to output the generate test files so they sit next to the 'definition' file. It may also patch the project file on the fly to include the new files.

Command line

  • To specify the project file. Pex will automatically update the project file (and make a copy of the old one)

pex.exe /testp:myproject.csproj ...

  • To specify the project file and a new file name for the updated version:

pex.exe /testp:myproject.csproj /testpnew:myproject.csproject ...

  • To compile the generated test project, 

pex.exe ... /testcp

Having the generated files at the right place

If one follows the .Net development guidelines for ordering the types (default behavior of Visual Studio when creating files), Pex can find accurately place each generated test file:
  • One type per file, the file name is equal to the type name,
  • The namespace hierachy translates into a hierarchy of subfolders (minus the default namespace)
  • If some of those rules are broken, Pex won't find the best place to write the generated tests, and will put them into the project root folder.

Patched project: Where are my files?


In order to avoid clutering the project (because you could end up with dozens of generated files), Pex adds the generated files as linked items under the 'definition' file. The screenshot below shows one generated file for the TriangleTest sample:

generatedtests.png
exported

exported is a .NET notion related to Visibility.

An exported member is either
  • a public type that is not nested, or
  • a nested public member whose declaring type is exported.

For example,
public class Outerclass 
{
  public class Innerclass 
  { 
    public int Field;
  }
}
contains an exported field, but in
public class Outerclass 
{
  // not public!
  class Innerclass 
  { 
    public int Field;
  }
}
only the Outerclass is exported.

Pex Component Model


Pex is built from individual components. Components are layered into the Pex (main) component, exploration components and path components:

  • Pex Components: A set of components is alive for the entire lifetime of the Pex process.
    • Exploration Components: In addition, a set of components is created and kept alive for the duration of a single test exploration.
      • Path Components: In addition, a set of components is created and kept alive for each execution path that is executed and monitored during the exploration of a parameterized test.

The user may customize the components and that exist and their configuration by writing Pex Packages, Exploration Packages, and Path Packages respectively.

PexInjectedExceptionAttribue


Attribute used to mark a generated unit test and specify the information about the exception that was injected.

This attribute is used when Pex injected exceptions in the program flow 'artificially'. Since this exception will not reproduce under a normal program execution, the information that the attribute contains is valuable to investigate the root cause of the failure.

[TestMethod]
[PexInjectedException(typeof(ThreadAbortException), "OnWrite")]
...
public void SomeGeneratedTest() {...}

Custom attribute used to mark an instance method as a unit test in MSTest.

Pex can generate such unit tests.

TestAttribute


Custom attribute used to mark an instance method as a unit test in NUnit.

Pex can generate such unit tests.

Parameterized Test Stubs


The Pex Wizard can generate stubs around any visible API. A test stub is fairly simple, it simply duplicates the signature of the API under test:

  • class under test,
public class Foo {
    public void Bar(int i) { ... }
}

  • test stub for bar,
[PexMethod]
public void Bar([PexAssumeUnderTest]Foo target, int i) {
    target.Bar(i);
}

Search Frontier Problem


After each run, Pex has to pick the next uncovered branch to cover. This particular choice is critical for the performance of the 'search'.

Samples

Benchmarks

Summaries


Ongoing work in Pex:

Method Sequence Generation Problem


When if we have chosen a constructor and a set of methods to mutate a constructed object,
in which order should we call the methods?

Samples

Benchmarks

Assertion Inference Problem


Ongoing work in Pex:

Here is some of our earlier work on the topic:

Reduction Rules


Pex reduces all expressions over symbolic variables to a normal form which is equivalent to the original expression.

Normal forms
For certain kinds of expressions, there is a unique normal form (e.g. polynomials).
However, for some kinds of expressions there isn't (e.g. integer arithmetic mixed with bitwise arithmetic).

Object Creation Problem


How to create objects?
Which constructor should be used, which methods should be used?

Samples

Benchmarks

exploration boundary MaxConstraintSolverTime was reached with value xs


Pex uses a constraint solver to compute new test inputs. Since constraint solving can be a very time consuming process, Pex allows to configure bounds, in particular a MaxConstraintSolverTime.

For many applications, increasing the time-out significantly will not result in better coverage. The reason is that most time-outs are caused by constraint-systems which have no solutions. But Pex might not be able to determine that it is inconsistent without trying all possible solutions, which will cause the time-out.

Test Failure Explanation: MaxStack exceeded


Pex limits the size of the call stack of any execution path that it explores during Input Generation. This feature prevents the Pex process from being terminated when a stack overflow occurs.

The following example practically removes this bound (not recommended):

[PexMethod(MaxStack=int.MaxValue)]
public void MyTest(...) {
    // ....
}


See Also

Test Failures

MaxRuns exceeded


Pex limits the number execution paths that it explores during Input Generation. This feature makes sure that Pex terminates when the program has loops or recursion.

Not every time Pex runs the parameterized test with particular inputs also causes Pex to emit a new test case. See TestEmissionFilter for more information.


[PexMethod(MaxRuns=2000)]
void ParameterizedTest(int n) {
    // ...
}

MaxRunsWithoutNewTests exceeded


Pex limits the number execution paths that it explores during Input Generation.

Not every time Pex runs the parameterized test with particular inputs also causes Pex to emit a new test case. See TestEmissionFilter for more information.

While Pex often finds many interesting test inputs initially, after a while, Pex does not emit any more tests.

This option governs how long Pex may keep trying to find yet another relevant test input.


[PexMethod(MaxRunsWithoutNewTests=2000)]
void ParameterizedTest(int n) {
    // ...
}

Critical Error: test inputs computed by constraint solver are not valid


This error is often the consequence of an earlier error, as explained below.

Pex uses a constraint solver to determine new test inputs. Sometimes, test inputs proposed by the constraint solver are invalid. This can happen when
  • certain constraints are not known, or
  • if values are created in a user-defined way, as defined by an attribute that derives from PexCreatableAttributeBase, then errors may occur in user-code, or
  • some of the involved types have an initialization logic not controlled by Pex (e.g. COM classes).

Please contact us  with the full report when you think Pex should be able to test the relevant classes.

Warning: Coverage Data Is Empty


Pex computes test inputs by monitoring the program execution. It is essential that the relevant code is properly instrumented so that Pex can monitor its behavior.

Even if the test is properly annotated, there are still a few reasons why this error may appear:
  • If all test inputs which Pex tried resulted in assumption violations, then no test will be generated, and the coverage of the generated tests is not existant. You can try to set the option TestEmissionFilter to All to see all tests Pex generated including those which violated assumptions.
  • There may be an installation issue. Pex uses an unmanaged profiler to monitor the execution. This profiler implements a COM interface. You can manually register it (although not recommended) with the following command:
  regsvr32 ...\Pex\bin\Microsoft.ExtendedReflection.ClrMonitor.x86.dll

Warning: debugonly and releaseonly are exclusives


When using the PexExpectedCoverage attribute, a user can specify to verify the coverage in debug or release mode only. Some optimization might occur in release mode wich might lead to unreachable code etc...

Debug mode and release mode flags are mutually exclusive.

Error: issue, defined in binding xxx


You used the PexCreatableByClassFactoryAttribute to tell Pex how to create instances of a particular type, and a property in the specified class was annotated with a PexFieldBindingAttribute, but one of the following the problems occurred:

  • The field-name specified by the attribute does not refer to a field of the type Pex wants to create.
  • The type of the field was different from the property type.
  • The property has index parameters.

Error: setter xxx has issues


You used an attribute deriving from PexCreatableByMethodAndSettersAttributeBase to tell Pex that it can initialize a data type by calling property setters, but a property setter was rejected by Pex.

The property must
  • be public,
  • be instance-based (not static),
  • have a setter,
  • have the correct type,
  • not have any additional index arguments.

Error: bad creation method (or similar)


You used an attribute deriving from PexCreatableByMethodAndSettersAttributeBase to tell Pex that it can create a data type by calling a creation method, but the creation method was rejected by Pex.

Error: missing creation method (or similar)


You used an attribute deriving from PexCreatableByMethodAndSettersAttributeBase to tell Pex that it can create a data type by calling a creation method, but Pex couldn't determine the creation method.

Error: creation method xxx returned null (or similar)


You used an attribute deriving from PexCreatableByMethodAndSettersAttributeBase to tell Pex that it can create a data type by calling a creation method, but the creation method returned a null reference, or a reference of an unexpected type.

Warning: field xxx is not public; Pex needs help to construct object (or similar)


Pex generates test inputs, and part of the inputs may be objects with fields. Here, Pex wants to generate an instance of an object which has a private field, and Pex believes that an interesting program behavior will occur when this private field has a particular value. However, while possible with Reflection, Pex does not dare to manufacture objects with arbitrary field values. Instead, in those cases it relies on the user to provide hints how to use the public methods of a class to create an object and bring it into a state where its private field has the desired value.

Read the chapter on Instantiating Existing Classes to learn how to help Pex in constructing interesting objects.

Warning: do not know any type assignable to xxx; Pex needs help to find types (or similar)


Pex generates test inputs for any .NET types. Here, Pex needs to create an instance that derives from an abstract class or implements a interface, and Pex does not know any type that fulfills the constraints.

You can help Pex by pointing to one (or more types) that match the constraints. Usually, one of the following attributes is convient.


For example, if Pex complains "do not know any types assignable to System.Collections.IDictionary", then you can help Pex by attaching the following PexUseTypeAttribute to the test (or to the fixture class):
[PexMethod]
[PexUseType(typeof(System.Collections.Hashtable))]
public void MyTest(IDictionary[] dictionaries) { ... }

You can also add an assembly-level attribute:
[assembly: PexUseType(typeof(System.Collections.Hashtable))]

Warning: will use xxx as xxx (or similar)


Pex generates test inputs for arbitrary .NET types. When a type are abstract or an interface, Pex needs to choose a particular implementation of that type. In order to make that choice, Pex needs to know which types exist. Here, Pex looked at a couple of referenced assemblies and found an implementation type, but Pex is not sure if it should use that type, or if there are more appropriate types available somewhere else. Pex simply picked a type which looked promising.

In order to get rid of this warning, you can either
  • Accept Pex' type choice (add a corresponding PexUseTypeAttribute), or
  • Guide Pex to use other types.

Warning: will use xxx to create instances of xxx (or similar)


Pex generates test inputs, and some of the parameters may be classes, so that Pex has to construct objects. Here, Pex wants to generate an instance of an object, but Pex is not sure what is the best way to do so. Pex simply picked a constructor of a type which looked promising.

In order to get rid of this warning, you can either

Read the chapter on Instantiating Existing Classes to learn how to help Pex in constructing interesting objects.

Error: Effects Not Enabled


The PexEffectiveExplorableMutatorsAttribute only works when you start Pex with the option /EffectsDirectory option, or when you run Pex in distributed mode.

Error: Effects need type under test


Effects are only collected for the type-under-test. You can set the type-under-test with the PexClass attribute:

[PexClass(typeof(MyTypeUnderTest))]
public class MyTestClass { ... }

Critical Error: unexpected exception while exploring test


An unexpected exception was caught while exploring a test. This event should not happen and is a bug in Pex. Please report this issue to mailto:pexbug@microsoft.com .

Read in detail How To Report a Pex Bug.

Error: TargetInvocationException


Diagnosis


An exception occurred in user code.

Repair


Inspect the stack-trace, and remove the bug in your code.

Critical failure: the Pex CLR profiler was not attached to the process


This message means that the instrumenting profiler was not attached to the process. This problem might be due to the following issues:

  • the environment variables to load the profiler were not set correctly. This happens if you call directly Microsoft.Pex.exe.
  • the profiler is not registered correctly on the machine.

Warning: External method 'xxx' called


Pex computes test inputs by monitoring the execution of the instructions of a .NET program. Pex cannot generate meaningful test inputs for code that is not written in .NET.

This warning appears because the instrumented code called an unmanaged, native method, which Pex cannot analyze. If you want Pex to explore the interaction of both, you have to mock the unmanaged method.

See also: Observed Call Mismatch, Uninstrumented Method Called, Uninstrumentable Method Called, Testability Issue, Limitation

Warning: Uninstrumentable method 'xxx' called


Pex computes test inputs by monitoring the execution of the instructions of a .NET program. However, there are some methods which Pex cannot monitor for technical reasons. For example, Pex does not monitor static constructor.

This warning appears because the instrumented code called a method that Pex cannot monitor.

See also: Observed Call Mismatch, Uninstrumented Method Called, External Method Called, Testability Issue, Limitation

warning: Uninstrumented Method From A One Point Zero Assembly Called


Pex cannot instrument assemblies compiled against any 1.x version of .net. (See Limitations).

Warning: Testability Issue


Pex computes test inputs by monitoring the program execution. Pex can only generate relevant test inputs when the program is deterministic, and when the relevant behavior is controlled by the test inputs.

This warning appears because during the execution of your test case a method was called which either behaves non-deterministically, or which interacts with the environment, for example, the methods of System.Random and System.IO.File. If you want Pex to create meaningful test inputs, you have to mock the methods which Pex flags as testability issues.

Michael Feathers provides a nice set of unit test rules  for 'pure' tests:

A test is not a unit test if:
  • It talks to the database
  • It communicates across the network
  • It touches the file system
  • It can't run at the same time as any of your other unit tests
  • You have to do special things to your environment (such as editing config files) to run it.
Tests that do these things aren't bad. Often they are worth writing, and they can be written in a unit test harness. However, it is important to be able to separate them from true unit tests so that we can keep a set of tests that we can run fast whenever we make our changes.

See Also

Observed Call Mismatch, Uninstrumented Method Called, External Method Called, Uninstrumentable Method Called, Limitation

Warning: Observed Call Mismatch


Pex computes test inputs by monitoring the program execution. However, Pex might not be able to monitor all instructions. For example, Pex cannot monitor native code, and Pex cannot monitor code that is not instrumented.

When Pex cannot monitor code, Pex cannot generate test inputs that are relevant to that code.

Often, Pex is not aware of the fact that it cannot monitor a method until a call to that method returns. However, the cause of this warning is that
  • Pex monitored some code, which initiated a call to an uninstrumented method.
  • The uninstrumented method called a method that is instrumented.
  • Pex monitors the called instrumented method.

Since Pex does not know what the uninstrumented intermediate method did, Pex might not be able to generate test inputs that are relevant to the instrumented nested call.

See also: Observed Call Mismatch, Uninstrumented Method Called, Uninstrumentable Method Called, External Method Called, Testability Issue, Limitation

Warning: Value Stored In Static Field


Pex can only systematically determine relevant test inputs when the unit test is deterministic, i.e. if it always behaves the same for the same test inputs. In particular, this means that the test should leave the system in a state behind which allows to re-execute that test. Ideally, the unit test should not change any global state, but all interactions with globals should be mocked.

This warning indicates that a static field was changed; this might make the test behave non-deterministically.

In some situations, changing a static field is okay:
  • When the test inputs setup/cleanup code that undoes the change.
  • When the field is only initiated once, and never changes its value afterwards.

Error: invalid fixture type: Foo


Fixture types must be 'public default constructible', i.e. they must
  • be a class,
  • be exported,
  • be non-abstract,
  • be not a generic type definition,
  • have a visible constructor.

[PexClass]
public class BadFoo
{
   private BadFoo() // Constructor not visible!
   {...}
}


[PexClass]
internal class InternalFoo {} // type not exported!


[PexClass]
public abstract AbstractFoo {} // abstract type!

Error: could not load assembly xxx


An invalid assembly name or filename was provided and Pex could not load that assembly. Please review the location of the failure and ensure that the assembly actually exists.

Warning: ignored exploration xxx


You annotated a test with the PexIgnoreAttribute.

Warning: ignored fixture xxx


You annotated a PexClass with the PexIgnoreAttribute.

Warning: do not know how to create instance of exception type xxx


You used an attribute deriving from PexInjectExceptionsOnCallAttributeBase to tell Pex to inject exceptions during a test run. However, some types that Pex was supposed to inject are not creatable -- e.g. they are abstract, or they do not have a public constructor without parameters.

There are several ways to address this problem:
  • You can set the parameter IgnoreUncreatableExceptionTypes of the attribute to true to simply ignore the problem.
  • If the exception type is not abstract, you can use an attribute deriving from PexCreatableAttributeBase to tell Pex how to create an instance.
  • If the exception type is abstract, you can set the parameter AllowExceptionSubTypes to true, and use attributes deriving from PexUseTypesAttributeBase to tell Pex which subtypes it may use.

Warning: Not supported: xxx


When you use PexInjectExceptionsOnXmlDocumentedCallsAttribute, Pex will try to obtain and parse the xml documentation file of the assembly to which calls are being made during the test.

An error occurred during parsing this file.

Warning: Could not find xml documentation file: error while locating assembly xxx


Pex tried to obtain the xml documentation file of an assembly which should contain information about which exceptions a method can throw.

Pex searches for the file as follows.
  • Same file name as assembly, but extension changed to .xml.
  • Same as above, but in the directory of the .NET installation.

Warning: could not load symbols for xxx


Diagnosis


The symbol file (.pdb) for the given module could not be found in the search path.
Certain diagnosis features of Pex work best if symbols are available.

Repair


  • Check that the symbols are available in the search path.
  • If you are using a symbol server, make sure symsrv.dll is in the path.

Warning: symbols could not merge source of xxx in yyy:zzzz


Diagnosis


The source range returned by the symbol file (.pdb) was outside of the source file range. Most likely, the symbols and sources are out of sync.

Repair


Ensure that the symbols and sources are in sync (see Symbols And Sources).

Error: cannot compile partial classes in new test project


This error occurs when Pex tries to compile the project containing the generated tests and emitted the generated tests as partial classes. Those modes are mutually exclusive since the created project will not compile.

To fix this error, either disable using partial classes using the TestNoPartialClasses flag or update the existing test project using the TestProject flag.

Warning: duplicate existing tests: xxx - xxx


Currently, when you run Pex, it always explores a program from scratch. Therefore, it might generate tests it had already generated before. Pex elimiates such duplicates tests as part of its Test Bookkeeping. However, since you got this warning, there seem to be two identical tests around.

Error: could not resolve test framework


Pex emits all test cases that it generates as code, decorated for a basic test framework which simply re-execute them. You got this error because Pex could not infer the test framework you would like to use. Pex looks through all referenced assemblies to find a unit testing framework. You can set it with the TestFramework option of the PexAssemblySettingsAttribute.

Note: In addition to adding a reference to a unit test framework, you must actually use some type from it. If you don't, the C# compiler silently removes the reference! For example, to keep the reference alive, tag the PexClassAttribute with a TestClassAttribute attribute.

Error: unit test mode requires a test framework supported attributes


You have selected the unit test execution mode but the test framework you are using does not use attributes.

Pex uses the custom attributes from the selected test framework to detect existing unit test. Therefore, it cannot operate if the test framework does use such approach.

Supported test frameworks that use attributes are MSTest, NUnit, MbUnit and xUnit.Net.

Error: cannot update readonly test project file


Pex attempted to update the test project file but the provided file is readonly. Make the file writable or provide a new project file name.

Error: test project compilation failed


Pex attempted to compile the test project (generated or updated) but the compilation failed. The compilation error details are located in the console output.

No further information about this warning or error available at this time.
Please contact the Pex developers  for further information.

Exit Code Success


Exit code returned on a successful execution.

  • Value: 0

See Also

corerror.h in the .Net framework SDK.

Exit Code ControlC


Exit code returned when the process exited when the Control+C key was pressed.

  • Value: 0xC000013A

See Also

corerror.h in the .Net framework SDK.

Exit Code FataExecutionEngineError1


Exit code returned when the CLR process fails critically.

  • Value: 0x80131506

See Also

corerror.h in the .Net framework SDK.

Exit Code FataExecutionEngineError2


Exit code returned when the CLR process fails critically.

  • Value: 0x800703E9

See Also

corerror.h in the .Net framework SDK.

Exit Code ClrMonitor


Exit code returned when an unhandled exception was not caught by the process.

  • Value: 0xE0434F4D

See Also

corerror.h in the .Net framework SDK.

Exit Code SafeDebugFail


Exit code returned when a Debug assertion or an assumption was raised in the Pex infrastructure.

  • Value: -666
  • Bug: please report this failure.

See Also

corerror.h in the .Net framework SDK.

Exit Code ClrMonitor


Exit code returned when the ExtendedReflection profiler encountered a fatal error.

  • Value: -667
  • Bug: please report this failure.

See Also

corerror.h in the .Net framework SDK.

Exit Code Unknown action


TODO

  • Value: -1

See Also

corerror.h in the .Net framework SDK.

Exit Code UserAbort


Exit code returned when the execution was stopped from a user abort message.

  • Value: -999

Exit Code DefaultFailure


Exit code returned when the execution failed in a 'reasonable' way.

  • Value: -1000

Exit Code UnknownIntPtrSize


Exit code returned when the process is neither a 32-bit or 64bit process.

  • Value: -1001

Exit Code OptionsParsingError


Exit code returned when an error was found in the options passed to the Pex command line tool.

  • Value: -667
  • Diagnose: inspect the console output, which contains the error details.

Exit Code ErrorInSandbox


An error was encountered while setting the security sandbox AppDomain up.

  • Value: -1004

Exit Code NoChannelSet


The instrumented process was instructed to listen to a serialization channel, but that channel name was not set.

  • Value: -1005

Exit Code AssemblyLoadError


Exit code returned when the CLR failed to load an assembly.

  • Value: -1006

Diagnostics

  • Delay Signed Assemblies: if you use delay signed assemblies, make sure you have correctly set up the strong name validation so that the CLR allows to load the assembly.

Exit Code PlatformMismatch


Exit code returned when an assembly of a specific platform (32bit/64bit) was to be loaded in a process with incompatible bitness.

  • Value: -1007

Exit Code UnexpectedToolError


Exit code returned when an unexpected exception occured while execution Pex.

  • Value: -1008
  • Bug: please report this bug.

Exit Code UnexpectedLaunchError


Exit code returned when an unexpected exception occured while preparing the instrumented process.

  • Value: -1009
  • Bug: please report this failure.

Exit Code ReflectionError


Exit code returned when an unrecoverable exception occured when reflecting the tests.

  • Value: -1010

Common Mistakes

  • Pex might return this exit code when it could not find any test to execute.

Exit Code NoExplorationFound


This error occurs when Pex could not find an appropriate method to explore.

Common reasons for this error are:
  • The intended target method is not visible.
  • The intended target method is not defined in a visible class.
  • The intended target method is defined in an abstract class.

If you are running Pex on a method in a test project, please make sure that the target method has the attribute PexMethod, and that it is defined in a PexClass.

  • Value: -1013

Exit Code InstrumentionDriverConfigurationError


Exit Code that occurs when Microsoft.Pex.exe was called without properly setting the process environment variables. Microsoft.Pex.exe is an internal driver that should not be called directly. Use pex.exe to launch Pex from the command line.

Exit Code ExternalProfilerRegistered


Exit code returned when Pex detected that another profiler was already registered.

  • Value: -1015


Remarks

The default behavior of Pex is to override any other profiler when starting the instrumented process. This behavior can be overriden through the ProfilerInterfaction command line option.

Exit Code X86MonitoringNotEnabled


Exit code returned when Pex detected that the CLR profiler for X86 code was not properly attached to the instrumented process.

There is most likely a problem with the Pex installation. Please uninstall and reinstall Pex.

  • Value: -1016

Exit Code X64MonitoringNotEnabled


Exit code returned when Pex detected that the CLR profiler for X64 code was not properly attached to the instrumented process.

  • Value: -1017

Exit Code RemotingInitializationError


This exit code is returned when Pex could not initialize remoting.

This is often a transient condition; please try to run Pex again.

  • Value: -1018

Exit Code VsBuildFailed


Pseudo exit code when the build failed before launching the Pex process in Visual Studio.

  • Value: -2000

Wix


Windows Installer Xml, tool used to build Windows Installer files.

This sample comes with Pex.

This tutorial shows how to
  • test an algorithm with parameterized unit testing,
  • write tests whose parameters are primitive types,
  • configure the values Pex should consider for the parameters.

When given code with a complicated control-flow structure, then Pex can infer the input values which will cause all possible execution paths to be taken.

Consider for example the triangle-classification method, which takes three integers, representing the lengths of the sides of a triangle.

public static TriangleKind Classify(int s1, int s2, int s3)
{
    if ((s1 == s2) && (s2 == s3) && (s1 == s3))
        return TriangleKind.Equilateral;
 
    if ((s1 + s2 <= s3) || (s1 + s3 <= s2) || (s2 + s3 <= s1))
        return TriangleKind.Invalid;
 
    if ((s1 == s2) || (s2 == s3) || (s1 == s3))
        return TriangleKind.Isosceles;
 
    if ((s1 != s2) && (s2 != s3) && (s1 != s3) && (s1 + s2 > s3) && (s1 + s3 > s2) && (s2 + s3 > s1))
        return TriangleKind.Scalene;
 
        return TriangleKind.Invalid;
}

We can write a simple parameterized unit test which simply passes its parameters through to the code which are interested in exploring.

[TestClass, PexClass]
public partial class TriangleTest 
{
    [PexMethod]
    public void TestTriangle(int s1, int s2, int s3) 
        Triangle.Classify(s1, s2, s3);
    }
}

If the Triangle class is located in a different assembly than the test code, then you need to instruct Pex to instrument the implementation code, e.g. with the following assembly-level attribute:
[assembly: PexInstrumentType(typeof(Triangle))]

If we are not interested in testing the classification method for negative or zero lengths, we can state this assumption as the first line of the test:
PexAssume.IsTrue(s1 > 0 & s2 > 0 & s3 > 0);

When Pex explores this parameterized unit test, it will check it can throw any exceptions. You could add additional verification using the PexAssert class.

See Also

PexClassAttribute, PexMethodAttribute, PexAssume, PexAssert

QuickSort


This sample comes with Pex.

This tutorial shows how to
  • test an algorithm with parameterized unit testing,
  • write tests whose parameters are primitive types or arrays over primitive types,
  • configure the values Pex should consider for the parameters.

A common operation performed on arrays is sorting. There are different algorithms to implement array sorting, but they all have to follow a common specification.

Suppose the signature of an algorithm which sorts arrays is the following.

public static class QuickSort
{
     public static void Sort(int[] szArray, int nLower, int nUpper);
}

  • nLower and nUpper are the inclusive bounds of the area of the array which we want to sort.

We can specify that the result of sorting an entire array should be an ordered list as follows. Note that we assume that we are given a non-null array.

[PexMethod]
public void TestQuickSort([PexAssumeNotNull] int[] a)
{
     QuickSort.Sort(a, 0, a.Length - 1);
     for (int i = 0; i < a.Length - 1; i++)
          PexAssert.IsTrue(a[i] <= a[i + 1]);
}

When we let Pex explore this test, it generates many different cases. In fact, it doesn't seem to finish. The reason is that the search space is huge. For every array length n, there are n! (n factorial) many execution paths through quicksort.

You can limit the time Pex spends in many ways, e.g. by limiting the number of times Pex may execute the test.

[PexMethod(MaxRuns=50)]

The generated inputs give us 100% code coverage.

See Also

PexMethodAttribute, PexAssumeNotNullAttribute
This sample comes with Pex.

This tutorial shows how to
  • model language grammars in C#,
  • write invariants over C# data-types,
  • test an algorithm whose input is a sentence of a grammar.

Let us assume that we want to test an evaluator of a small expression language. Here is its grammar (where IDENT and NUMBER are terminals and other terminals are enclosed in quotes) : 

Expr ::= IDENT
     |   NUMBER
     |   "let" Ident = Expr "in" Expr
     |  Expr + Expr
     |  Expr - Expr

Legal expressions are for example: 

1
a
1+a
2 - 4 + b
let x = 1 in 1 + x

Naively we could generate these expressions by just enumerating the strings from the grammar.

However languages are typically not context free, but have context conditions. In our example we might want that all expressions are closed. This means that every identifier that is applied must be defined. If we would add context conditions to our example then the first and last expression would be context correct while the other one contain context errors.

Context conditions are best described as attribute grammars or in more general terms as predicates over the abstract syntax of a language.

So when we use Pex for language testing, we don't start with describing the concrete grammar and then end up with hundreds of illegal programs but we do the following:

First, we define the abstract syntax of the language to test as C# classes. Then Pex can generate programs as instances of these classes. We write ToString() for the C# classes to pretty print the data in terms of the concrete syntax. This way we can represent the generated trees as normal strings. We give the context conditions as predicates. This is often called the language static semantics. We can also define the interpreter that gives context correct programs a meaning. This is often called dynamic semantics.

We can configure many aspects of Pex to guide the search.

The rest of this tutorial goes thru these steps in detail.

Tiny Language


The abstract syntax of a language is a data type that represents the essential parts of the derivation tree of the concrete syntax, for instance it strips out lexical information unless necessary. In our case we strip out the terminals "let" and "in". The terminals IDENT and NUMBER carry meaning. We model this as follows in C#.

    public enum Operator { Add, Sub }
    abstract public partial class Expression {}
    public partial class Constant : Expression {
        public int Value;
    }
    public partial class Binary : Expression {
        public Operator Operator;
        public Expression Left;
        public Expression Right;
    }
    public partial class Let : Expression {
        public string Name;
        public Expression Definition;
        public Expression Body;
    }
    public partial class Var : Expression {
        public string Name;
    }

The following functions pretty print expressions of the abstract syntax in the concrete syntax. We use them later to print the generated test cases.

    public partial class Constant : Expression {
        public override string ToString() {
            return this.Value.ToString();
        }
    }
    public partial class Binary : Expression {
        public override string ToString() {
            return string.Format("({0}{1}{2})", 
                                 this.Left, 
                                 this.Operator == Operator.Add ? "+" : "-", 
                                 this.Right);
        }
    }
    public partial class Let : Expression {
        public override string ToString() {
            return string.Format("(let {0}={1} in {2})", this.Name, this.Definition, this.Body);
        }
    }
    public partial class Var : Expression {
        public override string ToString() {
            return string.Format("{0}", this.Name);
        }
    }

We have to make sure that a our expressions should be acyclic, and do not contain null references. This is checked by IsWellformed.

    abstract public partial class Expression
    {
        public static bool IsWellformed(Expression e)
        {
            return IsWellformed(new Dictionary<Expression, bool>(), e);
        }
        public static bool IsWellformed(Dictionary<Expression, bool> visited, Expression e)
        {
            if (e == null) return false;
            if (visited.ContainsKey(e)) return false; // cycle
            visited.Add(e, true);
            bool res = e.GetInternalIsWellformed(visited);
            visited.Remove(e);
            return res;
        }
        public static bool IsWellformed(string s)
        {
            return !String.IsNullOrEmpty(s);
        }
        protected abstract bool GetInternalIsWellformed(Dictionary<Expression, bool> visited);
    }
 
    public partial class Constant : Expression
    {
        protected override bool GetInternalIsWellformed(Dictionary<Expression, bool> visited)
        {
            return true;
        }
    }
    public partial class Binary : Expression
    {
        protected override bool GetInternalIsWellformed(Dictionary<Expression, bool> visited)
        {
            return
              (this.Operator == Operator.Add | this.Operator == Operator.Sub) && 
              IsWellformed(visited, this.Left) &&
              IsWellformed(visited, this.Right);
        }
    }
    public partial class Let : Expression
    {
        protected override bool GetInternalIsWellformed(Dictionary<Expression, bool> visited)
        {
            return
                IsWellformed(this.Name) &
                IsWellformed(visited, this.Definition) &&
                IsWellformed(visited, this.Body);
        }
    }
    public partial class Var : Expression
    {
        protected override bool GetInternalIsWellformed(Dictionary<Expression, bool> visited)
        {
            return IsWellformed(this.Name);
        }
    }

The static semantics of TL is simple: TL programs must be closed, i.e. are not allowed to have free variables. This is checked by the function Closed. 

 abstract public partial class Expression {
        public static bool IsClosed(Expression e) {
            return e.GetInternalIsClosed(new Dictionary<string, bool>());
        }
        protected internal abstract bool GetInternalIsClosed(Dictionary<string, bool> names);
    }
 
    public partial class Constant : Expression {
        protected internal override bool GetInternalIsClosed(Dictionary<string, bool> names) {
            return true;
        }
    }
    public partial class Binary : Expression {
        protected internal override bool GetInternalIsClosed(Dictionary<string, bool> names) {
            // Closed(Left) and Closed(Right)
            return this.Left.GetInternalIsClosed(names) & this.Right.GetInternalIsClosed(names);
        }
    }
    public partial class Let : Expression {
        protected internal override bool GetInternalIsClosed(Dictionary<string, bool> names) {
            // Closed(Definition, names) and Closed(Body, names + {Name})
            if (!this.Definition.GetInternalIsClosed(names)) return false;
            bool contained = names.ContainsKey(this.Name);
            if (!contained)
                names.Add(this.Name, true);
            bool res = this.Definition.GetInternalIsClosed(names);
            if (!contained)
                names.Remove(this.Name);
            return res;
        }
    }
    public partial class Var : Expression {
        protected internal override bool GetInternalIsClosed(Dictionary<string, bool> names) {
            return names.ContainsKey(this.Name);
        }
    }

The dynamic semantics for TL, its meaning, is described by the function Eval.

Configuring Pex


Although our tiny language doesn't provide much, it allows generating infinitely many programs. And even if we would only allow context free programs, there would still be infinitely many. In order to control and terminate the generation process, the user has to provide bounds on the data types representing programs.

You must specify which (sub)types Pex may use, and within which bounds Pex should explore the program.
Please look at the source of the TinyLanguageTest class of sample project for a possible configuration.
This sample comes with Pex.

Please read the exercise on Creating complex objects, and Invariants in the Tutorial for more information.
to be deleted
Writing Secure Code, Second Edition, Chapter 10
http://www.microsoft.com/mspress/books/sampchap/5957.aspx 

PexAssertFailedException


Exception thrown by PexAssert.

MaxConstraintSolverTime - Seconds the constraint solver has to figure out inputs that will cause a new different execution path to be taken


This is an option of the PexSettingsAttributeBase and its derived types.

The deeper Pex explores the execution paths of a program, the more complex the constraint systems become that Pex builds from the control-flow and data-flow of the program. Depending on how limited your time is, you can set this value to let Pex think more or less about new execution paths.

Most often, the reason for a time-out is that Pex is trying to find a solution of a constraint system that does not have a solution, but Pex is not aware of this fact. Since this is the most common case for a time out, it may not make sense to increase the bound.

MaxConstraintSolverMemory - Megabytes the constraint solver has to figure out inputs that will cause a new different execution path to be taken


This is an option of the PexSettingsAttributeBase and its derived types.

The deeper Pex explores the execution paths of a program, the more complex the constraint systems become that Pex builds from the control-flow and data-flow of the program. Depending on the available memory of your machine, you can set this value to let Pex tackle more complicated constraint systems.

Most often, the reason for exceeding the available memory during constraint solving is that Pex is trying to find a solution of a constraint system that does not have a solution, but Pex is not aware of this fact. Since this is the most common case for an out-of-memory situation in the constraint solver, it may not make sense to increase the bound.

MaxBranches - Maximum number of branches that may be taken along a single execution path


This is an option of the PexSettingsAttributeBase and its derived types.

The motivation behind this exploration bound is to limit the length of any execution path that Pex explores during Input Generation. In particular, it prevents Pex from getting stuck when the program goes into an infinite loop.

Each conditional and unconditional branch of the executed and monitored code is counted towards this limit,
including branches which do not depend on the inputs of the parameterized test.

For example, the following code consumes branches in the order of 100:
for (int i=0; i<100; i++) { }

MaxCalls - Maximum number of calls that may be taken during a single execution path


This is an option of the PexSettingsAttributeBase and its derived types.

The motivation behind this exploration bound is to limit the length of any execution path that Pex explores during Input Generation. In particular, it prevents Pex from getting stuck when the program calls a method recursively an infinite number of times, which would cause a stack overflow that Pex cannot recover from.

Each call (direct, indirect, virtual, jump) of the executed and monitored code is counted towards this limit.

MaxStack - Maximum size of the stack at any time during a single execution path, measured in number of active call frames


This is an option of the PexSettingsAttributeBase and its derived types.

The motivation behind this exploration bound is to limit the size of the stack of any execution path that Pex explores during Input Generation. In particular, it prevents Pex from using all available stack space, which would cause a stack overflow that Pex cannot recover from.

MaxConditions - Maximum number of conditions over the inputs that may be checked during a single execution path


This is an option of the PexSettingsAttributeBase and its derived types.

The motivation behind this exploration bound is to limit the complexity of any execution path that Pex explores during Input Generation.

Each conditional branch which depends on the inputs of the parameterized test is counted towards this limit.

For example, each path in the following code consumes n+1 conditions:
[PexMethod]
void ParameterizedTest(int n) 
{
     for (int i=0; i<n; i++) { // conditions are "0<n", "1<n", ..., "!(n<n)"
          ...
     }
     for (int i=0; i<100; i++) { // irrelevant for MaxConditions, since conditions do not depend on input
          ...
     }
}

See Also

PexMethodAttribute

MaxRuns - Maximum number of runs that Pex will try during the exploration of a test


This is an option of the PexSettingsAttributeBase and its derived types.

The motivation behind this exploration bound is that any code which contains loops or recursion might have an infinite number of execution paths, and thus Pex needs to be limited during Input Generation.

The two settings MaxRuns, MaxRunsWithUniquePaths are related as follows.

Pex will call a parameterized test method up to MaxRuns times with different test inputs. If the executed code is deterministic, then it will take a different execution path each time. However, under some conditions the executed code might take an execution path it has taken already before with different inputs. Pex counts how many unique execution paths it finds; this number is limited by the MaxRunsWithUniquePaths option.

MaxRunsWithoutNewTests - Maximum number of consecutive runs without a new test being emitted


This is an option of the PexSettingsAttributeBase and its derived types.

While Pex can often find many interesting test inputs within a short time, after a while Pex will not find any more new test inputs, and Pex will emit no more unit tests. This configuration option puts a bound on the number of attempts that Pex may perform in a row without emitting a new test before Pex will stop the exploration.

Also see: MaxRuns, MaxRunsWithUniquePaths.

MaxRunsWithUniquePaths - Maximum number of unique paths that Pex will consider during an exploration


This is an option of the PexSettingsAttributeBase and its derived types.

The motivation behind this exploration bound is that any code which contains loops or recursion might have an infinite number of execution paths, and thus Pex needs to be limited during Input Generation.

The two settings MaxRuns, MaxRunsWithUniquePaths are related as follows.

Pex will call a parameterized test method up to MaxRuns times with different test inputs. If the executed code is deterministic, then it will take a different execution path each time. However, under some conditions the executed code might take an execution path it has taken already before with different inputs. Pex counts how many unique execution paths it finds; this number is limited by the MaxRunsWithUniquePaths option.

MaxExceptions - Maximum number of exceptions that will be explored until exploration is stopped


This is an option of the PexSettingsAttributeBase and its derived types.

The motivation behind this exploration bound is to stop the exploration of code that is too buggy: If Pex finds too many errors in the code, exploration is stopped.

TestEmissionBranchHits


Depending on the current TestEmissionFilter setting, Pex emits new test cases when they cover a branch in the program that was not covered before.

The TestEmissionBranchHits setting controls whether Pex should just consider whether a branch was covered at all (TestEmissionBranchHits=1), or whether a test covered it either once or twice (TestEmissionBranchHits=2), and so on.

TestEmissionBranchHits=1 will give a very small test suite that will cover all branches Pex could reach. (In particular, this test suite will also cover all reached basic blocks and statements.)
The default for this option is TestEmissionBranchHits=2, which generates a more expressive test suite that is also better suited to detect future regression errors.

See Also

PexMethodAttribute
Pex understands all safe, and many unsafe instruction as specified in the ECMA-335 standard. Pex will try to generate test inputs which cover all the corner cases of the instruction set.

{url:http://www.ecma-international.org/publications/standards/Ecma-335.htm}

IPexClassFactory<>


Interface which is implemented by a factory point to by the PexCreatableByClassFactoryAttribute.

Assembly


An assembly is a reusable, versionable, and self-describing building block of a common language runtime application.
The PexDomainAttributeBase and its derivatives can be used to define the domains of types, fields, and parameters for which Pex tries to find values. In addition to regular classes with regular fields, .Net has a number of built-in types which properties similar to fields. Pex' input generation treats them just as all other fields. The PexSpecialFieldNames contains a set of name constants and name getter methods for those special fields.

PexDecoratorAttributeBase


Abstract base attribute class for Pex Decoration Attribute.

InstrumentationLevel


Property of PexInstrumentTypeAttributeBase and PexInstrumentAssemblyAttributeBase that defines the scope of code instrumentation.

Possible values:
  • PexInstrumentationLevel.Excluded
  • PexInstrumentationLevel.Included -- Default

See Also

PexInstrumentTypeAttributeBase, PexInstrumentAssemblyAttributeBase

ITestFramework


Interface that characterizes a test framework.
Please contact mailto:pexdev@microsoft.com  to get information on how to integrate a custom test framework into Pex.

Abstract Attribute Pattern


The Abstract Attribute Pattern is a design that enables extensibility through attributes:

it is allowed to query for abstract attributes in the .Net, Reflection will return all attribute instances that are assignable to the requested abstract custom attribute. Therefore, by leaving the attribute abstract, it provides a nice and extension mechanism.

Example

  • the attribute base class
abstract class FooAttributeBase : Attribute
{
    abstract void DoSomething();
}

  • a sample attribute:
class MyFooAttribute : FooAttributeBase
{
    override void DoSomething() { Console.WriteLine("hello"); }
}
...
[MyFoo]
class Bar {}

  • querying the abstract attribute
foreach(FooAttributeBase attribute in 
    Attribute.GetAttributes(typeof(FooAttributeBase), typeof(Bar)))
{ Console.WriteLine(attribute); }
 
-- output
MyFooAttribute

PexAssumeFailedExceptionAttribute


Attribute used to register an exception type as an assumption.

[assembly: PexAssumeFailedException(typeof(MyException))]

Suggested Fix


Sometimes, when Pex finds a failing test case, Pex can provide a code snippet that, when inserted into the source code, will prevent the same failure from happening again. Pex uses a clever search for the root cause of the failure.

When Pex can determine a potential fix, the generated report contains an option to view it.
FixIt0.PNG

Pex might offer more than one way to fix the problem. If the failure cause was due to an inconsistent state of the object, it may offer to add a check which will throw an System.InvalidOperationException.
FixIt2.PNG

And even better, Pex will try to trace back the inconsistent program state to a parameter of a public method, and if it can, it will offer to add additional parameter validation code at the correct site.
FixIt1.PNG

Each fix is associated with a rank. The higher the rank, the closer the fix should represent the actual root cause.

The potential fix was derived the abstract knowledge Pex obtained from observing the program's execution, and it might not be executable code as is.

Kind and location


Pex will use different APIs to generate the fixes depending on the type of fix and the code location:

  • invariants, uses System.Diagnostic.Debug:
Debug.Assert(this.foo > 0);
  • assumptions in private methods, uses System.Diagnostic.Debug,
private void PrivateMethod(string s)
{
    Debug.Assert(s != null);
    ...
}
  • assumptions in public methods, throws System.ArgumentException,
public void PublicMethod(string s)
{
    if (s == null)
        throw new ArgumentNullException(s);
    ...
}
  • assumptions in test methods, uses PexAssume,
[Test]
public void SomeTest(string s)
{
    PexAssume.IsNotNull(s);
}

Support for Code Contracts


Pex will detect an assembly that has been rewritten for Code Contracts and automatically emit fixes
using the contracts API.

Extensibility


A custom emitter can be provided to change how fixes are emitted. For example, to use a custom assertion or assumption class.
A metadata entity.
A metadata entity.
A metadata entity.

A type definition represents a TypeDef token in a module.
A metadata entity.
A metadata entity.

A method definition represents a MethodDef token in a module. (With the exception of certain methods of multi-dimensional arrays which can be referenced but do not have MethodDef tokens; however, they do have method definitions in the Extended Reflection framework.)
A metadata entity.
A metadata entity.

A field definition represents a FieldDef token in a module.
Arrays in .Net fall into two categories:
  • zero-based, single-dimensional arrays (sz-arrays)
  • non-zero-based or multi-dimensional arrays (md-arrays or just multi-dimensional arrays)

GAC (Global Assembly Cache)


"Each computer where the common language runtime is installed has a machine-wide code cache called the global assembly cache. The global assembly cache stores assemblies specifically designated to be shared by several applications on the computer."

http://msdn2.microsoft.com/en-us/library/yf1d93sz(VS.80).aspx 

Missing Precondition


When Pex finds that a test run fails, it may suggest changing the code by adding a precondition to a method. Then, when running the test again, it would fail at a different, earlier point. Furthermore, when the test is annotated with PexAllowedException(typeof(ArgumentException)), Pex will deal nicely with then correctly specified precondition violations.

A suggested precondition is always of the form

  if (!c) throw new ArgumentException(...);

or

  if (c==null) throw new ArgumentNullException(...);

Missing Invariant


When Pex finds that a test run fails, it may suggest to change the code by adding a check for a class invariant to a method. Then, when running the test again, it would fail at a different, earlier point. When you also use Pex' special features to check class invariants at all public method call sites, you get additional checking for all future test runs.

A suggested invariant is always of the form
  if (!c) throw new InvalidOperationException(...);

How To Report a Pex Bug


If you have access to the Microsoft Corporate network,
you can access our issue tracker directly, see here.

Otherwise, please send an email with one or more for the following information to mailto:pexbug@microsoft.com .

  • A stacktrace
    • Look around in the output windows in Visual Studio. If you can find a stacktrace after you encountered this error, please send it to us.
  • Information on how to reproduce the error
    • The code snippet (up to ten lines of code) of the test case that causes this error, and
    • Tell us where you got the libraries from that your project references.
    • Send an email to pexbug@microsoft.com.
  • A Pex Report
    • If you can reproduce the bug, and the Pex team cannot diagnose the problem with the above information, you can create a Pex Report for us.
    • In Visual Studio, go to Tools – Options, select Pex – General on the left.
      • Set the option “Reports” to “true”.
    • Select Pex – Diagnostics on the left.
      • Set “Diagnostics” to “true”.
    • Press “OK”.
    • Close Visual Studio, start Visual Studio again. Load your project.
    • Run Pex.
    • When Pex is done, a report should have been created.
      • In the Pex Exploration Results window, select Views – Open Report.
      • Look at the address of the opened report.
      • Verify that the report does not contain confidential information.
      • Create a zip file holding that entire directory.
    • Send the zipped report to us.
•* You probably want to turn off Reports and Diagnostics afterwards when you keep using Pex, as these two features make Pex considerably slower.

TestProject


Assembly setting used to specify the file name of the test project. Having the target test project, Pex can deduce the output language, root namespace and update the project file with the generated test files.

Code Contracts


Code Contracts is a .Net 4.0 API that let the user write pre-condition, post-condition and object invariant. Please refer to the code contract documentation for further information.

(c) Microsoft Corporation. All rights reserved. pex Wiki Documentation 0.16.40915.5