如何向CodeContracts证明IEnumerable <T> .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:断言未经证实.你是否在静态检查器不知道的Single上做了一些假设？

在我的理解中,Single()永远不会返回null - 它返回IEnumerable的唯一值或者抛出异常.如何向代码分析器证明这一点？

Answer 1

在我的理解中,Single()永远不会返回null

不对 -

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

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

它返回的确切唯一值IEnumerable或它抛出异常.

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