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

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 никогда не может иметь свойства 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 не может быть нулевым

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

Answer 1

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

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

Другими словами, ваши параметрыявляются:

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

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

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

Answer 2

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