Code Contracts - ForAll - What is supported by static verification

Question

There are numerous information that static checking of Contract.ForAll has only limited or no support.

I did lot of experimenting and found it can work with:

• Contract.ForAll(items, i => i != null)
• Contract.ForAll(items, p) where p is of type Predicate<T>

it cannot work with:

• Field access
• Property access
• Method group (I think delegate is allocated here anyway)
• Instance method call

My questions are:

• What are other types of code that ForAll can work with?
• Does the Code Contracts undertand that after Contract.ForAll(items, i => i != null) is proven, that when taking one item from the list later in code (i.e. by indexing), the item is not null?

Here is full test code:

public sealed class Test
{
    public bool Field;
    public static Predicate<Test> Predicate;

    [Pure]
    public bool Property
    {
        get { return Field; }
    }    

    [Pure]
    public static bool Method(Test t)
    {
        return t.Field;
    }

    [Pure]
    public bool InstanceMethod()
    {
        return Field;
    }

    public static void Test1()
    {
        var items = new List<Test>();
        Contract.Assume(Contract.ForAll(items, i => i != null));
        Contract.Assert(Contract.ForAll(items, i => i != null)); // OK
    }

    public static void Test2()
    {
        var items = new List<Test>();
        Contract.Assume(Contract.ForAll(items, Predicate));
        Contract.Assert(Contract.ForAll(items, Predicate)); // OK
    }

    public static void Test3()
    {
        var items = new List<Test>();
        Contract.Assume(Contract.ForAll(items, i => i.Field));
        Contract.Assert(Contract.ForAll(items, i => i.Field)); // assert unproven
    }

    public static void Test4()
    {
        var items = new List<Test>();
        Contract.Assume(Contract.ForAll(items, i => i.Property));
        Contract.Assert(Contract.ForAll(items, i => i.Property)); // assert unproven
    }

    public static void Test5()
    {
        var items = new List<Test>();
        Contract.Assume(Contract.ForAll(items, Method));
        Contract.Assert(Contract.ForAll(items, Method)); // assert unproven
    }

    public static void Test6()
    {
        var items = new List<Test>();
        Contract.Assume(Contract.ForAll(items, i => i.InstanceMethod()));
        Contract.Assert(Contract.ForAll(items, i => i.InstanceMethod()));// assert unproven
    }
}

Answer 1

I was not able to find more working expressions, in fact I found that even Contract.ForAll(items, i => i != null) is not working reliably (but it understands that the item is not null when later used inside foreach in the same function). Finally, I gave up on possibility to use more complex ForAll contracts with static checker.

Instead I devised a way to control which contract are for static checker, and which are for runtime checker. I present this method here, in hope that it might be useful for people interesting in original question. The benefit is ability to be write more complex contracts, which can be checked at runtime only, and leave only easily provable contracts for static checker (and easily keep warnings at low count).

For that, 2 builds Debug are needed (If you don't already have them), Debug and Debug + Static Contracts, The Debug build has conditional compilation symbol MYPROJECT_CONTRACTS_RUNTIME defined. In this way it receives all Contract. and RtContract. contracts. Other builds receive only Contract. contracts.

public static class RtContract
{
    [Pure] [ContractAbbreviator] [Conditional("MYPROJECT_CONTRACTS_RUNTIME")]
    public static void Requires(bool condition)
    {
        Contract.Requires(condition);
    }

    [Pure] [ContractAbbreviator] [Conditional("MYPROJECT_CONTRACTS_RUNTIME")]
    public static void Ensures(bool condition)
    {
        Contract.Ensures(condition);
    }

    [Pure] [Conditional("MYPROJECT_CONTRACTS_RUNTIME")]
    public static void Assume(bool condition)
    {
        Contract.Assume(condition);
    }
}

public class Usage
{
   void Test (int x)
   {
        Contract.Requires(x >= 0);  // for static and runtime
        RtContract.Requires(x.IsFibonacci());  // for runtime only
   }
}