# Thursday, July 31, 2008

Alexander Nowak has started a blog post chronicle on Pex and already has 6 episodes to it!

  • Pex - test Case 5 (regular expressions)
  • Pex - test case 4 (strings and parameter validation)
  • Pex - Test case 3 (enums and business rules validation)
  • Pex - test case 2 
  • Pex - test case 1
  • Starting with Pex (Program Exploration)

    The posts give a nice point of view of Pex from a user perspective, and against classic testing techniques such as equivalence classes.

  • posted on Thursday, July 31, 2008 7:25:49 AM (Pacific Daylight Time, UTC-07:00)  #    Comments [0]
    # Tuesday, July 29, 2008

    Linear programming problems are usually solved using the simplex algorithm. While it is easy to encode a constraint system of linear equalities and inequalities as a Parameterized Unit Test for Pex, there is currently no way to tell Pex that we want test inputs that are “minimal” according to a custom objective function. However, Pex can still generate *surprising* feasible solutions.

    Let's start with a simple set of linear inequalities that define our problem.

    [PexMethod]
    public int Test(int x, int y)
    {
    // PexAssume is used to add 'constraints' on the input
    // in this case, we simply encode the inequalities in a boolean formula PexAssume.IsTrue( x + y < 10 & // using bitwise & to avoid introducing branches 5 * x + 2 * y > 20 & -x + 2 * y > 0 & x > 0 & y > 0);
    // the profit is returned so that it is automatically logged by Pex return x + 4 * y; }

    After running Pex, we get one feasible solution. It is not optimal as expected since we don't apply the simplex algorithm.

    image

    Enter overflows

    Remember that .Net arithmetic operations will silently overflow unless you execute them in a checked context? Let's push our luck and try to force an overflow by changing x > 0 constraint to x > 1000:

    [PexMethod]
    public int Test(int x, int y)
    {
        PexAssume.IsTrue(
            x + y < 10 &
            5 * x + 2 * y > 20 &
            -x + 2 * y > 0 &
            x > 1000 & y > 0
        );
        return x + 4 * y;
    }

    Z3, the constraint solver that Pex uses to compute new test inputs, uses bitvector arithmetic to find a surprising solution that fulfills all the inequalities (our profit has just gone of the roof :)).

    image 

    Z3 is truly an astonishing tool!

    Checked context

    In order to avoid overflow, one should use a checked context. Let's update the parameterized unit test:

    [PexMethod]
    public int Test(int x, int y)
    {
        checked
        {
            PexAssume.IsTrue(
                x + y < 10 &
                5 * x + 2 * y > 20 &
                -x + 2 * y > 0 &
                x > 0 & y > 0
            );
        }
        return x + 4 * y;
    }

    In fact, in that case, Pex generates 2 test cases. One test that passes and the other test that triggers an OverflowException (implicit branch).

    image

    Stay tuned for more surprising discoveries using Pex.

    posted on Tuesday, July 29, 2008 6:35:31 PM (Pacific Daylight Time, UTC-07:00)  #    Comments [2]
    # Thursday, July 03, 2008

    Brian Keller dropped by our offices to record a movie on Pex. A good old white board session to explain how pex works:

    http://channel9.msdn.com/posts/briankel/Pex-Automated-Exploratory-Testing-for-NET/

     

    posted on Thursday, July 03, 2008 11:21:54 AM (Pacific Daylight Time, UTC-07:00)  #    Comments [0]