Korrektheitsbeweis: Tutorium 06

[Sonne34]

Hallo,

ich habe eine Frage bezüglich des 6. Tutoriums. Hier soll ein Korrektheitsbeweis über die folgende Methode geführt werden:

Code: Alles auswählen

private double cosinus (double [] [] a) {
	double skalar, cosinus;
	double [] norms = calc2norm(a);
	cosinus = 0;
	for (int i = 0; i < a[0].length-1; i ++ ) {
		for (int j = i+1; j < a[0].length; j++) {
			skalar = 0;
			for (int k = 0; k < a.length; k++) {
				skalar += (a[k] [i] * a [k] [j]);
			}
			cosinus += (skalar / norms [i] * norms [j]));
		}
	}
	return cosinus;
}				

Ich habe nun den Korrektheisbeweis geführt und mit der Lösung in den FOlien verglichen. Zu der zweiten for Schleife habe ich nun eine Frage

for (int j = i+1; j < a[0].length; j++) {

Hier steht in der Lösung auf den Folien folgendes zur Invariante:

Nach j >= 0 Iterationen enthält cosinus die Summe der
ersten j Quotienten der Sakarprodukte von i und j geteilt
durch das Produkt der Norm von i und j.

Ich hatte da: : Nach j – i – 1 Iterationen wurden für die ersten j Elemente der Winkel korrekt berechnet.

Ich wollte mal fragen ob meine Lösung auch geht? Oder ob es reicht zu schreiben nach j > = 0 Iterationen?

Vielen Dank und viele grüße

[Prof. Karsten Weihe]

Ich wollte mal fragen ob meine Lösung auch geht? Oder ob es reicht zu schreiben nach j > = 0 Iterationen?

Sie sind da auf eine grundsätzliche Problematik mit der Formulierung von vollständigen Induktionen über Schleifen gestoßen: Der Schleifenzähler - in Ihrem Fall \(j\) - sollte besser nicht der Induktionsparameter sein, das führt nur zu solchen Verwirrungen wie bei Ihnen. Besser ist es, einen separaten Induktionsparameter (nennen wir ihn \(h\)) einzuführen, der nicht der Name einer Variable im Code ist, und dann zu schreiben: "Nach \(h\geq 0\) Iterationen gilt: ..."

Im Übungsbetrieb im SS16 war uns das aufgefallen, und in der Klausur im September 2016 hatte ich diese Erkenntnis auch schon berücksichtigt und entsprechend in der Aufgabenstellung verlangt, die Formulierung der Invariante mit "Nach \(h\geq 0\) Iterationen" einzuleiten. Selbstverständlich wird das auch in Zukunft so sein.

KW