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

       

Правило последовательности операторов


Правило вывода S1 - «Последовательность операторов»

If

{V} OP1 {P1} and

{P1} OP2 (Р}

then

{V} (OP1;OP2) {Р} <

Правило вывода S1 очевидным образом обобщается на последовательность операторов произвольной длины. Таким образом, для того чтобы отыскать предусловие для заданного постусловия по отношению к последовательности операторов, сначала отыщем предусловие для Р

по отношению к последнему оператору последовательности. Затем воспользуемся им в качестве постусловия по отношению к предыдущему, предпоследнему оператору и так далее, то есть будем продвигаться от оператора к операто­ру по последовательности в обратном направлении. Полученное таким образом предусловие по отношению к первому оператору последовательности является также предусловием для Р по отношению ко всей последовательности.



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