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.