为什么不能证明这个合同声明？

我有一个类，它看起来是这样的：为什么不能证明这个合同声明？

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" 
    } 
}

据我所知，有合同都需要知道result不会是空的信息。 bars至少有一个元素。如果其中一个元素匹配SomePredicate，result将是第一个这样的元素。如果不是，result将成为bars中的第一个元素。

为什么断言失败？

来源

2011-07-28 Matthew Pirocchi

您尚未确保或假定bars中的元素不为空。尝试：

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

或（实际不变）：

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

来源

2011-07-28 14:54:55 user7116

或'Contract.Requires（bars.Any（X => X = NULL）！）' – leppie

@leppie：要么就是那些表单首选？我在用户文档中找到的所有内容是“也可以使用扩展方法'System.Linq.Enumerable.Any'而不是'Contract.Exists'。” –

@Matthew：如果永远不可能有空元素，则使用ForAll，否则使用Any。使用'Any'时，你还必须在代码的后半部分有'First（x => x！= null）'。细微差别。 – leppie

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

来源

2011-07-28 14:54:15 Sven

如果bars的第一个元素是null会怎么样？（A：断言失败。）

来源

2011-07-28 14:54:31 dlev

为什么不能证明这个合同声明？

回答

相关问题