Формализмы для спецификаций - часть 5
Представляются состояния как отображения множества программных переменных в VAR на значения из DATA. Тем самым для множества состояний STATE справедливо.
STATE = defVAR -> DATA.
Соответственно этому предикаты на состояниях можно представить в виде отображений вида
PRED: STATE -> В.
Эти предикаты могут использоваться в качестве утверждений для спецификации операторов. Оператор соответствует отображению
STATE -> STATE.
Метод утверждений позволяет специфицировать программу путем задания предикатов. Оператор специфицируется двумя предикатами, называемыми предусловием Q и постусловием R. При этом имеет место R, Q Î PRED. Оператор
f: STATE -> STATE
удовлетворяет этой спецификации, если справедливо следующее высказывание:
" s ÎSTATE: Q(s) => R(f(s)).
Таким образом, оператор специфицируется парой предикатов (Q, R). Утверждение Q может пониматься как предположение об исходном состоянии, а R специфицирует утверждение о выходном состоянии в случае выполнения предположения. Поэтому говорится также s спецификациях предположение/утверждение (англ. rely/guarantee или также assumption/commitment).