Pex and Code Contracts 10 April 2010 Peter-Himschoot VS2010, .NET Development 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: 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: 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: 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: So, you can guide Pex by supplying contracts on the arguments of your methods.