4

我有以下界面：

[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 中抛出异常，我错过了什么？

谢谢

4

4 回答 4

2

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

public int CountOfItems
{
    get
    {
        int count = this.someEnumerable.Count();
        Contract.Assume(count > 0);
        return count;
    }
}
于 2012-08-06T21:26:48.130 回答
0

我认为，您无法在静态中证明这一点。
Enumerable.Count<TSource>扩展方法没有定义任何关于它的返回值的契约（例如，这个方法应该为无限序列返回什么？）。

因此，CC stais checker 会就此向您发出警告。

于 2012-08-03T12:04:29.220 回答
0

似乎向ContractInvariant实现添加方法可以解决警告。

于 2012-08-08T12:39:20.363 回答
0

假设您的代码是正确的。它有效，您只是试图让代码合同系统认识到这一事实。

这特别意味着调用CountOfItems的实例MyObject将始终返回大于零的值。它不会抛出异常，也不会返回零或更小的值。

这意味着someEnumerable将分配给某个对象，并且 someEnumerable.Count()对于引用的任何对象，都将始终返回大于零的值。这些事实在任何时候都是真实的（因为对何时CountOfItems可以调用没有限制。

MyObject这意味着存在一个包含这些事实的对象不变量（无论它是否在代码中明确说明） 。并且由于您的代码是正确的（假设），因此分配的MyObject保证的实现someEnumerable及其计数始终大于零。

因此，为了满足合同CountOfItems，合同系统需要了解这些不变量以及如何确保它们。

于 2012-08-03T16:23:08.127 回答