Code Contracts can't invert conditionals?

Question

I have this struct (simplified for brevity):

public struct Period
{
    public Period(DateTime? start, DateTime? end) : this()
    {
        if (end.HasValue && start.HasValue && end.Value < start.Value)
        {
            throw new ArgumentOutOfRangeException("end", "...");
        }
        Contract.EndContractBlock();

        this.start = start;
        this.end = end;
    }

    private readonly DateTime? start;
    private readonly DateTime? end;

    public static Period operator +(Period p, TimeSpan t)
    {
        Contract.Assume(!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);
    }
}

But the static checker is giving me this warning:

CodeContracts: requires unproven: end.HasValue && start.HasValue && end.Value >= start.Value

This requirement that it inferred from the custom parameter validation is just plain wrong. I want to allow null values for start or end, and only require start <= end if both are provided. However, if I change the constructor to this:

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

I get this warning, which looks more correct, but it's hard to see why the requires can't be proven:

CodeContracts: requires unproven: !start.HasValue || !end.HasValue || start.Value <= end.Value

I thought it might be having trouble with the ?:, but this warning is still there when I change the operator to:

public static Period operator +(Period p, TimeSpan t)
{
    var start = p.start.HasValue ? p.start.Value + t : (DateTime?) null;
    var end = p.end.HasValue ? p.end.Value + t : (DateTime?) null;

    Contract.Assume(!start.HasValue || !end.HasValue || start.Value <= end.Value);
    return new Period(start, end);
}

And of course, if I change that .Requires to .Assume, the warning goes away completely, but that's not an acceptable solution.

So it appears that the static checker in Code Contracts is not able to invert the condition correctly. Rather than simply inverting the condition by wrapping it with !(…) or applying De Morgan's law (as shown above), it appears to be inverting just the last component of the condition. Is the static checker unable to correctly interpret complex conditionals when using custom parameter validation?

Interestingly, I tried this, thinking the static checker would just strip the ! off the front, but no:

if (!(!start.HasValue || !end.HasValue || start.Value <= end.Value))
{
    throw new ArgumentOutOfRangeException("end", "...");
}
Contract.EndContractBlock();

CodeContracts: requires unproven: !(!(!start.HasValue || !end.HasValue || start.Value <= end.Value))

In this case, it did just wrap the whole condition with !(…), even though it didn't have to.

Also, if I change the nullable DateTime's to just plain non-nullable DateTime's and rewrite the contracts like this, it works as expected without any warnings:

public struct Period
{
    public Period(DateTime start, DateTime end) : this()
    {
        Contract.Requires(start <= end);
        this.start = start;
        this.end = end;
    }

    private readonly DateTime start;
    private readonly DateTime end;

    public static Period operator +(Period p, TimeSpan t)
    {
        Contract.Assume(p.start + t <= p.end + t);   // or use temp variables
        return new Period(p.start + t <= p.end + t);
    }
}

But simply using Contract.Assume(p.start <= p.end) won't work.

CodeContracts: requires unproven: start <= end

Answer 1

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.