对所有代码合同使用contract.

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

[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()时,我只需要使用一个假设?