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

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

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 значение аргумента для уважения предыдущего инварианта контракта

На данном этапе a Setting экземпляр никогда не может иметь a 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 поле), который не может быть удовлетворен во время статической проверки (cf. комментарий выше). Это звучит немного странным мне, так как легко доказать его:

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

Я пропускал что-то здесь?