Ограничение проверки правильности
Для устранения тупиков требуется наложить ограничение на предложения предусловий и постусловий. Предположим, что разрешены подпрограммы вида:
f (x: SOME_TYPE) is require some_property (separate_attribute) do ... endгде separate_attribute - сепаратный атрибут объемлющего класса. В этом примере, кроме separate_attribute, ничто не должно быть сепаратным. Вычисление предусловия f (как части мониторинга утверждений корректности либо как условия синхронизации, если фактический аргумент, соответствующий x, является сепаратным) может вызвать блокировку, когда присоединенный объект недоступен.
Эта ситуация запрещается следующим правилом:
|
Правило аргументов утверждения Если утверждение содержит вызов функции, то любой фактический аргумент этого вызова, если он сепаратный, должен быть формальным аргументом объемлющей подпрограммы. |
Отметим, что из этого правила следует, что такое утверждение не может появиться в инварианте класса, который не является частью подпрограммы.
