КаталогИндекс раздела
НазадОглавлениеВперед

3. Правила доказательства

Аналогия между монитором и представлением данных была отмечена во введении. Взаимное исключение на коде монитора гарантирует, что вызовы процедур следуют друг за другом во времени, как в последовательном программировании, те же ограничения наложены на доступ к нелокальным данным. Поэтому к мониторам могут применяться те же правила доказательства, что и к представлениям данных.

Как и в представлении данных, программист может связывать инвариант g с локальными данными монитора, чтобы описать некоторое условие, которое будет истинным для этих данных до и после каждого вызова процедуры. g должен также быть истинным после инициализации данных, и перед каждой командой wait; иначе следующий вызов процедуры не будет находить локальные данные в ожидаемом состоянии.

С каждой переменной условия b программист может связывать утверждение B, описывающее условие, при котором программа, ожидающая на b, желает быть продолженной. Так как другие программы могут вызывать монитор во время ожидания, ожидающая программа должна гарантировать, что инвариант g для монитора заранее истинен. Это дает, правило для wait:

g {b.wait} g&B

Так как сигнал может приводить к немедленному возобновлению ожидающей программы, условия g&B, которые ожидаются этой программой, должны стать истинными до сигнала; и поскольку B может снова быть сделанным ложным продолженной программой, только g может предполагаться истинным впоследствии. Правило для signal такое:

g&B{b.signal}g 

Здесь проявляется приятная симметрия с правилом для wait.

Введение переменных условия делает, возможным написание мониторов, подверженных риску тупиков [7]. Избежание этого риска, как и других опасностей планирования (треш, бесконечное откладывание и т.д. [11]) - ответственность программиста. Правила, ориентированные на утверждения, не могут доказать отсутствие таких рисков; возможно, для таких доказательств лучше использовать менее формальные методы. Наконец, во многих случаях монитор операционной системы создает некоторый "виртуальный" ресурс, который используется вместо реальных ресурсов программами пользователя. Этот виртуальный ресурс - абстракция набора локальных переменных монитора. Тот, кто доказывает правильность программы, должен, следовательно, определить эту абстракцию в терминах конкретного представления, и затем выразить желаемый эффект каждой из процедуры в терминах абстракции. Это правило доказательства подробно описано в [13].


НазадОглавлениеВперед
КаталогИндекс раздела