CodeContract проблема с обеспечивает - PullRequest
Новая
       2

CodeContract проблема с обеспечивает

1 голос
/ 31 июля 2011

Я получил следующий код: 

    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 ())

Почему?

1 Ответ

2 голосов
/ 31 июля 2011

Я не знаю, есть ли у функции String.Format() какие-либо контракты, но она может только пообещать, что result != null, пустая строка, является допустимым результатом.

Я проверил: только String.Format () обеспечивает результат! = Null

Вы можете просто исправить это, вставив Assume(): 

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

Но я бы серьезно пересмотрел вопрос о том, чтобы результат не был пустым частью вашего контракта здесь.Это действительно имеет значение для абонентов?

...