Это ошибка в статическом контроллере контрактов? - PullRequest
Новая
       23

Это ошибка в статическом контроллере контрактов?

6 голосов
/ 17 декабря 2009

Если я напишу это: 

public sealed class Foo
{
    private int count;
    private object owner;
    private void Bar()
    {
        Contract.Requires(count > 0);
        Contract.Ensures(owner == null || count > 0);

        if (count == 1)
            owner = null;
        --count;
    }
}

Статическая проверка контракта может подтвердить все утверждения.

Но если я напишу это вместо: 

public sealed class Foo
{
    private int count;
    private object owner;
    private void Bar()
    {
        Contract.Requires(count > 0);
        Contract.Ensures(owner == null || count > 0);

        --count;
        if (count == 0)
            owner = null;
    }
}

Он утверждает, что постусловие owner == null || count > 0 недоказано.

Я думаю, что могу доказать, что вторая форма не нарушает это постусловие: 

// { count > 0 } it's required
--count;
// { count == 0 || count > 0 } if it was 1, it's now zero, otherwise it's still greater than zero
if (count == 0)
{
    // { count == 0 } the if condition is true
    owner = null;
    // { count == 0 && owner == null } assignment works
}
// { count == 0 && owner == null || count != 0 && count > 0 } either the if was entered or not
// { owner == null || count > 0 } we can assume a weaker postcondition

Что-то не так с моим доказательством?

Я добавил утверждения в своем доказательстве, когда Contract.Assert вызывает код, и пришел к выводу, что если я добавлю только это, ему удастся доказать постусловие: 

--count;
Contract.Assert(count == 0 || count > 0)
if (count == 0)
    owner = null;

Но, если я теперь изменю это же утверждение на "более естественный" способ, он потерпит неудачу: 

--count;
Contract.Assert(count >= 0)
if (count == 0)
    owner = null;

Можно ожидать, что эти два утверждения были эквивалентны, но статическая проверка обрабатывает их по-разному.

(кстати, я использую бета-версию 2 VS10)

Ответы [ 2 ]

1 голос
/ 17 декабря 2009

Я бы не ожидал, что это очень сложное средство проверки будет в полностью рабочем состоянии, поскольку это всего лишь бета-версия. Я думаю, что это ошибка или, по крайней мере, вопрос, который стоит обсудить с разработчиками, потому что это очень просто сделать статическую проверку автоматически.

В любом случае, судя по всему, маркер обеспечивает только то, чтобы сказать, способна ли программа проверки статических контрактов обеспечить условие или нет. Это не означает, что условие недействительно, это просто означает, что оно не может найти доказательство.

Я бы гораздо больше беспокоился о случаях, когда говорится, что что-то гарантировано, что недействительно. Это будет считаться ошибкой!

0 голосов
/ 17 декабря 2009

Предостережение: я абсолютно ничего не знаю о специфике системы контрактов .net.

Тем не менее, я могу вам сказать следующее: буквально невозможно (см. Проблему с остановкой), чтобы получить полный доказатель для утверждений, столь же богатых, как и тот, который, как кажется, поддерживает эта система.

Итак: это ошибка? №

С другой стороны, представляется правдоподобным предположить, что это может быть распространенным случаем, который разработчики средства проверки могут захотеть добавить в свою систему.

...