Pex and Code Contracts

I’m currently experimenting with Pex, Moles and Code Contracts, and I wondered what effect code contracts have on Pex tests. So I build this simple piece of code:

   1: public class Demo
   2: {
   3:   public int Foo(int a, int b)
   4:   {
   5:     if (a < 0)
   6:       return a;
   7:     else if (a > 0)
   8:       return b;
   9:     else
  10:       return a + b;
  11:   }
  12: }

Then I make Pex generate its Parameterized Unit Tests (PUTs). This generates the following test:

   1: [PexClass(typeof(Demo))]
   2: [PexAllowedExceptionFromTypeUnderTest(typeof(InvalidOperationException))]
   3: [PexAllowedExceptionFromTypeUnderTest(typeof(ArgumentException), AcceptExceptionSubtypes = true)]
   4: [TestClass]
   5: public partial class DemoTests
   6: {
   7:     /// <summary>Test stub for Foo(Int32, Int32)</summary>
   8:     [PexMethod]
   9:     public int Foo(
  10:         [PexAssumeUnderTest]Demo target,
  11:         int a,
  12:         int b
  13:     )
  14:     {
  15:         int result = target.Foo(a, b);
  16:         return result;
  17:         // TODO: add assertions to method DemoTests.Foo(Demo, Int32, Int32)
  18:     }
  19: }

I just leave the code, right-click on The Foo method of the DemoTests class, choose “Run Pex explorations” and I get this:

image

As you can see the exploration calls my code with negative, zero and positive values. What happens when I add a contract stating that a should be positive?

   1: public class Demo
   2: {
   3:   public int Foo(int a, int b)
   4:   {
   5:     Contract.Requires(a > 0);
   6:     if (a < 0)
   7:       return a;
   8:     else if (a > 0)
   9:       return b;
  10:     else
  11:       return a + b;
  12:   }
  13: }

Only line 5 was added, but if I run the pex explorations again I get:

image 

The effect is that Pex now doesn’t explore negative numbers, because it can deduce from the contract not to even try.

What if I use a contract to state that b should be negative?

   1: Contract.Requires(b < 0);

Again Pex sees this and explores my code with negative b:

image

One more. When I change my code to do a little more with b, like this:

   1: public int Foo(int a, int b)
   2: {
   3:   Contract.Requires(a > 0);
   4:   Contract.Requires(b < 0 || b > 10);
   5:   if (a < 0)
   6:     return a;
   7:   else if (a > 0)
   8:   {
   9:     if (b > a)
  10:       return a;
  11:     else
  12:       return b;
  13:   }
  14:   else
  15:     return a + b;
  16: }

and when I run the explorations again:

image

So, you can guide Pex by supplying contracts on the arguments of your methods.