在代码合同中使用 Contract.ForAll

Question

好的，我还有另一个代码合同问题。我有一个看起来像这样的接口方法的合同（为清楚起见，省略了其他方法）：

[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 需要一个非空输入参数（它实现了一个具有 Requires 合同的接口），因此我在传递到 AddRequested 的子组上收到“需要未经证实：组！= null”错误。我是否正确使用了 ForAll 语法？如果是这样并且求解器根本不理解，是否有其他方法可以帮助求解器识别合同，或者我是否只需要在调用 GetAllGroups() 时使用 Assume？

Answer 1

Code Contracts User Manual 声明：“静态合约检查器尚未处理量词 ForAll 或 Exists。”在此之前，在我看来，选项是：

1. 忽略警告。
2. 在调用AddRequested()之前添加Contract.Assume(subGroup != null)。
3. 在调用AddRequested() 之前添加检查。也许是if (subGroup == null) throw new InvalidOperationException() 或if (subGroup != null) AddRequested(subGroup)。

选项 1 并没有真正的帮助。选项 2 是有风险的，因为它会绕过 AddRequested() Requires 合同，即使 IUnboundTagGroup.GetAllGroups() 不再确保该后置条件。我会选择选项 3。