Конспект установочных лекций по комплексному курсу Информатика, Теория информации


Формализмы для спецификаций - часть 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).

 




Начало  Назад  Вперед



Книжный магазин