# Saturday, December 22, 2007

Scott swinged by MSR a couple weeks ago to talk about Pex.

http://hanselminutes.com/default.aspx?showID=111

 

posted on Saturday, December 22, 2007 4:02:30 AM (Pacific Standard Time, UTC-08:00)  #    Comments [0]
# Thursday, December 06, 2007

Update: this talk has been cancelled.

I'll be giving a talk about Pex in Diegem on January 3.

http://msdnrss.thecoderblogs.com/2007/12/06/msdn-techtalk-dynamic-analysis-and-test-generation-for-net-with-pex/

posted on Thursday, December 06, 2007 8:33:33 AM (Pacific Standard Time, UTC-08:00)  #    Comments [0]
# Wednesday, December 05, 2007

In the previous post, we went through the exploration testing process to exercise a simple method, CheckPositive. In this post, we'll try the same exploration testing, but will let Pex do it.

// mehod under test
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 }
// hand-crafted unit tests
[TestMethod] void Zero() {
     CheckPositive(0, false);
}
[TestMethod] void MinusOne() {
     CheckPositive(-1, false);
}
[TestMethod] void MinusOneAndThrow() {
     CheckPositive(-1, true);
}

Exploration testing with Pex

To let Pex explore the CheckPositive, we write a little test wrapper around that method:

[TestClass, PexClass]
public partial class ExplorationTesting {
    [PexMethod]
    public void Test(int i, bool @throw) {
        CheckPositive(i, @throw);
    }

We also instrumented the original method with additional methods to track down the path conditions that Pex computes along the execution traces. Pex generates 3 pairs of values which are equivalent to what the test we manually created:

  • 0, false
  • int.MinValue, false
  • int.MinValue, true (throws)
posted on Wednesday, December 05, 2007 8:54:15 AM (Pacific Standard Time, UTC-08:00)  #    Comments [1]
# Tuesday, December 04, 2007

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.

posted on Tuesday, December 04, 2007 11:17:38 AM (Pacific Standard Time, UTC-08:00)  #    Comments [2]

Nikolai Tillmann published a paper on DySy, a tool that can infer likely invariants by monitoring the code that is running.

DySy is was built on top of the infrastructure that Pex uses to generate test cases. In fact, it is one of our sample application :)

posted on Tuesday, December 04, 2007 8:53:17 AM (Pacific Standard Time, UTC-08:00)  #    Comments [0]