在代码合同中使用Contract.ForAll

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

[ContractClassFor(typeof(IUnboundTagGroup))] public abstract class ContractForIUnboundTagGroup : IUnboundTagGroup { public IUnboundTagGroup[] GetAllGroups() { Contract.Ensures(Contract.Result() != null); Contract.Ensures(Contract.ForAll(Contract.Result(), g => g != null)); return null; } } 

我有代码消耗这样的接口：

  public void AddRequested(IUnboundTagGroup group) { foreach (IUnboundTagGroup subGroup in group.GetAllGroups()) { AddRequested(subGroup); } //Other stuff omitted } 

AddRequested需要一个非null的输入参数（它实现了一个具有Requires契约的接口），因此我在传入AddRequested组中得到一个’requires unproven：group！= null’错误。 我正确使用ForAll语法吗？ 如果是这样并且求解器根本不理解，是否有另一种方法可以帮助求解器识别合同，或者我只需要在调用GetAllGroups（）时使用Assume？

Answer 1

“ 代码合同用户手册”声明：“静态合同检查程序尚未处理Quantiers ForAll或Exists。” 在此之前，在我看来，选项是：

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

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