Выполнение алгоритма заканчивается когда нет больше сообщений в любом канале. Эти конфигурации не терминальны для всей системы так как вычисления в системе могут продолжится позже, начавшись отказом или восстановлением канала (на которые алгоритм должен среагировать). Мы пошлем сообщение конфигурационной стабильности, и определим предикат stable как
stable = "u, w : up(u, w) Þ Qwu не содержит сообщений <mydist,., .>.
Это предполагает что переменные Neighu корректно отражают существующие рабочие коммуникационные каналы, т.е., что (1) существует изначально. Для доказательства инвариантности утверждений мы должны рассмотреть три типа переходов.
(1) Получение сообщения <mydist, .,.> . Первое выполнение результирующего кодового фрагмента, как принято, выполняется автоматически и рассматривается отдельным переходом. Обратите внимание что в данном переходе принимается сообщение и возможно множество сообщений отправляется
(2) Отказ канала и обработка сообщения < fail. . > узлами на обоих концах канала.
(3) Восстановление канала и обработка сообщения <repair. . > двумя соединенными узлами.
Лемма 4.14 Для всех uo, wo, и vo, P(uo, wo, vo) –– инвариант.
Доказательство. Изначально, т.e., после выполнения инициализационной процедуры каждым узлом, (1) содержится предположением. Если изначально мы имеем Øup(uo, wo), (2) и (3) тривиально содержатся. Если изначально мы имеем up(uo, wo), тогда ndisuo[wo, vo] = N. Если wo = vo то Dwo[wo] = 0 но сообщение < mydist, vo, 0> в Qw0u0, таким образом (2) и (3) истинны. Если wo¹ vo то Dw0[vo]=N и нет сообщений в очереди, что также говорит что (2) и (3) содержаться. Мы рассмотрим три типа констатированных переходов упомянутых выше.
Тип (1). Предположим что u получает сообщение <mydist,v,d> от w. Следовательно нет топологических изменений и нет изменений в множестве Neigh , следовательно (1) остается истинно. Если v¹vo то это сообщение не меняет ничего в P(uo, wo, vo). Если v = vo, u =uo, и w=wo значение ndisu,[wo, vo] может изменится. Однако, если сообщение < mydist, vo, .> остается в канале значение этого сообщения продолжает удовлетворять (2), так как (2) в сохранности то и (3) также потому что посылка ложна. Если полученное сообщение было последним этого типа в канале то d = Dw0[vo] по (2), которое подразумевает что заключение (3) становится истинным и (3) в сохранности. Посылка (2) становится ложной, таким образом (2) в сохранности. Если v = vo, u = wo (и uo сосед u) заключение (2) или (3) может быть ложно если значение Dw0[vo] изменилось в следствие выполнения Recompute(v) в wo. В этом случае, однако, сообщение < mydist, vo, . > с новым значением посылается к uo, которое подразумевает что посылка (3) нарушена, и заключение (2) становится истинным, таким образом (2) и (3) сохранены. Это происходит и в случае когда сообщение < mydist, vo, . > добавляется в Qw0u0, и это всегда удовлетворяет d = Dw0[vo]. Если v = vo и u¹uo, wo ничего не изменяет в P(uo, wo, vo).
Тип (2). Предположим что канал uw отказал. Если u = uoи w = wo этот отказ нарушил посылку (2) и (3) таким образом эти правила сохранены. (1) в безопасности потому что wo удалился из Neighu0 и обратно. Нечто произойдет если u = wo и w = uo. Если u = wo но w¹ uo заключение (2) или (3) может быть нарушено так как значение Dw0 [vo] изменилось. В этом случае пересылка сообщения < mydist, vo, . > узлом wo опять нарушит посылку (3) и сделает заключение (2) истинным, следовательно (2) и (3) в безопасности. Во всех других случаях нет изменений в P(uo, wo, vo).
Тип (3). Предположим добавление канала uw. Если u = uo и w = wo то up(vo,wo) истинно, но добавлением wo в Neighu0 (и обратно) это защищает(1). Посылка < mydist, vo, Dw0 [vo]> узлом wo делает заключение (2) истинным и посылку (3) ложной, таким образом P(uo, wo, vo) обезопасен. Во всех других случаях нет изменений в P(uo, wo, vo).
Лемма 4.15 Для каждого uq и vo, L(uo, vo) –инвариант.
Доказательство. Изначально Du0[uo] = 0 и Nbu[uo] = local. Для vo¹uo , изначально ndisu[w, vo] = N для всех w Î Neighu, и Du0[vo] = N и Nbu0[vo] = udef.
Тип (1). Положим что u получил сообщение < mydist, v,d> от w. Если u¹ uo или v¹ vo нет переменных упомянутых изменениях L(uo, vo) . Если u = uo и v = vo значение ndisu[w, vo] меняется, но Du0 [vo] и Nbu0[vo] перевычисляется точно так как удовлетворяется L(vo, vo).
Тип (2). Положим что канал uw отказал. Если u = uo или w = uo то Neighu0 изменился, но опять Du0[vo] и Nbu0[vo] перевычисляются точно так как удовлетворяется L(uo, vo).
Тип (3). Положим что добавлен канал uw . Если u = uo то изменилсяNeighu0 добавлением w, но так как u устанавливает ndisu0[w, vo] в N это сохраняет L(uo, vo).
4.3.2 Корректность алгоритма Netchange
Должны быть доказаны два требования корректности.
Теорема 4.16 Когда достигнута стабильная конфигурация, таблицы Nbu[v] удовлетворяют :
(1) если u = v то Nbu[v] = local;
(2) если путь от u до v¹ u существует то Nbu[v] = w, где w первый сосед u на кратчайшем пути от u до v;
(3) если нет путь от u до v не существует то Nbu[v] = udef.
Доказательство. Когда алгоритм прекращает работу, предикат stable добавляется к P(u,w,v) для всех u, v, и w, и это подразумевает что для всех u, v, и w
up(u, w) Þ ndisu[w, v] = Dw[v]. (4.2)
Применив также L(u, v) для всех u и v мы получим
ì0 если u ¹ v
Du [v] = í 1+ min Dw[v] если u¹ v Ù$w Î Neighu: Dw[v] < N -1
îN w ÎNeigh u если u¹v Ù"w Î Neighu: Dw[v]³ N -1
(4.3)
которого достаточно для доказательства что Du[v] = d(u, v) если u и v в некотором связном компоненте сети, и Du[v] = N если u и v в различных связных компонентах.
Во-первых покажем индукцией по d{u, v) что если u и v в некотором связном компоненте то Du[v]£ d(u, v).
Случай d(u, v) = 0: подразумевает u = v и следовательно Du[v] = 0.
Случай d(u, v) = k +1: это подразумевает что существует узел w Î Neighuс d(w, v) = k. По индукции Du[v] £ k, которое по (4.3) подразумевает что Du[v] £ k + 1.
Теперь покажем индуктивно по Du[v] что если Du[v] < N то существует путь между u и v и d(u, v) £ Du[v].
Случай Du[v] = 0: Формула (4.3) подразумевает что Du[v] = 0 только для u = v, что дает пустой путь между u и v, и d(u, v) = 0.
Случай Du[v] = k +1 < N : Формула (4.3) подразумевает что существует узел w Î Neighu с Dw[v] = k. По индукции существует путь между w и v и d(w, v) £ k, что подразумевает существование пути между u и v и d(u, v) < k+ 1.
Следовательно что если u и v в некотором связном компоненте то Du[v] = d(u, v), иначе Du[v] = N. Это, Формула (4.2), и "u,v : L(u, v) и доказывает теорему о Nbu[v]. []
Докажем что стабильная ситуация в конечном счете достигается если топологические изменения прекращаются, норм-функция в отношении stable определена. Определим, для конфигурации алгоритма g,
ti = (число сообщений <mydist, .,i>) +
(число упорядоченных пар u, v таких что Du[v] = i)
и функцию f
f(g) = (to, t1,..., tN)
f(g) кортеж из (N + l) натуральных чисел, в некотором лексиграфическом порядке (обозначенном £l) . напомним что (N, £l) хорошо-обоснованное множество (Упражнение 2.5).
Лемма 4.17 Обработка сообщения < mydist,.,. > уменьшает f.
Доказательство. Пусть узел u с Du[v] = d1 получил сообщение < mydist, v, d2> , и после перевычислил новое значение Du[v] – d. Алгоритм подразумевает что d < di + 1.
Случай d < d1: Пусть d = d1 + 1 что подразумевает что td2 уменьшилось на 1 (и td1 следовательно), и только td с d > d1 увеличилось. Это подразумевает что значение f уменьшилось.
Случай d = d1: Не новое сообщение < mydist, ., .> посланное u, и влияет только на f так что td2 уменьшилось на 1, т.о. значение f уменьшилось.