My First Code Contracts Bug?

Over the past few weeks (really, since I've finished all this cool set up type stuff), I've been using Code Contracts to verify my physics engine. Until yesterday, everything was going smoothly.

And then I managed to find a bug.

And, like all bugs, it took me a frustratingly long time to get to the bottom of it.

The idea of Code Contracts, in case you don't know, is that you can write code that will be checked for correctness at compile time (sometimes) and at run time (during those other times). You also get to determine what is correct for a given method or class. It's like writing unit tests for every possible valid input value for a method and having all the tests pass.

For instance, lets say you have a method addOne that takes an integer and returns that value incremented by one:

public int addOne(int input)
{
  return input + 1;
}

Easy enough, right? Now, lets say you want to restrict the input values to 0 or greater. Code Contracts lets you specify that like so: 

public int addOne(int input)
{
  Contract.Requires<ArgumentException>(input >=0, "Input must be greater than 0!");

  return input + 1;
}

This contract will generate an ArgumentException at run time with the given message if the input doesn't meet the precondition for the method (input >= 0).

This is fine, even a bit cool (sure beats writing if-then-throw blocks!) but what else can we do? Well, lets say we want to guarantee that the return value will be the input value + 1. We can write the following:

public int addOne(int input)
{
  Contract.Requires<ArgumentException>(input >=0, "Input must be greater than 0!");
  Contract.Ensures(Contract.Result<int>() == input + 1);

  return input + 1;
}

During the build process, the verifier will  go through the code and see that, yes, the method will indeed meet the stated condition. If you were to say, have the method return input - 1 while leaving the postcondition the same, the verifier would warn you that something was wrong.  Cool, huh?

I think so. Like all software, however, this has some bugs. One of the important parts of verification is that it needs to be easy and it needs to be able to verify methods that are inherited from super types as well as those derived from other types with other methods that are verified.

I've been trying like crazy to get a simple == operator to work between two structs. The first is my Vector2 struct, the second is Edge. Vector2 has an X, a Y and a Length (which is derived from X and Y) while Edge is simply two Vector2s, V1 and V2.

My Vector2 == operator simply compares the X's and the Y's and returns whether they are both equal to each other. This compiled fine with no warnings. My Edge struct, trying to compare the Vector2s using the same principle, consistently generated a "Ensures unproven" warning, no matter how I tried to resolve it.

I finally broke down and wrote two classes that represented what I was doing with the structs. By trial and error I determined the following really annoying thing about Code Contracts. Composition works from within class objects but not other structures.

TestComposite Class: No Errors

TestComposite Struct: Errors

Could this be the first bug I've found in Code Contracts? I'm sure it's possible. If this were some sort of design feature, I would think it would have been documented somewhere. Unless I'm doing something so incomprehensibly stupid that it's just a rule of thumb (please, point this out to me if this is the case). I'll probably be posting to the Microsoft Dev forum about this at some point, just to get a definitive answer. At least I know how to work around it, which means I should be pushing a new update sometime soon.

Keep an eye out for a new article on setting up Jenkins to automatically deploy build artifacts to CodePlex. I think I'm going to take a bit of a break from CC before I try to dive deep again.

Happy hacking!