Если значения всех переменных, присутствующих
Правило вывода 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).