Инструменты тестирования на основе моделей - часть 3

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

Проверка моделей (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 дополняется двумя инструментами: для статической проверки сформулированных ограничений на основе дедуктивного анализа и для их динамической проверки при выполнении методов, ограничения к которым описаны.

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