Основы объектно-ориентированного проектирования


О правилах доказательств - часть 3



где Nonsep_Pre (f) - множество предложений предусловия f, не содержащих сепаратных вызовов, а Nonsep_Post (f) - аналогичное множество для постусловия.

Это правило частично отражает суть параллельного вычисления. Для доказательства правильности программы все еще требуется доказать те же условия (в числителе), что и в последовательном правиле. Но следствия этого для свойств вызова различны: клиенту нужно обеспечивать меньше свойств перед вызовом, поскольку, как это подробно обсуждено выше, по меньшей мере бесполезно пытаться обеспечить выполнение сепаратной части предусловия; но и на выходе мы получаем меньше гарантированных утверждений. Первое отличие является хорошей новостью для клиента, а последнее - плохой.

Таким образом, сепаратные предложения предусловий и постусловий объединяются с инвариантом как свойства, которые должны быть включены во внутреннее доказательство правильности тела подпрограммы, но они не используются явно как свойства ее вызова.

Это правило также восстанавливает симметрию между предусловиями и постусловиями, дополняя обсуждение, в котором выделялась роль предусловий.




Начало  Назад  Вперед



Книжный магазин