MathePrisma Logo

Graphen

Graphen

Korrektheitsbeweis

Wir zeigen also:

Korrektheit

Im Algorithmus Durchlaufen werden genau die Knoten als besucht markiert, welche mit v verbindbar sind.

Dazu verwenden wir 'Assertions' (Zusicherungen).

Definition

Eine Assertion ist eine logische Aussage, welche nach einem Schritt im Ablauf eines Algorithmus wahr ist.

Wir fügen Assertions einfach als Text jeweils an die entsprechende Stelle in die Beschreibung des Algorithmus ein.


Besonders wichtige Assertions sind die Schleifeninvarianten.

Definition

Eine Schleifeninvariante ist eine Assertion, welche vor, während und nach einer Schleife gilt.

Die entscheidende Schleife ist bei uns die 'solange'-Schleife.

bewege die Maus über die Assertions (bewege das Fenster zuerst so weit, dass du das gesamte gelbe Feld siehst)