Если значения всех переменных, присутствующих
Правило вывода SP1 – «Подпрограмма или сегмент программы»
Если значения всех переменных, присутствующих в условии В, остаются неизменными при выполнении сегмента программы S
(например, подпрограммы, то
{B} S {B} <
Если в условии В используются лишь такие переменные, значения которых одинаковы до и после выполнения S, очевидно, что значение В до исполнения S равно значению В после исполнения. Следовательно, если В истинно до исполнения, то В будет истинным и после, то есть В является предусловием для самого себя по отношению к S.
