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

Question

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

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 экземпляр никогда не может иметь nullPath имущество.

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

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 не может быть нулевым

Я что-то здесь упустил?

Answer 1

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

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

Другими словами, ваши варианты:

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

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

2. добавлять Contract.Assume(settings.Path != null) конструктору Program учебный класс.

Answer 2

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