[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,
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,
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,
Aqui, fk é 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.)
Os invariantes poderiam também ser enunciados assim: no início de cada iteração,