确保的 CodeContract 问题

Question

我得到以下代码：

    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;
    }

它给了我

警告 19 CodeContracts：确保未经验证：!String.IsNullOrEmpty(Contract.Result())

为什么？

Answer 1

我不知道 String.Format() 函数是否有任何约定，但它只能承诺 result != null，即空字符串是有效结果。

我检查过： String.Format() 仅确保结果！= null

您可以通过插入 Assume() 来简单地修复它：

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

但我会认真重新考虑制作结果此处的合同部分不为空。这对来电者真的很重要吗？