Правило усиления предусловия и ослабления постусловия
Предметом каждого правила вывода является взаимосвязь предусловия и постусловия. Начнем с правила вывода, которое в ряде случаев поможет упростить алгебраические преобразования выражений, возникающих в ходе доказательства. Это правило следует из вышеприведенного определения предусловий и постусловий и упрощает восприятие ряда других правил.
Правило вывода Р1 – «Усиление предусловия и ослабление постусловия»
If
V Þ V1 and
{V1} OP {P1} and
P1 Þ P
then
{V} OP {P} <
Если условие V
истинно перед выполнением оператора OP и если из V следует V1, то V1 истинно перед выполнением оператора OP. Если V1 является предусловием для P1 по отношению к OP, то P1 будет истинным после выполнения оператора OP. Если, наконец, из P1 следует Р, то и Р будет истинным после выполнения оператора OP. Иными словами, из истинности V перед выполнением OP следует истинность Р после его выполнения. Следовательно, V является предусловием для Р по отношению к OP.
Продвигаясь по программе в обратном направлении, можно усилить условия. Усиление условие может быть достигнуто путем добавления произвольного элемента с помощью операции логического умножения and или отбрасыванием элемента, участвующего в операции логического сложения or.
Двигаясь по программе в прямом направлении, можно ослабить условия. Условие может быть ослаблено добавлением произвольного элемента с помощью операции логического сложения or или отбрасыванием элемента, участвующего в операции логического умножения and.
Разумное усиление предусловий или ослабление постусловий (что встречается реже) может привести к получению более простых выражений и сокращению (иногда значительному) объема алгебраических преобразований в процессе доказательства. Вместе с тем, здесь следует соблюдать известную осторожность, чтобы не усилить предусловие или не ослабить постусловие столь сильно, что нельзя будет завершить доказательство. В приводимых ниже примерах показывается, каким образом можно легко обойти такую потенциально возможную проблему.
