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

Весьма часто желательно доказать корректность цикла совместно с его инициализацией (см. листинг 6.11, где задано условие I — инвариант цикла). Для этого мы располагаем правилом вывода W2.

Листинг 6.11. Правило вывода W2 — «Цикл с условием продолжения с инициализацией».

Правило вывода W2 объединяет в себе правила вывода SI, Р1 и W1 и следует из них.

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

• 1) найти инвариант цикла I (если он не был уже указан разработчиком или программистом);
• 2) доказать, что {V} — инициализация {1} (т.е. I изначально истинно);
• 3) доказать, что {I and В} ОР{1} (т.е. тело цикла обеспечивает сохранение истинности Г);
• 4) доказать, что {I and not В} => Р (т.е. постусловие Р истинно при завершении цикла).

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

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

Доказательство завершения обычно заключается в демонстрации того, что:

• • значение некоторого выражения увеличивается или уменьшается, по крайней мере, на фиксированное значение при каждом выполнении ОР;
• • существует соответственно верхняя или нижняя границы значений такого выражения.

Часто граница вытекает из условия В цикла while; иногда она является частью инварианта цикла. Такое выражение называют вариантом цикла. Строго говоря, для шага ОР требуется также показать, что весь цикл вообще выполняется, т. е. не может возникнуть ошибки фазы прогона (например, переполнение, ссылка на неописанную переменную и т. п.).

Правило «Разделяй и властвуй» № 1

Листинг 6.12. Правило вывода DC1 — «Разделяй и властвуй».

Правило вывода DC1 обобщается очевидным образом на произвольное число элементов (Р1, Р2, РЗ, Р4 и т. д.).

Иногда при доказательстве корректности, например в постусловии сегмента программы, возникает длинное выражение. Применяя правило вывода DC1, длинное постусловие, состоящее из двух или нескольких частей, объединенных операциями логического умножения and, можно разбить на более короткие части, получить предусловия отдельно для каждой части и затем объединить такие предусловия. При этом, конечно же, не уменьшится объем усилий, затрачиваемых на доказательство, но оно обычно становится лучше организованным, более ясным и более простым для восприятия. Отдельные шаги алгебраических преобразований часто оказываются более короткими и более простыми. Даже очень длинные и сложные выражения подчиняются стратегии «Разделяй и властвуй».

Правила «Разделяй и властвуй» № 2—4. Как было сказано выше, правило вывода DC1 относится к элементам, связанным операциями логического умножения and. Аналогичное правило вывода существует и для элементов, связанных операциями логического сложения or.

Листинг 6.13. Правило вывода DC2 — «Разделяй и властвуй».

Листинг 6.14. Правило вывода DC3 — «Разделяй и властвуй».

Поавило вывода DC3 представляет собой правило вывода DC1 при.

Листинг 6.15. Правило вывода DC4 — «Разделяй и властвуй».

Правило вывода DC4 представляет собой правило вывода DC2 при

Правило подпрограммы или сегмента программы № 1 формулируется следующим образом: если значения всех переменных, присутствующих в условии В, остаются неизменными при выполнении сегмента программы S (например, подпрограммы), то {В} S {В}.

Листинг 6.16. Правило вывода SP1 — «Подпрограмма или сегмент программы».

Если в условии В используются лишь такие переменные, значения которых одинаковы до и после выполнения S, очевидно, что значение В до исполнения S равно значению В после исполнения S. Следовательно, если В истинно до исполнения S, то В будет истинным и после исполнения S, т. е. В является предусловием для самого себя по отношению к S.

Правило подпрограммы или сегмента программы № 2. Если значения всех переменных, присутствующих в условии В, остаются неизменными при выполнении подпрограммы или сегмента программы S и если {V} S {Р}, то это правило записывается так, как представлено в листинге 6.17.

Листинг 6.17. Правило вывода SP2 —"Подпрограмма или сегмент программы".

Правило вывода SP2 непосредственно следует из правил вывода SP1, DC1 и DC2.

Чтобы применить правило вывода SP2, необходимо разделить постусловие на две части. В одной части должны быть ссылки лишь на те переменные, значения которых не изменяются в результате выполнения S. Эта часть постусловия является (согласно правилу вывода SP1) его собственным предусловием. Во второй части постусловия содержатся ссылки на все переменные, значения которых изменяются (или могли бы измениться) в результате выполнения S. Тем самым будет получено предусловие для этой части постусловия (применяя, например, соответствующие правила вывода или используя формальную спецификацию S). И, наконец, эти два частных предусловия нужно объединить, образуя требуемое предусловие.

Правило подпрограммы или сегмента программы № 3. Если значения всех переменных, присутствующих в условии В, остаются неизменными при выполнении подпрограммы или сегмента программы S, то это правило записывается так, как представлено в листингах 6.18 и 6.19.

Листинг 6 Л 8. Правило вывода SP3 — «Подпрограмма или сегмент программы». Цикл с условием продолжения инициализации.

Листинг 6.19. Правило вывода SP3 —"Подпрограмма или сегмент программы". Цикл с условием продолжения без инициализации.

Правило вывода SP3 является комбинацией правил вывода SP2 и Р1.

Та часть постусловия, которая зависит от результата выполнения S (т.е. Р в вышеприведенном утверждении), может быть более слабой по сравнению с тем постусловием, которое в действительности устанавливается при выполнении S (т.е. Р1). Аналогично соответствующая часть предусловия, которая в действительности удовлетворяется до выполнения S (т.е. V), может оказаться сильнее того предусловия, которое требуется для удовлетворительной работы S (т.е. VI).