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

Ограничение проверки правильности


Для устранения тупиков требуется наложить ограничение на предложения предусловий и постусловий. Предположим, что разрешены подпрограммы вида:

f (x: SOME_TYPE) is require some_property (separate_attribute) do ... end

где separate_attribute - сепаратный атрибут объемлющего класса. В этом примере, кроме separate_attribute, ничто не должно быть сепаратным. Вычисление предусловия f (как части мониторинга утверждений корректности либо как условия синхронизации, если фактический аргумент, соответствующий x, является сепаратным) может вызвать блокировку, когда присоединенный объект недоступен.

Эта ситуация запрещается следующим правилом:

Правило аргументов утверждения

Если утверждение содержит вызов функции, то любой фактический аргумент этого вызова, если он сепаратный, должен быть формальным аргументом объемлющей подпрограммы.

Отметим, что из этого правила следует, что такое утверждение не может появиться в инварианте класса, который не является частью подпрограммы.



Содержание раздела