[Enunciado do exercício.] Queremos mostrar que no início de cada iteração do bloco de linhas 8-11 de Dijkstra valem os invariantes (i), (ii) e (iii).
Os invariantes valem no início da primeira iteração. De fato, o invariante (i) vale porque se dist[v] < ∞ então v = r e o caminho trivial (r) é quase preto e tem a propriedade f((r)) = 0 = dist[r]. O invariante (ii) vale porque não existem vértices pretos. O invariante (iii) vale porque o único caminho quase preto com origem r é o caminho trivial (r) e f((r)) = 0 = dist[r].
Suponha agora que os três invariantes valem no início de uma iteração qualquer que não a última. Provaremos a seguir que os três invariantes continuam valendo no início da próxima iteração.
Que alterações ocorrem durante a iteração? Nenhum vértice preto fica cinza e o vértice y, definido na linha 8 de Dijkstra, é o único vértice cinza que fica preto. Para descrever as alterações de componentes do vetor dist, denotaremos por dist′ o estado de dist no fim da iteração. Podemos dizer então que dist′[v] ≤ dist[v] para todo vértice v e se dist′[v] < dist[v] então yv é um arco e dist′[v] = dist[y] + f(yv).
Depois desses preparativos, podemos provar que as invariantes (i), (ii) e (iii) continuam valendo no início da próxima iteração.
Seja v um vértice tal que dist′[v] < ∞ no fim da iteração. Basta mostrar que f(D) = dist′[v] para algum caminho D de r a v que é quase preto no fim da iteração.
No começo do iteração, havia um caminho quase preto C tal que f(C) = dist[v]. Esse caminho continua quase preto no fim da iteração. Portanto, C tem as popriedades desejadas desde que tenhamos dist′[v] = dist[v].
Suponha agora que dist′[v] < dist[v]. Então v é vizinho de y e dist′[v] = dist[y] + f(yv). Como dist′[v] < ∞, temos dist[y] < ∞. Assim, o invariante (i) aplicado a y garante que existia um caminho quase preto C de r a y tal que f(C) = dist[y]. Como y fica preto no fim da iteração, C fica todo preto. Portanto, o caminho C + yv é quase preto. Ademais, f(C + yv) = f(C) + f(yv) = dist[y] + f(yv) = dist′[v].
No fim da iteração, seja v um vértice preto e B um caminho de r a v. Basta mostrar que f(B) ≥ dist′[v].
Se v ≠ y então v já era preto no começo da iteração e portanto f(B) ≥ dist[v] ≥ dist′[v]. Suponha agora que v = y e seja x o primeiro vértice de B que era cinza no início da iteração (possivelmente x = y). Seja B1 o segmento inicial de B que vai de r a x. É claro que B1 é quase preto. Pelo invariante (iii), f(B1) ≥ dist[x]. Logo, f(B) ≥ f(B1) ≥ dist(x). Graças à maneira como o algoritmo escolhe y, temos dist[x] ≥ dist[y]. Assim, f(B) ≥ dist[y] = dist[v] ≥ dist′[v].
No fim da iteração, seja v um vértice cinza e C um caminho quase preto de r a v. Basta mostrar que f(C) ≥ dist′[v].
Se C não passa por y então C era quase preto no começo da iteração e v era cinza. Pelo invariante (iii), f(C) ≥ dist[v] ≥ dist′[v], como queríamos provar.
Suponha agora que C passa por y. Então C = C1 + C2, sendo C1 o segmento inicial de C que vai de r a y e C2 o segmento final de C que vai de y a v. Como y é preto no fim da iteração e v é cinza, temos y ≠ v e portanto C2 tem pelo menos um arco. Temos duas alternativas a considerar: