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


Правила обоснования корректности: разоблачение предателей


Так как для сепаратных и несепаратных объектов семантика вызовов различна, то важно гарантировать, что несепаратная сущность (объявленная как x: T для несепаратного T) никогда не будет присоединена к сепаратному объекту. В противном случае, вызов x.f (a) был бы неверно понят - в том числе и компилятором - как синхронный, в то время как присоединенный объект, на самом деле, является сепаратным и требует асинхронной обработки. Такая ссылка, ошибочно объявленная несепаратной, но хранящая верность другой стороне, будет называться ссылкой-предателем (traitor). Нам нужно простое правило обоснования корректности, чтобы гарантировать отсутствие предателей в ПО, а именно, что каждый представитель или лоббист сепаратной стороны надлежащим образом зарегистрирован как таковой соответствующими властями.

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

Правило (1) корректности сепаратности

Если источник присоединения (в инструкции присваивания или при передаче аргументов) является сепаратным, то его целевая сущность также должна быть сепаратной.

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

Отметим, что синтаксически x является сущностью, а y может быть произвольным выражением. Поэтому нам следует определить понятие "сепаратного выражения". Простое выражение - это сущность; более сложные выражения являются вызовами функций (напомним, в частности, что инфиксное выражение вида a + b формально рассматривается как вызов: нечто вроде a.plus (b)). Отсюда сразу получаем определение: выражение является сепаратным, если оно является сепаратной сущностью или сепаратным вызовом.

<


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



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