Проверка требований
После того как требования к модулю формализованы, проверка поведения модуля на соответствие им может осуществляться в процессе тестирования автоматически.
Предположим, что в некоторый момент времени t тестируемый модуль выполняет m операций f1, …, fm, которые были поданы на выполнение раньше на τ1, …, τm соответственно (τi≥ 1, i=1, …, m). Пусть C1, …, Cm - контракты операций f1, …, fm соответственно, и в моменты подачи операций f1, …, fm были выполнены предусловия preC1, …, preCm; тогда для проверки правильности поведения модуля в момент времени t необходимо проверить выполнимость предиката PostC1(τ1)
… PostCm(τm). Понятно, что для проверки соответствия поведения модуля требованиям также важно уметь строить хорошие тестовые последовательности, но рассмотрение этого вопроса выходит за рамки данной работы.
