Tag: forall

在代码合同中使用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？