Предусловия при параллельном выполнении
Давайте рассмотрим типичное использование ограниченного буфера buffer клиентом, посылающим в него объект y с помощью процедуры put. Предположим, что buffer - это атрибут объемлющего класса, объявленный как buffer: BOUNDED_BUFFER [T] с элементами типа T (пусть y имеет этото же тип).
|
Клиент может, например, инициализировать buffer с помощью ссылки на реальный буфер, переданной из процедуры его создания, используя предложенную выше схему визитной карточки: |
Так как 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 может вклиниться какой-то другой клиент и снова сделать буфер полным.
Это тот же дефект, который ранее потребовал от нас обеспечить резервирование объекта через инкапсуляцию.
| Мы снова можем попробовать инкапсуляцию, написав PUT1 или PUT2 как процедуры, в которые buffer передается в качестве аргумента, например, для PUT1: |
| Но на самом деле это не очень поможет клиенту. Во-первых, причиняет неудобство проверка условия was_full при возврате, а затем что делать, если оно истинно? Попытаться снова - возможно, но нет никакой гарантии успеха. На самом деле хотелось бы иметь способ выполнить put в тот момент, когда буфер будет наверняка неполон, даже если придется ждать, пока это случится. |
