How to prove to CodeContracts that IEnumerable<T>.Single() never returns null?

Question

I have the following code snippet:

    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 says:

CodeContracts: assert unproven. Are you making some assumption on Single that the static checker is unaware of?

In my understanding, Single() never returns null - it returns either the exactly only value of the IEnumerable or it throws an exception. How can I proof this to the code analyzer?

Answer 1

In my understanding, Single() never returns null

Not true -

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.

That is correct - so if the collection contains just a single null value then Single will return null.