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

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

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