Теория и практика защиты программ

Правило цикла с условием продолжения с инициализацией


Правило вывода W2 – «Цикл с условием продолжения с инициализацией

 

Пусть задано условие I

(инвариант цикла).

If

{V} инициализация {I} and

{I and B} OP

{I} and

(I and not B} Þ Р

then

{V} (инициализация; while В do OP endwhile) {P} <

Правило вывода W2 объединяет в себе (и следует из) правила вывода S1, P1 и W1.

Чтобы доказать частичную корректность цикла с условием продолжения с помощью правила вывода W2, необходимо:

1.     найти инвариант цикла I (если он не был уже указан разработчиком или программистом);

2.     доказать, что {V} инициализация {I} (то есть I изначально истинно);

3.     доказать, что {I and B} OP {I} (то есть тело цикла обеспечивает сохранение истинности I) и

4.     доказать, что (I and not В}Þ

постусловие P

(то есть P

истинно при завершении цикла). Для доказательства, что цикл полностью корректный, необходимо дополнительно

5.     показать, что цикл завершается, то есть существует верхняя граница числа выполнений оператора OP.

Доказательство завершения обычно заключается в показе того, что (1) значение некоторого выражения увеличивается или уменьшается по крайней мере на фиксированное значение при каждом выполнении OP и что (2) существует соответственно верхняя или нижняя граница значений такого выражения. Часто граница вытекает из условия В

цикла while; иногда она является частью инварианта цикла. Такое выражение называют вариантом цикла. Строго говоря, для шага OP

требуется также показать, что весь цикл вообще выполняется, то есть не может возникнуть «ошибка фазы прогона» (например, переполнение, ссылка на неописанную переменную и т.п.).



Содержание раздела