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