Using Contract.ForAll in Code Contracts

Question

Okay, I have yet another Code Contracts question. I have a contract on an interface method that looks like this (other methods omitted for clarity):

[ContractClassFor(typeof(IUnboundTagGroup))]
public abstract class ContractForIUnboundTagGroup : IUnboundTagGroup
{
    public IUnboundTagGroup[] GetAllGroups()
    {
        Contract.Ensures(Contract.Result<IUnboundTagGroup[]>() != null);
        Contract.Ensures(Contract.ForAll(Contract.Result<IUnboundTagGroup[]>(), g => g != null));

        return null;
    }
}

I have code consuming the interface that looks like this:

    public void AddRequested(IUnboundTagGroup group)
    {
            foreach (IUnboundTagGroup subGroup in group.GetAllGroups())
            {
                AddRequested(subGroup);
            }
            //Other stuff omitted
    }

AddRequested requires a non-null input parameter (it implements an interface which has a Requires contract) and so I get a 'requires unproven: group != null' error on the subGroup being passed into AddRequested. Am I using the ForAll syntax correctly? If so and the solver simply isn't understanding, is there another way to help the solver recognize the contract or do I simply need to use an Assume whenever GetAllGroups() is called?

Milore

The latest version has enabled ForAll, you might want to give it a try :) – Harriot

Answer 1

The Code Contracts User Manual states, "The static contract checker does not yet deal with quantiers ForAll or Exists." Until it does, it seems to me the options are:

1. Ignore the warning.
2. Add Contract.Assume(subGroup != null) before the call to AddRequested().
3. Add a check before the call to AddRequested(). Maybe if (subGroup == null) throw new InvalidOperationException() or if (subGroup != null) AddRequested(subGroup).

Option 1 doesn't really help. Option 2 is risky because it will circumvent the AddRequested() Requires contract even if IUnboundTagGroup.GetAllGroups() no longer ensures that post-condition. I'd go with option 3.

Microfiche

Thanks; I'm thinking I'll probably go with using Assume, since the original code (pre-Contracts) did not have a null check. It also cleanly marks the various places where the static prover needed 'help' so that hopefully I can go back and remove some of them as the prover becomes more powerful. – Milore