очевидным образом на произвольное число
Правило вывода
DC1 – «Разделяй и властвуй»
If
{V1} OP {Р1} and
{V2} OP {Р2}
then
{V1 and V2} OP
{P1 and P2} <
Правило вывода
DC1 обобщается
очевидным образом на произвольное число элементов (P1, P2, РЗ,
P4 и т.д.).
Иногда при доказательстве корректности, например, в постусловии сегмента программы, возникает длинное выражение. Применяя правило вывода
DC1, длинное постусловие, состоящее из двух или нескольких частей, объединенных операциями логического умножения and
, можно разбить на более короткие части, получить предусловия отдельно для каждой части и затем объединить такие предусловия. При этом конечно же, не уменьшится объем усилий, затрачиваемых на доказательство, но оно обычно становится лучше организованным более ясным и более простым для восприятия. Отдельные шаги алгебраических преобразований часто оказываются более короткими и более простыми. Даже очень длинные и сложные выражения подчиняются стратегии «разделяй и властвуй».
Правило вывода
DC1 относится к элементам, связанным операциями логического умножения and. Аналогичное правило вывода существует и для элементов, связанных операциями логического сложения or.