[Enunciado] Queremos provar os invariantes do algoritmo de Dijkstra. Se denotarmos por M o conjunto dos vértices maduros (todos estão em T), os invariantes podem ser escritos assim:
Os invariantes i a v valem no início da primeira iteração pois nessa ocasião s é o único vértice de T, o conjunto M está vazio, dist[s] ≡ 0 e dist[v] é ∞ para todo v diferente de s. Suponha agora que os invariantes valem no início de uma iteração qualquer que não a última; provaremos que os invariantes continuam valendo no fim da iteração corrente, e portanto também no início da iteração seguinte.
Começamos com uma observação preliminar. No início da iteração corrente, todos os arcos do leque de entrada de M estão relaxados, graças ao invariante iv e à ausência de custos negativos. Durante a iteração, o algoritmo altera o valor de dist[x] somente se y-x é um arco tenso. Logo, as componentes do vetor dist[] indexadas pelos vértices de M não são alterados durante a iteração.
Para mostrar que os invariantes i e ii continuam valendo no fim da iteração, basta mostrar que pa[] continuará representando uma árvore radicada e que os arcos dessa árvore serão justos.
As únicas alterações de pa[] e dist[] que ocorrem durante a iteração correspondem aos vizinhos z de y em G tais que o arco y-z está tenso no início da iteração. Como já observamos acima, tal z não pertence a M. Além disso, de acordo com o invariante v, y é folha de T. Há dois casos a considerar, conforme z esteja ou não em T. No primeiro caso, z é folha de T, graças ao invariante v. Nesse caso, o arco pa[z]-z será retirado de T e o arco y-z será acrescentado. No segundo caso, z e y-z serão acrescentados a T. Em ambos os casos, pa[] continuará representando uma árvore radicada com raiz s e dist[z] passará a ter o valor da expressão dist[y]+cyz, sendo cyz o custo do arco y-z. Assim, todos os arcos da árvore representada por pa[] serão justos. Isso prova que os invariantes i e ii continuarão valendo no fim da iteração corrente.
Seja v-w um arco de G tal que v está em M ∪ {y}. Precisamos mostrar que dist[v]+cvw ≥ dist[w] no fim da iteração corrente, sendo cvw o custo do arco v-w. Isso é certamente verdade se v ≡ y, pois todos os arcos do leque de saída de y que violavam a desigualdade têm o valor original de dist[w] substituído por dist[v]+cvw.
Considere agora o caso em que v pertence a M. Em virtude do invariante iii, dist[v]+cvw ≥ dist[w] no início da iteração. Como já observamos acima, o valor de dist[v] não é alterado durante a iteração. Ademais, nenhuma componente de dist[] aumenta durante a iteração. Portanto, a desigualdade dist[v]+cvw ≥ dist[w] permanece válida no fim da iteração.
Seja v um vértice qualquer em M ∪ {y} e z um vértice qualquer fora de M ∪ {y}. Precisamos mostrar que dist[v] ≤ dist[z] no fim da iteração corrente. Considere primeiramente o caso v ≡ y. No início da iteração temos dist[y] ≤ dist[z] em virtude da maneira como o algoritmo escolheu y. Mesmo que o valor de dist[z] seja alterado durante a iteração, seu novo valor será dist[y]+cyz. Como cyz é positivo, teremos dist[y] ≤ dist[z] no fim da iteração.
Agora considere o caso em que v está em M. Em virtude do invariante iv, dist[v] ≤ dist[z] e dist[v] ≤ dist[y] no início da iteração. Como já observamos acima, o valor de dist[v] não é alterado durante a iteração. Se o valor de dist[z] não for alterado durante a iteração, teremos dist[v] ≤ dist[z] no fim da iteração. Suponha agora que o valor de dist[z] é alterado. Então y-z é um arco e o novo valor de dist[z] será dist[y]+cyz. Como dist[v] ≤ dist[y] no início da iteração, e dist[y] não se altera, e cyz é positivo, teremos dist[v] ≤ dist[z] no fim da iteração.
Seja w um vértice de G fora de M ∪ {y}. Suponha que w pertence a T no fim da iteração. Se w não estava em T no início da iteração então é claro que w é uma folha de T no fim da iteração. Suponha agora que w estava em T no início da iteração. Então w era folha de T em virtude do invariante v. Durante a iteração, nenhum arco com ponta inicial w é acrescentado a T e portanto w continua sendo folha de T no fim da iteração (ainda que o pai de w em T possa ter sido alterado).