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

Если значения всех переменных, присутствующих


Правило вывода SP3 – «Подпрограмма или сегмент программы»

Если значения всех переменных, присутствующих в условии В, остаются неизменными при выполнении подпрограммы или сегмента программы S и

If

VÞV1 and

{V1} S {Р1} and

P1ÞР

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

{V and В} S {Р and B}

and

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

{V or В} S {Р or В} <

Правило вывода SР3 является комбинацией правил вывода SР2 и P1.

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


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