In the previous post, we clarified what Pex was not doing. So what does it do?

Pex performs some kind of automated exploration testing. I'll dive deeper into the details of this, but let's start with an example that gives the high level idea of the methodology.

Exploration Testing

Let's start by doing some exploration testing on a simple method that checks that an integer is positive, CheckPositive:

1 void CheckPositive(int i, bool @throw) {
2     if (i < 0) {      
3          Console.WriteLine("not ok");
4          if (@throw)
5             throw new ArgumentException();
6     }
7     else
8         Console.WriteLine("ok");
9 }

One way to 'explore' this method would be to throw different values at CheckPositive and use the debugger to see what's happening.

Iteration 1: pick the default

Let's create a unit test that does exactly that and step into the debugger. Since we don't really know anything about CheckPositive yet, we simply pick 0 for i (actually default(int)).

[TestMethod]
void Zero() {
     CheckPositive(0, false);
}

When we reach the statement "Console.WriteLine..." on line 8, we can figure out that we took this branch because the condition "i < 0" on line 2 evaluated to false. Let's remember this and continue on.
          line 2, i < 0 == false, uncovered branch

The execution continues and the test finished successfully.

Iteration 2: flip the last condition

In the previous run, we've remembered that some code was not covered on line 3. We also know that this code path was not covered because the condition "i < 0" evaluated to false. At this point, we usually intuitively figure out a value of 'i' in our brain, to make this condition true. In this case, we need to solve "find i such that i < 0". Let's pick -1.

[TestMethod]
void MinusOne() {
     CheckPositive(-1, false);
}

We run the test under the debugger. As expected on line 2, the condition evaluates to true, and the program takes the other branch that in the previous test.
The program continues and reaches line 4 where another if statement branch. Since the condition  "@throw" evaluates to false, we take the branch that throws and remember the condition:
          line 4, @throw == false, uncovered branch

The program continues to run and finishes.

Iteration 3: path condition + flipped condition

We've still some uncovered branch to cover in the method, 'guarded' by the condition at line 4. To be able to cover this code, we need 2 things:
      1) reach line 4: i < 0
      2) make the condition in line 4 evaluate to true: @throw == true

So to cover the last statement in the method, we need to find parameter values such that
                  i < 0 && @throw == true

Let's pick -1, and true.

[TestMethod]
void MinusOneAndThrow() {
     CheckPositive(-1, true);
}

The test executes and now throws an exception as we wanted. At this point, we've fully covered to behavior of CheckPositive.

What about Pex?

Pex uses the same 'exploration' methodology as above. Pex executes a parameterized unit tests over and over and tries to cover each branch of the program. As it executes more code, it learns about new branches to cover etc... To find the input, Pex uses a constraint solver, Z3.