- - - - CENAPAD-MGCO

A seguir: Conclusões Acima: O Algoritmo de Naimi-Trehel Anterior: Progresso

Um Request visita um número finito de sítios

Para provar que um Request não pode visitar um número ilimitado de sítios, vamos demonstrar o seguinte invariante:

• A7 $\equiv$ if [i] = $v_{1}v_{2}\ldots v_{m}$,then for $j, k \in [1\ldots m]$, $v_{j} \neq$ i, and $j \neq k \Longrightarrow v_{j} \neq v_{k}$.
• Em outras palavras, todos os elementos em [i] são distintos, e seu comprimento não pode crescer indefinidamente.

A7 não é indutivo, e precisamos reforçá-lo com o seguinte predicado:

$$A8 = j \in \ensuremath{ {\mathbf V} } [i] \Longrightarrow j \ensuremath{ \ensuremath{\rightarrow} ^{+}} i$$

onde $j \ensuremath{ \ensuremath{\rightarrow} ^{+}} i$ significa que existe uma rota de j para i de comprimento maior ou igual a 1 no grafo .

Como para todo i $\ensuremath{ {\mathbf V} } [i]$ é inicialmente vazio, A8 é válido inicialmente. Precisamos agora varrer todas as regras do algoritmo, demonstrando que se A8 for válido antes da execução da regra, A8 será válido também após a sua execução.

A8 corre o risco de ser invalidado por regras que modifiquem o valor de algum $\ensuremath{ {\mathbf V} } [i]$ ou que modifiquem o grafo ${\cal D}$. Portanto, devemos repetir a demonstração do Teorema 1, considerando as alterações em VV e nas relações do tipo $u \ensuremath{ \ensuremath{\rightarrow} ^{+}} v$.