Кодовые контракты. Почему некоторые инварианты не рассматриваются вне класса?

Рассмотрим этот неизменный тип:

public class Settings
{
    public string Path { get; private set; }

    [ContractInvariantMethod]
    private void ObjectInvariants()
    {
        Contract.Invariant(Path != null);
    }

    public Settings(string path)
    {
        Contract.Requires(path != null);
        Path = path;
    }
}

Здесь можно заметить две вещи:

• Существует инвариант контракта, который гарантирует, что свойство Path никогда не может быть null
• Конструктор проверяет значение аргумента Path для соответствия предыдущему контрактному инварианту

На этом этапе экземпляр Setting никогда не может иметь свойство null Path.

Теперь посмотрим на этот тип:

public class Program
{
    private readonly string _path;

    [ContractInvariantMethod]
    private void ObjectInvariants()
    {
        Contract.Invariant(_path != null);
    }

    public Program(Settings settings)
    {
        Contract.Requires(settings != null);
        _path = settings.Path;
    } // <------ "CodeContracts: invariant unproven: _path != null"
}

В принципе, он имеет свой собственный контрактный инвариант (в поле _path), который не может быть выполнен во время статической проверки (см. комментарий выше). Это звучит немного странно для меня, так как это легко доказать:

• settings является неизменным
• settings.Path не может быть нулевым (поскольку параметры имеют соответствующий контрактный инвариант)
• поэтому, присваивая settings.Path _path, _path не может быть null

Я что-то пропустил?

Ответы

Ответ 1

После проверки форума контрактов с кодами, я нашел этот похожий вопрос со следующим ответом от одного из разработчиков:

Я думаю, что поведение, которое вы испытываете, вызвано каким-то интерподированием, который происходит. Статическая проверка сначала анализирует конструкторы, затем свойства, а затем методы. При анализе конструктора Sample он не знает, что msgContainer.Something!= Null, поэтому он выдает предупреждение. Способ решить это, либо путем добавления предположения msgContainer.Something!= Null в constuctor, либо лучше добавить postcondition!= Null к Something.

Иными словами, ваши варианты:

• Сделать свойство Settings.Path явным, а не автоматическим, и вместо этого указать инвариант в поле поддержки. Чтобы удовлетворить ваш инвариант, вам нужно добавить предварительное условие к аксессуру набора свойств: Contract.Requires(value != null).

  Вы можете при желании добавить постсоединение к get accessor с помощью Contract.Ensures(Contract.Result<string>() != null), но статический контролер не будет жаловаться в любом случае.

• Добавьте Contract.Assume(settings.Path != null) в конструктор класса Program.

Ответ 2

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