为什么这个合约断言不能被证明?

本文关键字：不能 证明 断言 为什么 | 更新日期: 2023-09-27 18:03:55

我有一个类，看起来像这样:

class Foo
{
    private IEnumerable<Bar> bars;
    ...
    private void DoSomething()
    {
        Contract.Requires(bars != null);
        Contract.Requires(bars.Any());
        Bar result = bars.FirstOrDefault(b => SomePredicate) ?? bars.First();
        Contract.Assert(result != null); // This asserts fails the static checker as "cannot be proven"
    }
}

据我所知，Contracts拥有所有需要知道result不会为空的信息。bars中至少有一个元素。如果这些元素中的一个与SomePredicate匹配，则result将是第一个这样的元素。如果不是，result将是bars的第一个元素。

为什么断言失败?

为什么这个合约断言不能被证明?

集合bars仍然可以包含null项。如果该项目是第一项，那么result仍然可以是null。

您没有确保或假设bars内部的元素不为空。试一试:

Contract.ForAll(bars, x => x != null);

或者(实际的不变量):

Contract.Requires(bars.FirstOrDefault(x => SomePredicate(x)) != null
               || bars.First() != null);

如果bars的第一个元素是null呢?(A:断言失败)

相关文章：