Уточним и дополним понятие предикатной спецификации, определенное в разд. 1.2. Рассмотрим следующую простую схему взаимодействия программы с окружением: ввод входных данных происходит перед началом исполнения программы, вывод результатов - по завершению исполнения, а других взаимодействий с окружением нет. В данной схеме программа реализует функцию, отображающую значения входных данных в значения результатов. Допустим, программа представлена оператором S; x обозначает набор входных данных, а y - набор результатов. Спецификация программы определяется формулой P(x) & Q(x, y), где P(x) - предусловие, истинное перед исполнением программы, а Q(x, y) - постусловие, истинное после исполнения программы. Программа со спецификацией представляется известной тройкой Хоара {P(x)} S {Q(x, y)}, см. [9].
Спецификация P(x) & Q(x, y) является предикатной при условии, что взаимодействие программы с окружением ограничивается вводом данных перед началом исполнения и выводом результатов после завершения. Программа принадлежит классу программ с предикатной спецификацией, если удается переместить ввод всех данных перед началом исполнения программы, а вывод - после завершения исполнения. Для программы реального времени (реактивной системы) подобный перенос ввода и вывода принципиально невозможен. Такая программа относится к классу программ с процессной спецификацией [4; 5], поскольку эффект исполнения программы нельзя представить в виде функции - эффект определяется только в виде процесса. Спецификация может быть адекватно представлена на языке алгебры процессов Р. Милнера [12] или Т. Хоара [13].