12

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

[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. 我是否正确使用了 ForAll 语法？如果是这样并且求解器根本不理解，是否有另一种方法可以帮助求解器识别合同，或者我是否只需要在调用 GetAllGroups() 时使用 Assume？

4

1 回答 1

10

代码合同用户手册指出， “静态合同检查器尚未处理量词 ForAll 或 Exists。” 在此之前，在我看来，选项是：

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

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

于 2010-06-25T08:42:29.780 回答