代码之家 › 专栏 › 技术社区 › Dan Bryant

对所有代码合同使用contract.

forall code-contracts static-analysis c#

12

Dan Bryant · 技术社区 · 14 年前

好吧,我还有一个代码契约问题。我在一个接口方法上有一个契约,看起来像这样(为了清晰起见,省略了其他方法):

[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协定的接口),因此我得到了一个“Requires unproven:Group!”=null'传递到的子组上的错误 附加请求 . 我是否正确使用了forall语法?如果是这样,并且解算器根本不理解,有没有其他方法帮助解算器识别契约,或者在调用getAllGroups()时,我只需要使用一个假设?

1 回复 | 直到 14 年前

1

10

Jack Leitch 14 年前

这个 Code Contracts User Manual 声明,“静态合同检查程序尚未处理所有或存在的分位数。”在处理之前,我认为选项如下:

忽略警告。
添加 Contract.Assume(subGroup != null) 在呼叫之前 AddRequested() .
在呼叫前添加支票 附加请求() . 也许吧 if (subGroup == null) throw new InvalidOperationException() 或 if (subGroup != null) AddRequested(subGroup) .

选项1没有真正的帮助。选项2具有风险,因为它将绕过 附加请求() 需要合同,即使 IUnboundTagGroup.GetAllGroups() 不再保证岗位条件。我会选择第三种。