Contract.Requires and DateTime

Question

I have the following method:

private static void SampleMethod(DateTime dateTime1, DateTime dateTime2)
{
    Contract.Requires(dateTime1 > dateTime2);
    Console.WriteLine("date 1 > date 2");
}

SampleMethod(DateTime.Today, DateTime.Today.AddDays(1));

When I build it with static checking enabled, I get the warning CodeContracts: requires unproven: dateTime1 > dateTime2

Note that dynamic checking is working fine for me, its only the static checking I'm having a problem with.

How do I go about either proving this assertion, or else suppressing the warning?

EDIT:

I was reading about the ContractVerificationAttribute, if I add [ContractVefirication(false) to the method it makes no difference (I suspect this might be a bug) but adding it to the class will turn off static checking correctly for the whole class. Am still looking for a way to turn off static checking for that one Requires though.

Answer 1

The static verifier has its limitations, sometimes you have to help. It has a limited understanding of numerical math but DateTime seems to be out of its scope.

That's why Contract.Assume(bool) exists:

    DateTime d1 = DateTime.Today;  
    DateTime d2 = d1.AddDays(-7);

    Contract.Assume(d1 > d2);

    SampleMethod(d1, d2);

CodeContracts: Checked 4 assertions: 4 correct