在代码合同中使用Contract.ForAll

好的，我还有另一个代码合同问题。我有一个接口方法的合同，看起来像这样（为清楚起见省略其它方法）：在代码合同中使用Contract.ForAll

[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需要非空输入参数（它实现了一个接口有一个需求合同），所以我得到一个'需要未经证实：组！=空'错误的子组被传递到AddRequested。我是否正确使用ForAll语法？如果是这样，求解者根本不理解，还有另一种方法可以帮助求解器识别合同，或者每当调用GetAllGroups（）时，我是否只需要使用Assume？

来源

2010-06-23 Dan Bryant

最新版本已启用'ForAll'，你可能想试试:) – porges 2010-07-09 21:56:44

Code Contracts User Manual指出：“静态合同检查器尚未处理ForAll或Exists量子。”直到它，在我看来，选项是：

忽略警告。
在致电AddRequested()之前添加Contract.Assume(subGroup != null)。
在致电AddRequested()之前添加支票。也许if (subGroup == null) throw new InvalidOperationException()或if (subGroup != null) AddRequested(subGroup)。

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

来源

2010-06-25 08:42:29

谢谢;我想我可能会使用Assume，因为原始代码（合同前）没有空检查。它也干净地标记了静态证明者需要“帮助”的各个地方，以便希望我可以回过头来移除其中的一些，因为证明者变得更加强大。 – 2010-06-25 13:10:00

在代码合同中使用Contract.ForAll

回答

相关问题