c# - 代码契约(Contract) : How to satisfy 'Ensures Unproven' in property getter?

Question

我有以下界面:

[ContractClass(typeof(MyObjectContract))]
public interface IMyObject
{
    int CountOfItems { get; }
}

以下合约:

[ContractClassFor(typeof(IMyObject))]
public abstract class MyObjectContract
{
    int IMyObject.CountOfItems
    {
        get
        {
            Contract.Ensures(Contract.Result<int>() > 0);
            return 1;
        }
    }
}

以下实现:

public class MyObject : IMyObject
{
    private IEnumerable someEnumerable .... 

    public int CountOfItems
    {
        get
        {
            return this.someEnumerable.Count();
        }
    }
}

现在我收到一条警告说 ensures unproven: Contract.Result<int>() > 0

我应该如何证明计数大于零？我不想在 getter 中抛出异常，我错过了什么？

谢谢

Answer 1

正如其他人所提到的，您无法静态地证明 IEnumerable<T>.Count()由于基类库 (.NET Framework) 和静态检查器的限制，返回大于 0 的值。但是，您可以向静态检查器表明您假定该事实为真。这就是您使用基类库解决所有此类契约问题或静态检查器无法证明的陈述的方法。

public int CountOfItems
{
    get
    {
        int count = this.someEnumerable.Count();
        Contract.Assume(count > 0);
        return count;
    }
}