Graphen (Durchlaufen 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)