[?]Invariante

Doltsche

Hallo zusammen

Ich bin gerade das Buch Intensivkurs C++ am lesen und bin dabei auf folgenden, mir rätselhaft kommentierten Code gestossen:

// Invariante: Wir haben z Zeilen geschrieben

	int z = 0;
	// Nullsetzen von z macht die Intvariante wahr

        while(z != zeilen)
	{
		//die Invariante ist hier wahr

		// eine Ausgabenzeile schreiben
		// macht die Invariante falsch
		cout << "zeile" << endl;

		// z inkrementieren macht die Invariante wahr
		z++;
	}
	// wir schliessen, die Invariante ist hier wahr

(gleiche Absätze und Formatierung wie im Buch)

Insbesondere das hier irritiert mich:

// eine Ausgabenzeile schreiben
// macht die Invariante falsch
cout << "zeile" << endl;

Für mich stellt sich da jetzt etwas die Frage, seit wann eine Stringausgabe eine Schleife beeinflusst... .

Auch der letzte Kommentar, dass die Invariante nach dem Schliessen wahr sein soll. Das ist ja komplett unlogisch. Die while-Schleife wird ja erst dann beendet, wenn die Bedingung nicht mehr zutrifft, also falsch ist.

Ich hoffe ihr könnt mir da weiterhelfen.
Vielen Dank schonmal im Voraus.

MfG Samuel

Dravere

Eine Invariante ist immer ein Zustand, welcher man über mehrere Codezeilen hinweg prüfen kann. Die Invariante muss vor und danach korrekt sein, damit der Algorithmus auch korrekt ist. Im Code selber darf sie falsch sein.

Die Invariante hier ist also, dass wir z Zeilen geschrieben haben. Wenn wir starten trifft dies zu, da z 0 ist. Wenn wir eine Zeile rausgeschrieben haben, trifft die Invariante nicht mehr zu, da wir tatsächlich z + 1 Zeilen rausgeschrieben haben. Deshalb ist die Invariante wieder richtig, wenn wir z um 1 erhöhen.

Daraus kann man schliesslich, dass am Anfang und Ende der Schleife die Invariante immer richtig ist, wodurch die Invariante auch nach der Schleife korrekt ist.

http://de.wikipedia.org/wiki/Invariante_(Informatik)
http://de.wikipedia.org/wiki/Design_By_Contract

Damit solltest du allenfalls auch noch genügend zusätzliche Stichwörter haben. Wenn es aber immer noch unklar ist, frag ruhig nochmals genauer nach.

Grüssli