Если значения всех переменных, присутствующих
Правило вывода SP2 – «Подпрограмма или сегмент программы»
Если значения всех переменных, присутствующих в условии В, остаются неизменными при выполнении подпрограммы или сегмента программы S и
If
{V} S {P}
then
{V and B} S
(Р and B} and
{V or В} S {Р or В} <
Правило вывода SР2 непосредственно следует из правил вывода SP1, DC1 и DС2.
Чтобы применить правило вывода SР2, необходимо разделить постусловие на две части. В одной части должны быть ссылки лишь на те переменные, чьи значения не изменяются в результате выполнения S. Эта часть постусловия является (согласно правилу вывода SP1) его собственным предусловием. Во второй части постусловия содержатся ссылки на все те переменные, значения которых изменяются (или могли бы измениться) в результате выполнения S. Тем самым будет получено предусловие для той части постусловия (применяя, например, соответствующие правила вывода или используя формальную спецификацию S). И, наконец, эти два частных предусловия нужно объединить, образуя требуемое предусловие.
