Может ли инвариантный метод [ContractInvariantMethod] работать внутри контракта интерфейса?

Question

Я создаю интерфейсный контракт, как описано в § 2.8. Интерфейсные контракты из 4 февраля 2011 г. Руководство пользователя кодовых контрактов (PDF) .Это не проблема.

Кроме того, я хочу смешать инвариант объекта (см. § 4.2 ContractInvariantMethod ) в том же интерфейсе контракта.Это проблема.Я не могу найти примеры использования объектных инвариантов в интерфейсных контрактах.

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

/* Note: The intention of this snippet is to cause the data implementation
 * to fail if it is not initalized before its public data access methods are called. 
 */
[ContractClassFor(typeof(IDataProxy))]
abstract class IDataProxyContract : IDataProxy
{
    [ContractInvariantMethod]
    private void ObjectInvariant()
    {
        Contract.Invariant(IsInited == true, "Instance not initialized.");
    }

Я не могу найти документацию, которая конкретно описывает этот сценарий или опровергает его.

На данный момент я не уверен, пропускаю ли я какой-либо шаг, чтобы заставить его работать, или если технология Code Contract полностью игнорирует объектный инвариант в этом контексте.Я хотел бы заставить это работать.Кто-нибудь знает ответ?

Answer 1

Очевидно, ответ на форуме DevLabs ответил Мануэль Фандрих, Microsoft (MSFT):

Инварианты объектов на интерфейсах в настоящее время не поддерживаются.Я понимаю, почему они могут быть полезны.

Полный контекст и пример кода здесь ...

Answer 2

Инварианты предоставляют механизм для ограничения внутреннего состояния объекта .

Они рассматриваются как детали реализации, поэтому они реализованы внутри частного метода. Интерфейсы, очевидно, не имеют понятия состояния (даже свойства являются синтаксическим сахаром для методов) и, следовательно, не могут иметь инвариантов. В их наиболее примитивном использовании инварианты используются на полях. Однако концепция автоматических свойств, очевидно, размыла эту линию, что привело к путанице в этом случае.

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

Answer 3

По умолчанию они отключены.

Я предполагаю, что контракты не включены опциями компилятора, поэтому они не вплетаются в код.

решение состоит в том, чтобыскачайте этот пакет с devlabs

• http://msdn.microsoft.com/en-us/devlabs/dd491992

после его установки, перейдите в свойства проекта и вы увидите еще одну вкладку.

затем вы можете включить опцию: «Выполнить проверку контракта во время выполнения: полная»