Static Checker problem with LINQ's Contains()

Question

Hello Guys,

I'm using VS 2010 Ultimate and the latest version of Code Contracts (1.4.50126.1).

I've noticed and "isolated" a problem with static checker: it produces the "CodeContracts: requires unproven: source != null" warning even when I have an invariant for the property used in expression.

namespace My
{
    using System;
    using System.Diagnostics.Contracts;
    using System.Linq;
    
    public class InternalClass
    {
        [ContractInvariantMethod]
        private void ObjectInvariant()
        {
            Contract.Invariant(Integers != null);
        }

        public InternalClass()
        {
            Integers = new[] { 1, 2, 3 };
        }

        public Int32[] Integers { get; set; }
    }

    public class TestClass
    {
        public TestClass()
        {
            InternalClass obj = new InternalClass();

            // obj.Integers.ToString();

            obj.Integers.Contains(1);
        }
    }
}

The warning points to the "obj.Integers.Contains(1);" line.
Please also notice the commented string. If I uncomment it, checker's warning dissapears! For me it is very odd behavior.

Answer 1

If you change "Integers" to a property with a read-only backing field the warning will go away. (Also if you add the requires value =! null to the setter.)

The problem is that there are no means of controlling what value callers might assign using the public setter. Your invariant (together with the non-existing requires) states that InternalClass is responsible for ensuring the non-nullness. I.e. if I do "obj.Integers = null" I don't violate any contract, but InternalClass does.

- Raphael

Answer 2

The problem is that there are no means of controlling what value callers might assign using the public setter.

By adding the Invariant, I claim that this property has both Require and Ensure contracts. This is clearly stated in Code Contracts documentation:

2.3.1 Invariants on Automatic Properties

Automatic properties are getters and setters without an explicit implementation. Due to the lack of a code body, it isn't possible to write Requires or Ensures directly on such auto-properties. Instead, we use invariants on auto-properties to indirectly write such pre- and postconditions on the setters and getters of
auto-properties. For example, the code below

... here goes the example ...

As the example illustrates, invariants on auto-properties turn into:
1. A precondition for the setter
2. A postcondition for the getter
3. An invariant for the underlying backing field

Anyway, even if I had added precondition to this property, that wouldn't guarantee that 3rd party code couldn't assign 'null' to it.

 I.e. if I do "obj.Integers = null" I don't violate any contract, but InternalClass does.

This is totally untrue. As a developer, you are responsible for making sure that your code doesn't violate any contracts. And if you set "obj.Integers" to "null", you violate InternalClass's contract.

Also, your post doesn't explain why uncommenting of "obj.Integers.ToString();" line removes the warning.