In a previous post we started using Microsoft Pex and showed how it helped exploring all possible code paths, and how that helped discovering a defect in our program logic. In that example, even our program logic is defective, all test cases succeeded. A test case fails if there is an un-caught exception or a failed assertion.
To see an example of a failed test case and how Pex could help in fixing it, let’s add the following basic function to our code:
public void Add(ArrayList a, object o)
{
a.Add(o);
}
when you run Pex for that simple method, you get the following results:
As you might expected, the ArrayList object might be NULL. In situations similar to this one, when a higher-level component (the code that called Add() method) passes malformed data to a lower-level component(that Add() method), which the lower-level component rejects, then the higher-level component should be prevented from doing so in the first place.
One way to achieve this is to promote the failure condition of the lower-level component to the abstraction level of the higher-level component. This is what the Add Precondition feature of Pex does: It expresses a low-level failure condition at the abstraction level of the code under test. When added to the code-under-test as argument validation code—also called a precondition—then this effectively prevents the code under test from causing a failure somewhere in its execution. In other words, the Add Precondition feature doesn’t completely fix an error, but it promotes the failure condition to a higher, more appropriate abstraction level.
To add a precondition to your code, click the failed test case row, then on the details section (right) click Add Precondition, as in picture below
Pex will open Preview and Apply updates dialog box to show you the proposed code modifications that Pex will do.
Review and Click Apply. The modified method will look like:
public void Add(ArrayList a, object o)
{
//
Debug.Assert(a != (ArrayList)null, "a");
//
a.Add(o);
}
When you run Pex for our method now, we will not find a failed test case.
The concept of assertions is well known in unit test frameworks. Pex understands the built-in Assert classes provided by each supported test framework. However, most frameworks do not provide a corresponding Assume class as Pex did. PexAssume is a class to express assumptions, i.e. a precondition. The methods of this class can be used to filter out undesirable test inputs. If you do not want to use an existing test framework, Pex also has the PexAssert class. Some functionalities can be achieved using attributes instead of PexAssume methods, like PexAssumeNotNullAttribute and PexAssumeUnderTestAttribute.
[PexMethod]
public void Test1(object o) //precondition: o should not be null
{
PexAssume.IsNotNull(o);
...
}
[PexMethod]
public void Test2([PexAssumeNotNull]object o) //precondition: o should not be null
{
...
}
When you write an assertion, Pex will not only passively detect assertion violations, but Pex will in fact actively try to compute test inputs that will cause the assertion to fail (just as an assertion might throw a PexAssertFailedException). Pes uses these exceptions internally to stop a test case when an assumption fails.
You can annotate the test—or the test class, or the test assembly—with one of the following attributes to indicate which exception types can or must be thrown by the test in order to be considered successful:
PexAllowedExceptionAttribute indicates that a test method, or any other method that it calls directly or indirectly, can throw a particular type of exception for some test inputs.
using System;
using Microsoft.Pex.Framework;
using Microsoft.Pex.Framework.Validation;
namespace ConsoleApplication3
{
class Stack
{
int[] _elements;
int _count;
public Stack(int capacity)
{
if (capacity < 0) throw new ArgumentOutOfRangeException();
_elements = new int[capacity];
_count = 0;
}
}
[PexClass]
public partial class StackTest
{
[PexMethod]
[PexAllowedException(typeof(ArgumentOutOfRangeException))]
public void CtorTest(int capacity) // will not fail
{
Stack s = new Stack(capacity); // may throw Argume
ntOutOfRangeException
}
}
}
PexAllowedExceptionFromTypeAttribute indicates that any method of a specified type can throw a particular type of exception for some test inputs.
using System;
using System.Collections;
using Microsoft.Pex.Framework;
using Microsoft.Pex.Framework.Validation;
namespace ConsoleApplication3
{
[PexClass]
public partial class ArrayListTest
{
[PexMethod]
[PexAllowedExceptionFromType(typeof(NullReferenceException), typeof(ArrayListTest))]
public void Add1(ArrayList a, object o) //will not fail
{
a.Add(o);
}
}
}
PexAllowedExceptionFromTypeUnderTestAttribute indicates that any method of the designated type under test can throw a particular type of exception for some test inputs.
PexAllowedExceptionFromAssemblyAttribute indicates that any method located in a specified assembly can throw a particular type of exception for some test inputs.
Pex supports different filters that decide when generated test inputs will be emitted as a test case. You can configure these filters with the TestEmissionFilter property that you can set for example in the PexMethod attribute. Possible values are the following:
Regarding increased branch coverage, the TestEmissionBranchHits property controls how a branch is covered. For example:
The default is TestEmissionBranchHits=2, which generates a more expressive test suite that is also better suited to detect future regression errors.
using System;
using Microsoft.Pex.Framework;
using Microsoft.Pex.Framework.Settings;
namespace ConsoleApplication3
{
[PexClass]
partial class TestEmission
{
int max(int x, int y)
{
if (x > y)
return x;
else
return y;
}
[PexMethod(TestEmissionFilter=Microsoft.Pex.Framework.Settings.PexTestEmissionFilter.All)]
public void MaxTest1(int a, int b, int c, int d) // 1 test case generated
{
int e = max(a, b);
PexObserve.ValueForViewing("max", e);
}
[PexMethod(TestEmissionFilter = Microsoft.Pex.Framework.Settings.PexTestEmissionFilter.Failures)]
public void MaxTest2(int a, int b, int c, int d) // No test cases generated
{
int e = max(a, b);
PexObserve.ValueForViewing("max", e);
}
}
}
If the code under test does not contain loops or unbounded recursion, Pex will typically stop quickly because there is only a (small) finite number of execution paths to analyze. However, most interesting programs contain loops and/or unbounded recursion. In such cases the number of execution paths is (practically) infinite, and it is in general undecidable whether a statement is reachable. In other words, Pex would take forever to analyze all execution paths of the program.
In order to make sure that Pex terminates after a reasonable amount of time, there are several exploration bounds. All bounds have predefined default values, which you can override to let Pex analyze more and longer execution paths. The bounds are parameters of the PexMethod, PexClass, and PexAssemblySettings attributes. There are different kinds of bounds:
Constraint Solving Bounds: apply to each attempt of Pex to determine whether an execution path is feasible or not. Pex might need several constraint solving attempts to compute the next test inputs.
Exploration Path Bounds: apply to each execution path that Pex executes and monitors. These bounds make sure that the program does not get stuck in an infinite loop, or recursive method.
Exploration Bounds apply to the exploration of each parameterized unit test.
The following example shows a parameterized test that involves a loop. The loop bound depends on the test inputs, and the exception can only be triggered if the loop is executed a certain number of times. Here, we used an explicit bound of 10 runs MaxRuns=10 to let Pex finish quickly. However, with this bound, Pex will most likely not be able to trigger the exception, as Pex will not unroll the loop sufficiently many times:
[PexMethod(MaxRuns = 10)]
public void TestWithLoop(int n)
{
var sum = 0;
for (int i = 0; i < n; i++)
sum++;
if (sum > 20) throw new Exception();
}
In the Pex Exploration Results you may see the Exception statement
reached, but you will see on the Pex tool bar that there is 1 boundry
reached.
If you click on it, you will see more details:
on the right, you could click Set MaxRuns=20 to increase the MaxRuns
boundry. You could do the same from the Pex tool bar
and also setting boundary to infinity. Both actions will open a dialog
to review and approve the code changes.
The following example shows another parameterized test that involves a loop, but this loop does not depend on the test inputs. Here, we used an explicit bound of 10 branches MaxBranches=10 to let Pex finish quickly. However, with this bound, Pex cannot even once execute the code from beginning to end, as executing the embedded loop will cause more than 10 branches to be executed.
[PexMethod(MaxBranches = 10)]
public void TestWithFixedLoop(int j)
{
var sum = 0;
for (int i = 0; i < 15; i++)
sum++;
if (j == 10) throw new Exception();
}
In those cases, where a particular run exceeded some path-specific bounds, we get a special row in the results. The Set MaxBranches= button on the results tool can be used to increase the bounds. If you increased the boundary to 20, you will get all you branched executed and the exception statement reached.
In this post we talked about how and when a test case fail, how to use precondition and assumptions to differentiate between failures from your unit code and failures from malformed input, how to allow specific exception to be raised from your tests without causing it to fail, how to control which test inputs should Pex use as a test case, and finally how to control the Pex stop criteria whether through bounding the constraint solver, or bounding the exploration paths, or bounding the exploration runs.
