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