在Code Contracts中使用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
    }

< p >< code >AddRequested< /code >需要一个非空的输入参数（它实现了一个要求契约的接口），所以当我将subGroup传递到< code >AddRequested< /code >时，会出现“requires unproven：group！= null”的错误。我是否正确使用了ForAll语法？如果是这样，而求解器只是不能理解，是否有另一种方法帮助求解器识别契约，或者在调用GetAllGroups（）时是否仅需要使用Assume？< /p >

- Dan Bryant

---

最新版本已启用ForAll，你可能想试试 :) - porges

Answer 1

代码合约用户手册中指出："静态合约检查程序目前尚未处理全称量词 ForAll 或 Exists。" 在它处理之前，我认为以下是选项：

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

选项1并没有帮助。选项2很危险，因为即使 IUnboundTagGroup.GetAllGroups() 不再确保后置条件，它也将规避 AddRequested() 要求的合约。我会选择选项3。

- Jack Leitch

---

谢谢；我想我可能会选择使用Assume，因为原始代码（在Contracts之前）没有空检查。它还清晰地标记了静态证明器需要“帮助”的各个地方，这样希望随着证明器变得更加强大，我可以回去删除其中一些。 - Dan Bryant