c# - 如何向 CodeContracts 证明 IEnumerable.Single() 永远不会返回 null？

Question

我有以下代码片段:

    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: assert unproven. Are you making some assumption on Single that the static checker is unaware of?

在我看来，Single() 永远不会返回 null - 它要么返回 IEnumerable 的唯一值，要么抛出异常。我如何向代码分析器证明这一点？

Answer 1

In my understanding, Single() never returns null

不正确-

string[] a = new string[] {null};

bool check = (a.Single() == null);  // true

It returns either the exactly only value of the IEnumerable or it throws an exception.

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