очевидным образом на произвольное число
Правило вывода 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.
