Graphen (Gewichte Korrektheitsbeweis )

	Wir zeigen also
Korrektheit	Der Algorithmus von Dijkstra bestimmt die gewichteten Abstände dg(w) für alle Knoten w.
Vorüberlegungen	Auch der Algorithmus von Dijkstra realisiert eine mögliche Variante für das Durchlaufen eines Graphen. Wir haben wegen der Übersichtlichkeit diesmal keine Vorgängerknoten 'gemerkt'. Dies könnte man aber einfach (nämlich so wie in den anderen Algorithmen) ergänzen. Deshalb ist Folgendes bereits klar: Für jeden Knoten w ist dg(w) < genau dann, wenn w von v aus erreichbar ist. Für jeden Knoten w mit dg(w) < ist dg(w) die gewichtete Länge eines Weges von v nach w. Dass dg(w) wirklich kleinstmöglich ist, zeigen wir wieder mit geeigneten Assertions. Wir unterscheiden (zunächst) zwischen der berechneten Zahl dg(w) und dem tatsächlichen gewichteten Abstand ag(w) von Knoten w von v. Wir wollen also zeigen: dg(w) = ag(w) für alle von v aus erreichbaren Knoten w, und wissen bereits ag(w) ≤ dg(w) für alle von v aus erreichbaren Knoten w.
bewege die Maus über die Assertions (bewege das Fenster zuerst so, dass du das gesamte gelbe Feld siehst)
	Übrigens: Bei der Begründung von Assertion A2 ging wesentlich mit ein, dass alle Kantengewichte nicht negativ sind.