Schleifeninvariante, Terminierung?

[ellisD]

Hallo liebe Leute,


leider habe ich Probleme meine Scheinaufgabe zu erledigen. Was ist und wie berechnet man eine Schleifeninvariante? Wozu überhaupt und wie gehe ich vor?? Gibts da irgendwie ein Schema welches ich anwenden kann um auf die Schleifeninvariante zu kommen? Ich steig da nicht durch :-(


Aufgabe 1
Zeigen Sie mit Hilfe einer geeignet gewahlten Schleifeninvariante, dass die
Methode quadrat(n) fur Parameter n >= 0 den Wert n*n berechnet:
public static int quadrat(int n) {
int q = 0;
int i = 1;
while (i <= n) {
q = q + 2 * i - 1 ;
i++;
}
return q;
}

a) Programmieren Sie eine Methode
public static double max(double[] array)
die das Maximum in einem Array ermittelt.
b) Zeigen Sie, dass Ihr Programm total korrekt ist.
c) Zeigen Sie, dass Ihr Programm terminiert.
d) Von welcher Zeitkomplexitat ist Ihr Programm (worst case, best case und
average)?

Die Methode hab ich fertig, nur wie beweise ich dass sie total korrekt ist und terminiert?

Hoffe auf schnelle Hilfe...

 

[Marcinek]

Hallo,

für die Grundlagen würde ich hier schauen:

http://ira.informatik.uni-freiburg.de/teaching/ppp-2002/Hardek-Folien.pdf

Gruß,

Martin

 

[0x7F800000]

Was ist und wie berechnet man eine Schleifeninvariante?

"Schleifeninvariante" ist ein irgendwie gearteter funktionaler Zusammenhang zwischen den Variablen, auf den die Schleife während ihrer ausführung herumwurschtet. IMHO ein völlig überflüssiges Konzept: wenn du die ganz normale Induktion verstanden hast, dann kannst du auch über Schleifen alles beweisen, ob du es jetzt "Schleifeninvariante" nennst, oder nicht. In deinem Fall wäre sowas wie "Am Anfang jedes Schleifendurchlaufs gilt [c]q = (i-1)^2[/c]" eine Schleifeninvariante, aber das ist, wie gesagt, mit einer stinknormalen Induktion zu zeigen.

Wozu überhaupt und wie gehe ich vor??

Um Algorithmen zu verstehen und ihre Korrektheit zu beweisen. Ein Kalkül, welches alles für dich automatisch löst, gibt es nicht, musst jeden einzelnen Fall anguggen, und jedes mal aufs neue irgendeine Beweisstrategie ausdenken.

Gibts da irgendwie ein Schema welches ich anwenden kann um auf die Schleifeninvariante zu kommen?

Es ist bewiesen, dass es keinen Algorithmus gibt, der eine Schleifeninvariante automatisch bestimmt.

Den beweis habe ich nicht gesehen, aber ich vermute mal, dass es mit hilfe von WHILE-Programmen irgendwie auf einen Widerspruch gegen die Unentscheidbarkeit des Halteproblems zurückgeführt wird.

 

[ellisD]

Okay, vielen Dank.. die erste Aufgabe habe ich nun mit Mühe und Not gelöst. Bitte um Verbesserungen falls was nicht stimmt ;-)

Lösung:
Schleifeninvariante : q == (i - 1)²
Vor Schleife:
i == 1 <= n + 1 (da n >=0)
q = 0 = (i - 1)² = (1 - 1)² = 0² = 0
Während Schleife:
q(neu) = q(alt) + 2 * i(alt) - 1
i(neu) = i(alt) + 1
q' = q + 2 * i - 1 = (i - 1)² * i = i² = (i' - 1)²
q(neu) = (i(neu) - 1)²
Nach Schleife:
┐ ( i <= n) = i > n
INV:
i <= n + 1 = i == n + 1
q = (i - 1)² ∩ i == n + 1 ==> q = n²


Bei 7b bin ich allerdings noch überfordert und erarbeite mir das gerade. Wenn ichs weiß, poste ich es ;-)

 

[ellisD]

public double[] array = new array[20];	
	
	public static double max(double[] array) {
		
		double max = 0;
			
			for (int i = 0; i < array.length; i++){
				if ( array [i] > max) {
					max = array[i];
				}
			}
		return max;	
	}

Keine Ahnung wie ich hier totale Korrektheit beweise...kann mir da jemand helfen?

 

[0x7F800000]

Keine Ahnung wie ich hier totale Korrektheit beweise...kann mir da jemand helfen?

Hier kann dir keiner helfen, weil der Algo falsch ist. Teste es mal mit {-1}.

Tipp: [c]Double.NEGATIVE_INFITITY[/c] bzw. [c]1 / -0d[/c]

 

[Marcinek]

Hallo,

die Schleifeninvariante ist ein Zustand, der vor und nach der Ausführung genau so besteht.

Hier ist es das Array. Den vor und nach der Methode bleibt dieses unberührt.

Es gilt

Array P Array. Siehe die Folien, die ich gepostet hbe.

Um zu Berweisen, dass diese Algo terminiert, muss es eine Abbruchbedingung geben. Hier ist es trivial, den die Schleife läuft maximal über die Anzahl der ELemente im Array, und diese kann nur berschränkt sein im mathematischen Sinne

Um die totale korrektheit zu beweisen, muss man beweisen, dass sich in max zu jeder Zeit der Wert aus dem Array befindet, der am größten ist.

Da wir hier max nur dann ändern, wenn ein größeres Element gefunden wird, ist es genau das maximum. q.e.d.

Das bezieht sich auf die max(Array) Methode.

Gruß,
Martin

 

[Marcinek]

Hier kann dir keiner helfen, weil der Algo falsch ist. Teste es mal mit {-1}.

Tipp: [c]Double.NEGATIVE_INFITITY[/c] bzw. [c]1 / -0d[/c]

Die Methode akzeptiert n >= 0 und daher muss das hier nicht betrachtet werden?

 

[0x7F800000]

Die Methode akzeptiert n >= 0 und daher muss das hier nicht betrachtet werden?

...?

a) Programmieren Sie eine Methode
public static double max(double[] array)
die das Maximum in einem Array ermittelt.

Wo steht hier irgendwas von irgendwelchen Einschränkungen >= 0?

Was deinen Vorschlag mit dem Array als Schleifeninvariante angeht, bezweifle ich, dass das der Sinn der Sache gewesen ist. Okay, ins array wird nichts geschrieben, also ändert sich da nichts, korrekt. Und 2+2 bleibt stets 4. Auch korrekt. Jede Wahre Aussage bleibt wahr. Alles korrekt, aber genauso unnütz.

So etwas wie "Bei jedem Durchlauf gilt [c]max = Math.max{a_0, ... , a_i}[/c]" würde schon wesentlich mehr sinn machen.

 

[Marcinek]

Nein, das ist ein wesentlicher, in diesem Beispiel aber primitiver, Bestandteil der Invariante. (Siehe Folien)


Und wie kann ich eine Funktion "max" als Invariante (oder als Bestandteil des Beweises) nehmen, wenn ich gerade dabei bin die totale Korrektheit der Methode max beweisen?

So etwas wie "Bei jedem Durchlauf gilt max = Math.max{a_0, ... , a_i} " würde schon wesentlich mehr sinn machen.

Natürlich macht das mehr Sinn, aber wie kann man das Beweisen ist die Frage?

Die {-1} von dir angesprochen, dachte ich, dass es für die andere Methode mit dem quadrieren gilt.

In dem Forum gibt es noch ein Thread zu diesem Thema, da ist max init auf 1. Element des Arrays, da würde es besser aussehen mit der -1

 

[0x7F800000]

Und wie kann ich eine Funktion "max" als Invariante (oder als Bestandteil des Beweises) nehmen, wenn ich gerade dabei bin die totale Korrektheit der Methode max beweisen?

Missverständnis: das erste [c]max[/c] war die zurückgegebene lokale variable, [c]Math.max[/c] soll die mathematische Maximums-Funktion sein. Von der zu untersuchenden [c]max[/c]-Methode war in beiden Fällen nicht die Rede.

 

[Marcinek]

Aber wenn du eine Funktion, wie max beweisen möchtest, kannst du dich nicht auf eine Funktion max stützen. Das ist nicht sinn der Übung.

Und die betrachtung hier im Thread ist Sprachen unabhängig.

 

[0x7F800000]

Aber wenn du eine Funktion, wie max beweisen möchtest, kannst du dich nicht auf eine Funktion max stützen.

Ich hab's doch gesagt: es gibt hier zwei verschiedene Funktionen [c]max[/c]: eine ist die mathematische Funktion [c]max[/c], das ist ein völlig von der Implementierung unabhängiges Objekt, das frei im Raum herumschwebt, und keinerlei Korrektheitsbeweise erfordert, nennen wir es [c]MATH_MAX[/c]. Auf der anderen Seite gibt es die Implementierung einer methode [c]max[/c] die mit irgendwelchen Schleifen auf Arrays rumwurschtet, nennen wir es [c]MY_MAX[/c]. Die Aufgabe besteht darin, nachzuweisen, dass [c]MY_MAX = MATH_MAX[/c] gilt, dass die angegebene Methode also tatsächlich das Maximum ausrechnet. Bei dem Beweis der Korrektheit des Programms [c]MY_MAX[/c] darf man selbstverständlich alle möglichen mathematischen Funktionen wie etwa [c]+[/c], [c]cos[/c], [c]gamma[/c] und eben [c]MATH_MAX[/c] verwenden, ansonsten könnte man nicht mal die Behauptung formulieren, wenn es [c]MATH_MAX[/c] nicht gäbe. Dass die Variable [c]max[/c] auch genauso heißt, ist einfach ein notationstechnisches Unglück. Im übrigen dürfte man in dem Beweis der Korrektheit von [c]MY_MAX[/c] auch [c]MY_MAX[/c] selbst verwenden, vorausgesetz man ruft es nur mit argumenten auf, für die die korrektheit schon bewiesen ist.