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


Предусловия при параллельном выполнении


Давайте рассмотрим типичное использование ограниченного буфера buffer клиентом, посылающим в него объект y с помощью процедуры put. Предположим, что buffer - это атрибут объемлющего класса, объявленный как buffer: BOUNDED_BUFFER [T] с элементами типа T (пусть y имеет этото же тип).

Клиент может, например, инициализировать buffer с помощью ссылки на реальный буфер, переданной из процедуры его создания, используя предложенную выше схему визитной карточки:

make (b: BOUNDED_BUFFER [T],...) is do ...; buffer := b; ... end

Так как buffer, имеющий сепаратный тип, является сепаратной сущностью, то всякий вызов вида buffer.put (y) является сепаратным и должен появляться лишь в подпрограмме, одним из аргументов которой является buffer. Поэтому мы должны вместо него использовать put(buffer, y), где put - подпрограмма из класса клиента (ее не следует путать с put из класса BOUNDED_BUFFER), объявленная как:

put (b: BOUNDED_BUFFER [T]; x: T) is -- Вставить x в b. (Первая попытка) do b.put (x) end

Но это не совсем верное определение. У процедуры put из BOUNDED_BUFFER имеется предусловие not full. Поскольку не имеет смысла пытаться вставлять x в полный b, то нам нужно скопировать это условие в новой процедуре из класса клиента:

put (b: BOUNDED_BUFFER [T]; x: T) is -- Вставить x в b require not b.full do b.put (x) end

Уже лучше. Как же можно вызвать эту процедуру для конкретных buffer и y? Конечно, при входе требуется уверенность в выполнении предусловия. Один способ состоит в проверке:

if not full (buffer) then put (buffer, y) -- [PUT1]

но можно также учитывать контекст вызова, например, в:

remove (buffer); put (buffer, y) -- [PUT2]

где постусловие remove включает not full. (В примере PUT2 предполагается, что начальное состояние удовлетворяет соответствующему предусловию not empty для самой операции remove.)

Будет ли это верно работать? В свете предыдущих замечаний о непредсказуемости ошибок в параллельных системах ответ неутешителен - может быть. Между проверкой на полноту full и вызовом put в варианте PUT1 или между remove и put в PUT2 может вклиниться какой-то другой клиент и снова сделать буфер полным.


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



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