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


Параллельная семантика предусловий - часть 2


Для программы в виде "визитной карточки":

r (x: separate SOME_TYPE) is do some_attribute := x end

или в каком-либо другом виде, не содержащем вызова вида x.some_routine, не требуется ждать фактического аргумента, соответствующего x.

Если же такой вызов имеется, то для удобства авторов клиентов он должен быть отражен в краткой форме класса. Это будет указываться в заголовке подпрограммы как r (x: blocking SOME_TYPE)...

С помощью нашего правила приведенная выше версия put в классе клиента достигнет желаемого результата:

put (b: BOUNDED_BUFFER [T]; x: T) is require not b.full do b.put (x) ensure not b.empty end

Вызов вида put (buffer, y) из клиента-производителя будет ждать, пока buffer не станет свободным (доступным) и не полным. Если buffer свободен, но полон, то данный вызов не может выполняться, но какой-нибудь другой клиент-потребитель может получить доступ к буферу (поскольку предусловие not b.empty, интересующее потребителей, будет в данном случае выполнено); после того, как такой клиент удалит некоторый элемент, сделав буфер неполным, клиент-производитель сможет начать выполнение своего вызова.

Как реализации решить, какой из двух или более клиентов, условия запуска вызовов которых выполнены (свободны блокирующие объекты и выполнены предусловия), должен получить доступ? Некоторые люди предпочитают передавать такие решения компилятору. Предпочтительнее определить по умолчанию политику FIFO, улучшающую переносимость и равнодоступность. Разработчикам приложений и в этом случае будут доступны библиотечные механизмы для изменения принятой по умолчанию политики.

Подчеркнем еще раз, что специальная семантика предусловий как условий ожидания применяется только к тому, что мы назвали предложениями сепаратных вызовов, т. е. к предложениям, включающим условия вида b.some_property , где b - это сепаратный аргумент. Несепаратное предложение, такое как i > = 0, будет иметь обычную семантику корректности, так как к нему неприменим парадокс параллельных предусловий: если клиент обеспечивает выполнение указанного условия перед вызовом, то оно будет выполнено и в момент запуска подпрограммы, а если это условие не выполнено, то никакое ожидание не приведет к изменению ситуации.




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



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