Korrektheitsbeweis: Tutorium 06

Bei Postings zu Aufgabe Nr. x auf Blatt Nr. y lassen Sie Ihr Betreff bitte mit "y.x: " beginnen, gefolgt von einer möglichst präzisen Überschrift, danke!

Moderator: Algorithmen und Datenstrukturen

Forumsregeln
Bei Postings zu Aufgabe Nr. x auf Blatt Nr. y lassen Sie Ihr Betreff bitte mit "y.x: " beginnen, gefolgt von einer möglichst präzisen Überschrift, danke!
Sonne34
Windoof-User
Windoof-User
Beiträge: 26
Registriert: 3. Mai 2015 18:10

Korrektheitsbeweis: Tutorium 06

Beitrag von Sonne34 » 8. Apr 2017 12:10

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
Moderator
Moderator
Beiträge: 1824
Registriert: 21. Feb 2005 16:33

Re: Korrektheitsbeweis: Tutorium 06

Beitrag von Prof. Karsten Weihe » 8. Apr 2017 13:53

Sonne34 hat geschrieben: 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

Antworten

Zurück zu „AuD: Theoretische Aufgaben“