c# – 为什么不能证明这个合同断言？

发布时间：2020-12-16 01:45:59 所属栏目：百科来源：网络整理

导读：我有一个看起来像这样的类： class Foo{ private IEnumerableBar bars; ... private void DoSomething() { Contract.Requires(bars != null); Contract.Requires(bars.Any()); Bar result = bars.FirstOrDefault(b = SomePredicate) ?? bars.First(); Contra

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

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拥有它需要知道的所有信息,结果不会为空.酒吧至少有一个元素.如果其中一个元素与SomePredicate匹配,则结果将是第一个这样的元素.如果没有,结果将是条形图中的第一个元素.

为什么断言失败了？

解决方法

您尚未确定或假设栏内的元素不为空.尝试：

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

或者(你的实际不变量)：

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

（编辑：李大同）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!