Projeto de Algoritmos | Índice Remissivo

Prova da correção do algoritmo das distâncias

[Enunciado]  Queremos mostrar que a função distancias está correta, ou seja, que a função faz o que sua documentação promete. Para isso, é preciso mostrar que, no início da última iteração (quando a fila está vazia), o vetor dist tem a seguinte propriedade:  para cada cidade x,

1. dist[x] ≤ N;
2. se dist[x] < N então
   1. existe um caminho de comprimento dist[x] que começa em c e termina em x e
   2. todo caminho que começa em c e termina em x tem comprimento pelo menos dist[x];
3. se dist[x] == N então nenhum caminho começa em c e termina em x.

Nesses enunciados, um caminho é uma sequência de estradas em que cada estrada começa onde terminou a estrada anterior. A primeira estrada de todos os caminhos começa na cidade central c. O comprimento do caminho é o seu número de estradas.

É fácil constatar que as propriedades A e Ba valem no início da última iteração pois são invariantes, ou seja, valem no início da cada iteração, desde a primeira. Para constatar que as propriedades Bb e C valem no início da última iteração, é preciso mostrar a validade de dois outros invariantes:  no começo de cada iteração, para toda estrada que vai de uma cidade x a uma cidade y,

1. se x é preta e y é preta então dist[x]+1 ≥ dist[y] e
2. se x é preta e y é branca então x está na fila.

Nesses enunciados, uma cidade j é considerada preta se dist[j] < N e branca se dist[j] == N.  (Prove que a validade de 1 e 2 no início da última iteração implica em Bb e C.)

Os invariantes 1 e 2, por sua vez, decorrem de três outros invariantes: no início de cada iteração,

3. todas as cidades da fila são pretas,
4. dist[f_p] ≤ … ≤ dist[f_u-1] ≤ dist[f_p] + 1, e
5. dist[h] ≤ dist[f_p] para cada cidade preta h que não está na fila.

Aqui, f_k é uma abreviatura de fila[k].   (Prove que, no início de cada iteração, 3, 4 e 5 implica em 1 e 2. Depois, prove que 3, 4 e 5 valem no início de cada iteração.)

Apêndice

Os invariantes poderiam também ser enunciados assim: no início de cada iteração,

1. para cada cidade x,  se dist[x] < N então dist[x] é a distância de c a x;
2. dist[fila[0]] ≤ … ≤ dist[fila[u-1]];
3. dist[fila[u-1]] ≤ dist[fila[p]] + 1;
4. para cada índice h em 0..p-1, toda estrada que começa em fila[h] termina em algum elemento de fila[0..u-1].