在代码合同中使用Contract.ForAll [英] Using Contract.ForAll in Code Contracts

问题描述

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

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合同的接口），因此我在传递的subGroup上收到 requires unproved：group！= null错误放入 AddRequested 。我是否正确使用ForAll语法？如果是这样，并且求解器根本不了解，是否还有另一种方法可以帮助求解器识别合同，或者只要调用GetAllGroups（）我就需要使用Assume吗？

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?

推荐答案

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

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. 忽略警告。


2. 在调用 AddRequested（） Contract.Assume（subGroup！= null） c $ c>。


3. 在调用 AddRequested（）之前添加支票。也许 if（subGroup
== null）抛出新的InvalidOperationException（）或 if（subGroup！= null）
AddRequested（ subGroup）。

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).

选项1并没有真正的帮助。选项2有风险，因为即使 IUnboundTagGroup.GetAllGroups（）不再确保 AddRequested（）需要合同，它也可以避免后置条件。我会选择选项3。

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.

这篇关于在代码合同中使用Contract.ForAll的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！