c# - 为什么不能证明这个契约(Contract)主张？

Question

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

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 不会为 null 的所有信息。 bars 中至少有一个元素。如果其中一个元素与 SomePredicate 匹配，则 result 将是第一个这样的元素。如果不是，result 将是 bars 中的第一个元素。

为什么断言会失败？

Answer 1

集合 bars 仍可能包含一个 null 的项目。如果该项目是第一项，则 result 仍然可以是 null。