Спецификация и тестирование систем с асинхронным интерфейсом



         

Алгоритм проверки корректности поведения - часть 5


Доказательство.

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

.

Предположим, что это не так. То есть

p1, p2
isin.gif P: p1
p2
p2 < p1.

Из того, что p2 < p1 следует, что дуга, помеченная p2, встречается в пути раньше, чем дуга, помеченная p1. Следовательно, к вершине, в которую ведет дуга, помеченная p2, приписано множество, содержащее p2 и не содержащее p1. Такое множество не является идеалом, то есть рассматриваемые дуги не могут принадлежать дереву возможных линеаризаций. Противоречие показывает, что наше предположение не верно и любая последовательность на пути из корня в лист является линеаризаций.

Докажем, что для любой линеаризации ( P,

) найдется путь в дереве возможных линеаризаций, помеченный последовательностью соответствующей данной линеаризации.

Для этого мы рассмотрим путь в дереве возможных линеаризаций множества P, помеченный соответствующей последовательностью элементов ( p1, p2, …, pn ), и покажем, что этот путь будет присутствовать в дереве возможных линеаризаций частично-упорядоченного множества ( P,

).

Предположим, что это не так и одна из вершин этого пути была удалена из дерева. Это могло произойти только в случае, когда данная вершина принадлежит поддереву, к корню которого приписано множество, не являющееся идеалом ( P,

). Так как рассматриваемый путь ведет из корня в лист дерева, то корень любого поддерева, содержащего вершину из данного пути, также принадлежит этому пути. Следовательно, к одной из вершин рассматриваемого пути приписано множество, не являющееся идеалом ( P,
).

Это множество состоит из элементов, приписанных к пути из корня дерева в эту вершину. Так как такой путь в дереве единственен, то он совпадает с началом пути ( p1, p2, …, pn ). Следовательно,

k: &#x007B; p1, p2, …, pk &#x007D; - не является идеалом ( P,
).


Содержание  Назад  Вперед