CodeContract problem with ensures

问题:

I got the following code:

    protected virtual string FormatException(Exception exception, int intendation)
    {
        Contract.Requires(intendation >= 0);
        Contract.Requires<ArgumentNullException>(exception != null);
        Contract.Ensures(!String.IsNullOrEmpty(Contract.Result<string>()));

        var msg = exception.ToString().Replace("\r\n", "\r\n".PadRight(intendation, '\t'));
        string text = string.Format("\r\n******* EXCEPTION ********\r\n\t{0}", msg);
        return text;
    }

It gives me

Warning 19 CodeContracts: ensures unproven: !String.IsNullOrEmpty(Contract.Result())

Why?

回答1:

I don't know if the String.Format() function has any contracts but it could only promise that the result != null, an empty string is a valid result.

I checked: String.Format() only ensures result != null

You can simply fix it by inserting an Assume() :

Contract.Assume(!String.IsNullOrEmpty(text));
return text;

But I would seriously reconsider making result is not empty part of your contract here. Does it really matter to the callers?