Почему статический контролер CodeContracts предполагает, что я заключу контракт (a) сразу после того, как я заключил контракт. (A)?

Question

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

public abstract class InitializerClass 
{ 
    protected bool _initialized 

    public bool IsInitialized 
    { 
     get { return _initialized; } 
    } 

    public virtual void Initialize() 
    { 
     //Warning CodeContracts: Missing precondition in an externally visible 
     //method. Consider adding Contract.Requires(this.IsInitialized); for 
     //parameter validation 
     Contract.Ensures(IsInitialized); 
    } 
} 

это другой класс:

public abstract class OrderingClass 
{ 
    protected bool _ordered 

    public bool IsOrdered 
    { 
     get { return _ordered; } 
    } 

    public override void Initialize() 
    { 
     //Message CodeContracts: Suggested assume: Contract.Assume(this.IsOrdered); 
     Contract.Ensures(IsOrdered); 
    } 
} 

на самом деле, оба предупреждения указывают на закрытие фигурной скобки методов, в строках, которые просто соответствуют требованиям Contract.Ensure. Что случилось с моим кодом?

Answer 1

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

Существует два способа устранения предупреждения.

Во-первых, добавить предложенное предварительным условием:

public virtual void Initialize() 
{ 
    Contract.Requires(IsInitialized); 
    Contract.Ensures(IsInitialized); 
} 

Во-вторых, установить значение IsInitialized в true:

public virtual void Initialize() 
{ 
    IsInitialized = true; 
    Contract.Ensures(IsInitialized); 
} 

Вам нужно будет добавить частный сеттера к IsInitialized для того, чтобы приведенный выше код для работы.

public bool IsInitialized 
{ 
    get { return _initialized; } 
    private set { __initialized = value; } 
} 

Просто установка _initialized = true в Initialize(), вероятно, не позволит контракты кода для проверки пост-состояние, поэтому добавление частного сеттера. Однако, сказав, что добавив следующий контракт на IsInitialized может свести на нет необходимости добавлять свойство сеттер:

Вы получаете предупреждение в OrderingClass для той же самой причине. Код контракта предлагает Contract.Assume(), потому что вы не можете использовать Contract.Requires() в переопределениях.