在代码合同中使用Contract.ForAll

Question

好的,我还有另一个Code Contracts问题.我有一个接口方法的合同,看起来像这样(为清楚起见省略了其他方法):

[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;
    }
}

我有代码消耗这样的接口:

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

AddRequested需要一个非空输入参数(它实现具有需要契约的接口),所以我得到了"需要得到证实:组= NULL"在亚错误被传递到AddRequested.我正确使用ForAll语法吗？如果是这样,并在求解根本不理解,有另一种方式来帮助求解承认合同或者我只需要使用时GetAllGroups()被调用的假设？

Answer 1

" 代码合同用户手册"声明:"静态合同检查程序尚未处理Quantare ForAll或Exists." 在此之前,在我看来,选项是:

1. 忽略警告.
2. Contract.Assume(subGroup != null)在致电之前添加AddRequested().
3. 在通话前添加支票AddRequested().也许if (subGroup == null) throw new InvalidOperationException()还是if (subGroup != null) AddRequested(subGroup).

选项1并没有真正帮助.备选方案2存在风险,因为AddRequested()即使IUnboundTagGroup.GetAllGroups()不再确保后置条件,它也将绕过" 需求"合同.我选择3.