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.

Overloading & Co/Contra-variance could break your code!

Co and contra-variance were introduced to VB.NET and C# to make working with certain classes more natural (“because it should work”). But beware, I was experimenting a bit with this and found following possible breaking change. I started with these two classes:

C#

   1: public class Person
   2: {
   3:   // ...
   4: }
   5:  
   6: public class Vip : Person
   7: {
   8:   // ...
   9: }

VB.NET

   1: Public Class Person
   2:   ' 
   3: End Class
   4:  
   5: Public Class Vip
   6:   Inherits Person
   7:   '
   8: End Class

Then I added a collection of people:

C#

   1: public class PersonList
   2: {
   3:   public void Add(object obj) {
   4:     // ...
   5:   }
   6:  
   7:   public void Add(Person p)
   8:   {
   9:     // ...
  10:   }
  11:  
  12:   public void Add(IEnumerable<Person> people)
  13:   {
  14:     foreach (Person p in people)
  15:     {
  16:       // ...
  17:     }
  18:   }
  19: }

VB.NET

   1: Public Class PersonList
   2:   Public Sub Add(ByVal obj As Object)
   3:     '
   4:   End Sub
   5:  
   6:   Public Sub Add(ByVal person As Person)
   7:     ' 
   8:   End Sub
   9:  
  10:   Public Sub Add(ByVal list As IEnumerable(Of Person))
  11:     ' 
  12:   End Sub
  13: End Class

Next I create a PersonList collection and then add a list of Vip’s:

C#

   1: class Program
   2: {
   3:   static void Main(string[] args)
   4:   {
   5:     PersonList people = new PersonList();
   6:  
   7:     List<Vip> others = new List<Vip> {
   8:       new Vip(), new Vip()
   9:     };
  10:  
  11:     people.Add(others);
  12:   }
  13: }

VB.NET

   1: Sub Main()
   2:   Dim people As New PersonList
   3:   Dim others As New List(Of Vip)(New Vip() {New Vip(), New Vip()})
   4:   people.Add(others)
   5: End Sub

When I compile this in Visual Studio 2008 the first Add method, taking the object argument, gets called.

But with Visual Studio 2010 (using the .NET 4 target) the third Add method gets called. This is because now IEnumerable<T> is co-variant and will now convert the List<Vip> to an IEnumerable<Person>.

Ok, granted. This is NOT something you will see every day, but if you ever encounter it, this might be very confusing.

This kind of problem can also occur with extension methods and user-defined conversions…