Архитектура среды тестирования на основе моделей


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




    Начало  Назад  Вперед



    Книжный магазин