Code Contracts can't invert conditionals?

.net, c#, code-contracts

Solution

I think part of the problem may be your conditional that you're using in the `Contract.Requires` call.

Take the example of your one constructor:

public Period(DateTime? start, DateTime? end) : this()
{
    Contract.Requires(!start.HasValue || !end.HasValue || start.Value <= end.Value);
    this.start = start;
    this.end = end;
}

What if `start.HasValue` is `false` (meanining `!start.HasValue` is `true`), but `end` does have a value. What does `start.value <= end.Value` evaluate to in this situation, since one is `null` and the other has a value?

It seems instead, that your `Contract.Requires` condition should be stated as follows:

Contract.Requires(!(start.HasValue && end.HasValue) || start.Value <= end.Value);

If either one of `start` or `end` don't have a value, then the conditional will return `true` (and the OR condition short circuits, never evaluating whether or not `start.Value <= end.Value`). However, if both `start` and `end` have a value assigned, the first part of the conditional returns `false`, at which point then, `start.Value` must be less than or equal to `end.Value` in order for the conditional to evaluate to `true` overall. This is what you're after.

Here's a question for you: is it true that any instance of `Period` requires that `start.Value <= end.Value` or one or the other (or both) of them are `null`? If so, you could specify this as an Invariant, instead. That means that at any method entry or exit, `!(start.HasValue && end.HasValue) || start.Value <= end.Value` must hold true. This can simplify your contracts quite a bit when it works out.

UPDATE

Reviewing my blog article I posted in the comments (TDD and Code Contracts), you can safely annotate your `operator +(Period p, TimeSpan t)` implementation with the Code Contracts `PureAttribute` attribute. This attribute tells the Code Contracts static analyzer that the method does not alter any internal state of the object on which the method is called, and is therefore side-effect free:

[Pure]
public static Period operator +(Period p, TimeSpan t)
{
    Contract.Requires(!(p.start.HasValue && p.end.HasValue) || p.start.Value <= p.end.Value)

    return new Period(
        p.start.HasValue ? p.start.Value + t : (DateTime?) null,
        p.end.HasValue ? p.end.Value + t : (DateTime?) null);
}

UPDATE

OK, I thought about this some more, and I think I now understand the issue that Code Contracts is having with your contracts. I think you further need to add a `Contract.Ensures` contract (i.e. a post condition contract) to your constructor:

public Period(DateTime? start, DateTime? end) : this()
{
    Contract.Requires(!(start.HasValue && end.HasValue) || start.Value <= end.Value);
    Contract.Ensures(!(this.start.HasValue && this.end.HasValue) || this.start.Value <= this.end.Value);
    this.start = start;
    this.end = end;
}

This tells Code Contracts that when your constructor exits, the object's `start` and `end` fields, if they both have a value, must satisfy the condition that `start.Value <= end.Value`. If that condition is not satisfied, (potentially) an exception will be thrown by Code Contracts. This should also help out the static analyzer.

UPDATE (again, and mostly for completeness)

I did some more sleuthing on the "unproven" warning. This can occur both for `Requires` and `Ensures`. Here's another example of someone having a similar problem: http://www.go4answers.com/Example/ensures-unproven-contractresult-79084.aspx.

Adding a contract invariant can be done as follows (for the code in question by the OP):

[ContractInvariantMethod]
protected void PeriodInvariants()
{
    Contract.Invariant(!(start.HasValue && end.HasValue) || start.Value <= end.Value);
}

This method will be called upon every entry/exit into a method on the object to ensure that this condition holds true.

Another blog entry that should prove interesting

I found another blog entry by someone else that may prove interesting: http://www.rareese.com/blog/net-code-contracts

In this case, I disagree with the author's "solution" to getting rid of the `requires unproven` warning. Here's the author's code:

public static void TestCodeContract(int value)
{
    if(value > 100 && value < 110)
        TestLimits(value); 
}

public static void TestLimits(int i)
{
    Contract.Requires(i > 100);
    Contract.Requires(i < 110);

    //Do Something
}

Here, the real solution to the problem should be the following:

public static void TestCodeContract(int value)
{
    Contract.Requires(value > 100 && value < 110);
    // You could alternatively write two Contract.Requires statements as the blog
    // author originally did.
}

This should also get rid of the warning since the static analyzer now knows that `value` must be in the range of 101 to 109, which also happens to satisfy the contract criteria of the `TestLimits` method.

My suggestion to you, therefore, is to check wherever the `Period` constructor is called, and/or the `Period.operator +(...)` method to ensure that the calling method also has the necessary `Contract.Requires` statements (or, alternatively, `Contract.Assume`, which tells the static analyzer to just assume that the conditional provided is true).

When using Code Contracts, you need to instrument all of your code. You normally can't "pick and choose" which part to specify contracts for, as the static analyzer most likely won't have enough information to complete its analysis (and therefore, ensure the contracts are being guaranteed) and you will receive many warnings.

Problem

Original source