3

Looking at the code sample below, Microsoft Code Contracts warns:

CodeContracts: Missing precondition in an extremely visible method. Consider adding Contract.Requires(science == null); for parameter validation

Am I missing something here? Why would CC suggest that I require the parameter to be null, which is the exact opposite of what should be done here?

I'm using VS2015, .NET 4.6.

using System;
using System.Diagnostics.Contracts;
public sealed class Weird
{

    public Weird(object science)
    {
        if (null == science)
        {
            throw new ArgumentNullException();
        }

        Contract.EndContractBlock();

        this.Science = science;
    }
    private object Science { get; }

    [ContractInvariantMethod]
    private void ObjectInvariant()
    {
        Contract.Invariant(null != this.Science);
    }
}
2
  • I'm confused here--it sounds like what it's asking for is correct. You throw on null anyway, why not specify that as a contract? Commented Sep 29, 2015 at 22:30
  • The condition of the parameter validation is the inverse of the condition of the contract. So, to avoid an ArgumentNullException, CC should suggest Contract.Requires (science != null). But instead, it's suggesting science==null. Commented Sep 29, 2015 at 23:28

4 Answers 4

4

This isn't a much better answer than your workaround, but I got it to "work" by simply changing:

private object Science { get; }

to:

private object Science { get; set; }

Basically the same as your workaround but without providing your own backing field. I guess Code Contracts doesn't quite understand the new syntax.

1
3

Try not to use reverse comparison. In C# there's no need to write:

if (null == science)

instead of

if (science == null)

Your code will become clearer and I think the wrong contract suggestion will be gone.

Also, if you'll make a mistake and write just an assignment (=) inside if block, compiler will warn you about that.

To make your code even more clear you can try to use some AOP stuff, like PostSharp, and specify your contracts as property attributes in interface, which your class will implement. So the contracts logic will not interleave with business logic.

5
  • 1
    Are you saying that the CC warning is due to null == science or are you just offering that advice in general? Commented Sep 29, 2015 at 19:28
  • Both. I don't use reverse comparison in my code and wasn't getting such warnings from MS Code Contracts when I used it. Commented Sep 29, 2015 at 19:40
  • @MikhailTumashenko, I reversed the order of the comparison (to science == null). Unfortunately, Code Contracts still issues the same warning. Commented Sep 29, 2015 at 20:38
  • Which version of MS CC are you using? Commented Sep 29, 2015 at 20:48
  • I'm not sure how to check the version number of CC. I'm using Visual Studio 2015, and CC is integrated. This is unlike previous versions of CC that were installed as addons to VS. Commented Sep 29, 2015 at 20:57
2

Based on the work-arounds, it looks like CC doesn't understand that the read-only auto property is writeable in the constructor. Both work-arounds provided remove the action of writing to a read-only property. Perhaps CC is trying to avoid executing a statement that it believes to be in error ( this.Science = science; ) by sending the execution down the only other branch available ( null == science ).

Earlier versions of C# did not allow writing to a read-only auto property. I guess the Code Contracts system didn't get the memo!

1

I find that the warning goes away when I replace the auto property with a field-backed property. Compare the following code with what I posted in my original question:

using System;
using System.Diagnostics.Contracts;
public sealed class Weird
{        
    public Weird(object science)
    {
        if (science == null)
        {
            throw new ArgumentNullException();
        }

        Contract.EndContractBlock();

        this.science = science;
    }

    private readonly object science;

    private object Science
    {
        get
        {
            return this.science;
        }
    }

    [ContractInvariantMethod]
    private void ObjectInvariant()
    {
        Contract.Invariant(null != this.Science);
    }
}

I'm not liking this, because I don't necessarily want use a field-backed property solely for the purpose of satisfying a Code Contract. But, oh well, I guess.

I'm still open to an answer that allows me to satisfy my contract while using auto properties.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.