如何向CodeContracts证明IEnumerable. single()永远不会返回null

本文关键字：永远 null 返回 single CodeContracts 证明 IEnumerable | 更新日期: 2023-09-27 17:49:32

我有以下代码片段:

    public static string returnString()
    {
        string[] stringList = { "a" };
        if (stringList.Count() != 1)
        {
            throw new Exception("Multiple values in list");
        }
        var returnValue = stringList.Single();
        Contract.Assert(returnValue != null, "returnValue is null");
        return returnValue;
    }

CodeContract说:

CodeContracts:断言未经验证。你是否对单个做了一些静态检查器不知道的假设?

在我的理解中，Single()从不返回null -它返回IEnumerable的唯一值或抛出异常。我如何向代码分析器证明这一点?

如何向CodeContracts证明IEnumerable<T>. single()永远不会返回null

在我的理解中，Single()从不返回null

Not true -

string[] a = new string[] {null};
bool check = (a.Single() == null);  // true

它要么返回IEnumerable的唯一值，要么抛出异常。

那是正确的-所以如果集合只包含一个null值，那么Single将返回null。

相关文章：