CodeContracts: возможно, вызов метода по нулевой ссылке

Question

У меня есть аргумент с помощью инструмента статического анализа CodeContracts .

Мой код:

Снимок экрана http://i40.tinypic.com/r91zq9.png

( версия ASCII )

Инструмент сообщает мне, что instance.bar может быть нулевой ссылкой. Я верю в обратное.

Кто прав? Как я могу доказать это неправильно?

Answer 1

Обновление : похоже, проблема в том, что инварианты не поддерживаются для статических полей .

2-е обновление: Ниже описан метод , рекомендуемый в настоящее время .

Возможный обходной путь - создать свойство для instance, которое Ensure будет содержать инварианты, которые вы хотите сохранить. (Конечно, вам нужно Assume их для подтверждения Ensure.) После того, как вы это сделаете, вы можете просто использовать свойство, и все инварианты должны быть проверены правильно.

Вот ваш пример использования этого метода:

class Foo
{
    private static readonly Foo instance = new Foo();
    private readonly string bar;

    public static Foo Instance
    // workaround for not being able to put invariants on static fields
    {
        get
        {
            Contract.Ensures(Contract.Result<Foo>() != null);
            Contract.Ensures(Contract.Result<Foo>().bar != null);

            Contract.Assume(instance.bar != null);
            return instance;
        }
    }

    public Foo()
    {
        Contract.Ensures(bar != null);
        bar = "Hello world!";
    }

    public static int BarLength()
    {
        Contract.Assert(Instance != null);
        Contract.Assert(Instance.bar != null);
        // both of these are proven ok

        return Instance.bar.Length;
    }
}

Answer 2

Ваш код содержит частный статический инициализированный экземпляр:

private static Foo instance = new Foo();

Предполагаете ли вы, что это означает, что конструктор instance всегда будет запускаться до доступа к любому статическому методу, поэтому обеспечение инициализации bar будет *

В однопоточном корпусе, я думаю, вы правы.

Последовательность событий будет:

1. Позвоните на Foo.BarLength()
2. Статическая инициализация класса Foo (если еще не завершена)
3. Статическая инициализация частного статического члена instance с экземпляром Foo
4. Вход в Foo.BarLength()

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

Итак, у вас может быть такой сценарий:

1. Тема Альфа: Звоните на Foo.BarLength()
2. Thread Alpha: Статическая инициализация класса Foo (если еще не завершена) начинается
3. Переключение контекста
4. Тема бета: Звоните на Foo.BarLength()
5. Thread Beta: Нет вызова для статической инициализации класса Foo, поскольку это уже выполняется
6. Тема бета: вход в Foo.BarLength()
7. Тема бета: доступ к null статическому члену instance

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

Answer 3

CodeContracts является правильным. Ничто не мешает вам установить instance.bar = null до вызова метода BarLength().

Answer 4

Если вы пометите поле 'bar' только для чтения, это должно удовлетворить статический анализатор, что поле никогда не будет установлено на что-либо еще после выполнения ctor.

Answer 5

Я согласен с вами. instance и bar являются частными, поэтому CodeContracts должен знать, что instance.bar никогда не устанавливается в ноль.