Pex и кодовые контракты - PullRequest
Новая
       55

Pex и кодовые контракты

1 голос
/ 07 декабря 2011

Ниже приведен пример кода из документации Pex pexandcontracts.pdf http://research.microsoft.com/en-us/projects/pex/pexandcontracts.pdf. Я понимаю, что это не специфичный для pex вопрос, скорее он относится к контрактам кода, но это код из учебных пособий pex. 

namespace CodeDigging
{
    public class StringExtension
    {
        public static string TrimAfter(string value, string suffix)
        {
            // <pex>
            Contract.Requires(!string.IsNullOrEmpty(suffix));
            // </pex>
            Contract.Requires(value != null);
            Contract.Ensures(!Contract.Result<string>().EndsWith(suffix));

            int index = value.IndexOf(suffix);
            if (index < 0)
                return value;                  // (1) First possible contract violation
            return value.Substring(0, index);  // (2) second possible contract violation
        }
    }
}

Статический верификатор выдает следующие предупреждения:

CodeContracts: обеспечивает недоказанность:! Contract.Result (). EndsWith (суффикс) в точке (1) и точке (2).

Мой вопрос: как можно решить эту проблему?Согласно исследованиям Pex, нет возможности нарушения контракта.(... есть?)

Ответы [ 3 ]

3 голосов
/ 07 декабря 2011

Я бы поспорил, что это плохое использование Contract.Ensures, поскольку гарантия довольно сложна и вряд ли может быть использована для более поздних Требований. Я был бы более склонен предоставить гарантии ненулевого значения и длины (т. Е. Не длиннее исходной строки значения). Вместо этого условие! EndsWith должно быть утверждением теста, который Pex может использовать для руководства своими исследованиями.

2 голосов
/ 07 декабря 2011

Лучше всего использовать Contract.Assume, когда статическая проверка не может проверить выражение.

У вас будет множество мест, где вам придется использовать Contract.Assume, если вы попытаетесь обнулить предупреждения статической проверки, если ваша программа не тривиальна, потому что большинство библиотек .Net еще не имеют контракты, чтобы я не беспокоился об этом. Большую часть времени иметь четкий код и хороший набор модульных тестов лучше, чем иметь предупреждения с нулевым контрактом. Тем не менее, оставьте сквигли, чтобы вы могли убедиться, что предупреждения являются ложноположительными, когда вы кодируете.

0 голосов
/ 26 сентября 2015

Да, есть возможность нарушить договор. Помните, что IndexOf и EndsWith по умолчанию используют сравнение, зависящее от культуры, что иногда может иметь неожиданное поведение. Если я напишу 

TrimAfter("\u0301a\u0301a", "\u0301a")

затем IndexOf не соответствует первому вхождению, потому что он рассматривает средние символы как один 'á', поэтому index равен 2, а метод возвращает "\u0301a", который, очевидно, заканчивается суффиксом .

Если вы хотите корректно доказывать правильность алгоритмов, используйте StringComparison.Ordinal.

Однако статическая проверка Code Contracts в настоящее время не поддерживает анализ строковых значений и не понимает эту связь между IndexOf и Substring.

...