Доказательство алгоритма Дейкстры построено по индукции по числу посещенных узлов.
Инвариантная гипотеза: Для каждого посещенного узла v , dist [v] считается кратчайшим расстоянием от источника до v ;и для каждого не посещаемого узла u , dist [u] предполагается самое короткое расстояние при путешествии только через посещенные узлы от источника до u .Это предположение рассматривается только в том случае, если путь существует, в противном случае расстояние устанавливается равным бесконечности.(Примечание: мы не предполагаем, что dist [u] - это фактическое кратчайшее расстояние для не посещаемых узлов)
Базовый случай - это когда существует только один посещенный узел, а именно исходный узел, в этом случаегипотеза тривиальна.
В противном случае предположим гипотезу для n-1 посещенных узлов.В этом случае мы выбираем ребро vu , где u имеет наименьшее число dist [u] из всех не посещенных узлов, а ребро vu таков, что dist [u] = dist [v] + длина [v, u] . dist [u] считается кратчайшим расстоянием от источника до u , потому что если бы был более короткий путь, и если w был первым не посещенным узлом натогда этот путь по первоначальной гипотезе dist [w]> dist [u] создает противоречие.Точно так же, если бы был более короткий путь к u без использования не посещенных узлов, и если бы последним, но одним узлом на этом пути было w , то у нас было бы dist [u] = dist [w] + length [w, u] , также противоречие.
После обработки u все равно будет верно, что для каждого невидимого узла w , dist [w] будет кратчайшим расстоянием от источникана w , используя только посещенные узлы, потому что если бы был более короткий путь, который не идет по u , мы бы нашли его ранее, и если бы был более короткий путь, используя u мы бы обновили его при обработке u .