Модели для композиции указываются инструменту

Модели для композиции указываются инструменту построения тестов перечислением имен соответствующих классов.

Проверка моделей (model checking). Свойства безопасности проверяются за счет анализа возможности нарушения инвариантов состояний, представленных как методы с особым атрибутом. Свойства живучести могут удостоверяться за счет анализа достижимости стабильных состояний, в которых специально отмеченные характеристические методы возвращают true.

Библиотека CodeContracts предоставляет средства для описания чисто декларативных ограничений на свойства входных параметров и результатов операций. Моделирование состояния не поддерживается. Имеются следующие возможности.

Ограничения записываются на языке C# в виде булевских выражений, передаваемых как аргументы библиотечным методам.
Можно описывать ограничения следующих видов.
- Предусловия операций (метод Contract.Requires).
- Постусловия операций при нормальной работе (Contract.Ensures).
- Постусловия операций при выдаче исключения (Contract.EnsuresOnThrow).
- Утверждения о выполнении некоторых свойств в какой-то точке кода внутри метода (Contract.Assert).
- Инварианты классов — оформляются в виде методов со специальной аннотацией, содержащих обращения к Contract.Invariant.
Помимо обычных выражений на C# можно использовать следующие.
- Кванторные выражения, оформленные в виде обращений к методам Contract.Exists и Contract.ForAll.
- Обращение к значениям выражений до выполнения проверяемого метода в постусловиях в виде вызова метода Contract.OldValue.
- Обращение к значению результата в постусловиях с помощью Contract.Result.
Библиотека CodeContracts дополняется двумя инструментами: для статической проверки сформулированных ограничений на основе дедуктивного анализа и для их динамической проверки при выполнении методов, ограничения к которым описаны.

Содержание Назад Вперед