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