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


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



Здесь INV - инвариант класса, Pre (f) - множество предложений предусловия f, а Post (f) - множество предложений постусловия. Напомним, что утверждение является конъюнкцией набора предложений вида:

clause1; ...; clausen

Знаки больших "и" означают конъюнкцию всех предложений. Фактические аргументы f явно не указаны, но выражения со штрихами, такие как t.q' , означают подстановку фактических аргументов вызова вместо формальных аргументов f.

Из соображений краткости правило приведено в форме, не поддерживающей доказательства вызовов рекурсивных процедур. Однако добавление такой поддержки никак не повлияет на наше обсуждение. Детали, связанные с рекурсией, можно найти в [M 1990].

Причина, по которой предложения утверждения рассматриваются по отдельности, а затем соединяются посредством "и", заключается в том, что в таком виде правило подготовлено для перехода к описанному ниже случаю сепаратных вызовов при параллелизме. Для подготовки к параллельному случаю также интересно, что инвариант INV учитывается при доказательстве для тела подпрограммы (в числителе правила), но невидим при доказательстве вызова (в знаменателе).

Что изменится в параллельном случае? В предложении предусловия может появиться ожидание только для предусловий в виде t.cond, где t - это сепаратная сущность, являющаяся формальным аргументом подпрограммы, содержащей рассматриваемый вызов. В подпрограмме вида:

f (..., a: T, ...) is require clause1; clause2; ... do ... end

любое из предложений предусловия, не содержащее сепаратный вызов на сепаратном формальном аргументе, является условием корректности: любой клиент должен обеспечить выполнение этого условия перед каждым вызовом, иначе вызов будет ошибочным. Всякое предложение предусловия, включающее вызов вида a.some_condition, в котором a является сепаратным формальным аргументом, является условием ожидания, которое будет блокировать вызов до своего выполнения.

Эти наблюдения можно выразить в виде правила доказательства, которое заменяет для сепаратного вычисления предыдущее последовательное правило:




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



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