Invariante eines Algorithmus

Kirby_Sike

Kirby_Sike

Top Contributor
Also das ist das letzte Thema wo es noch hackt, bzgl. Klausur xD Wir sollen Korrektheitsbeweise für "Algorithmen" führen können.

Diese bestehen ja aus Wohldefiniertheit, Termination, Korrektes Ergebnis nach Termination. Die Wohldefiniertheit und die Termination habe ich verstanden, jedoch verwirrt mich der letzte Punkt. Ich verstehe absolut nicht wie ich an diese Teilaufgabe herangehe...xD Was ist eine Invariante überhaupt, sprich welche merkmale hat eine Invariante.

Das einzige was ich dazu im Skript gefunden habe sind drei "Schritte":
- Die Invariante muss vor dem ersten Durchlauf gelten
- Wenn die Invariante vor dem ersten Durchlauf gilt, so gilt sie auch danach
- Die Invariante muss nach terminierung das korrekte Ergebnis liefern

Vielleicht weiß ja einer von euch wie das funktioniert xD

Hier mal eine Übungsaufgabe an der ich sitze:

exercise1.PNG
 
B

BestGoalkeeper

Bekanntes Mitglied
Die Schleifeninvariante lautet: A_0 <= A_1 <= A_2 <= ... <= A_i gilt für 0 <= i <= len(A)-1. Also für 0 bis i-1 gilt, das Array A ist aufsteigend sortiert. Die Schleifeninvariante gilt vor, nach, während der Schleife. Nach der Schleife gilt i=len(A)-1 - somit ist das ganze Array A sortiert.

Die Schleifeninvariante kann schrittweise entwickelt werden oder durch genaues Hinsehen.
 
Kirby_Sike

Kirby_Sike

Top Contributor
Also ist die Schleifeninvariante ein Mix zwischen Algorithmus und bedingung der Schleife richtig?
 
B

BestGoalkeeper

Bekanntes Mitglied
Nein, die Schleifeninvariante ist eine mathematische Beschreibung einer Bedingung, die vor, nach und während der Schleife gilt und die im Idealfall angibt, was der Algorithmus tut/berechnet.
Sieh dir mal das wp-Kalkül oder Hoare-Kalkül an...
 
Kirby_Sike

Kirby_Sike

Top Contributor
Die Schleifeninvariante lautet: A_0 <= A_1 <= A_2 <= ... <= A_i gilt für 0 <= j<= len(A)-1. Also für 0 bis j-1 gilt, das Array A ist aufsteigend sortiert.

oder @mihe7 ?
 
B

BestGoalkeeper

Bekanntes Mitglied
Ups ja hast recht...
Die Schleifeninvariante lautet: A_n >= A_(n-1) >= A_(n-2) >= ... >= A_(n-i), wenn n=len(A)-1 (und 0<=i<=n). Also ist das Array A von (n-i) bis n aufsteigend sortiert.
 
mihe7

mihe7

Top Contributor
Mal ein Vorschlag. Sei n := A.length. Ich schreibe a_g statt A[g] - ist hier im Editor einfacher.

In der inneren Schleife wird das "bislang" größte Element jeweils nach rechts geschoben. Die Invariante I der inneren Schleife ist:
  1. 1 <= i <= n UND
  2. 0 <= j <= n-i gilt UND
  3. kein Element links von j ist größer als das Element an Position j.
Also ist I nichts anderes als 1 <= i <=n UND 0 <= j <= n-i UND a_j = max{a_0, ... a_j}.

Die Schleifenbedingung B ist j < n-i. Die Schleife terminiert, wenn !B gilt.

Nach dem Terminieren der Schleife gilt also I und !B, also (1 <= i <= n UND 0 <= j <= n-i UND a_j = max{a_0, ..., a_j}) UND (j >= n-i). Aus 0 <= j <= n-i UND j >= n-i folgt j=n-i und damit a_{n-i} = max {a_0, ..., a_{n-i}}, was zugleich die Nachbedingung der Schleife darstellt. Als Vorbedingung könnte man 1 <= i <= n formulieren.

Für die innere Schleife haben wir also Vorbedingung, Invariante und Nachbedingung, der Korrektheitsbeweis steht natürlich noch aus.

Bei der äußeren Schleife gilt im Prinzip die Idee, dass alle Elemente ab n-i aufsteigend sortiert sind. Das alleine reicht aber noch nicht, es muss sich dabei auch um die größten Elemente handeln, also
  1. 1 <= i <= n UND
  2. a_{n-i} <= a_{n-i+1} <= ... <= a_{n-1} UND
  3. a_{n-i} = max {a_0, ..., a_{n-i}}
Die Schleifenbedingung ist i < n, die Schleife terminiert, wenn i >= n gilt. Zusammen mit der Invariante folgt aus 1 <= i <= n UND i >= n zunächst i = n und damit a_0 <= a_1 <= ... <= a_{n-1} als Nachbedingung der äußeren Schleife. Korrektheitsbeweis steht auch hier noch aus.
 
B

BestGoalkeeper

Bekanntes Mitglied
Die Schleifeninvariante lautet: A_n >= A_(n-1) >= A_(n-2) >= ... >= A_(n-i), wenn n=len(A)-1 (und 0<=i<=n). Also ist das Array A von (n-i) bis n aufsteigend sortiert.
Hier nochmal in mihe7s Schreibweise ((x) kann schnell mit einem Tupel oder was Anderem verwechselt werden...):
A_{n-i} <= ... <= A_{n-1} <= A_{n}, wenn n=len(A)-1 und 0<=i<=n. (Man soll ja Zeichen sparen...)
Invariante der inneren Schleife:
max{A_{0},...,A{j-1}} <= A{j} <= A{j+1} <= ... <= A{n}, wenn n=len(A)-1 und 0<=j<=i<=n. Also, das größte Element des noch unsortierten, vorderen Bereichs ist kleinergleich des ersten Elements des bereits sortierten, hinteren Bereichs.
der Korrektheitsbeweis steht natürlich noch aus.
Mach das mal. ;) Ist danach auch gefragt?
 
mihe7

mihe7

Top Contributor
Mal für die innere Schleife, ausführlich: wir nehmen an, dass am Beginn einer Iteration die Invariante gilt und zeigen, dass diese beim Übergang auf die nächste Iteration immer noch Gültigkeit besitzt.

Wird der Schleifenrumpf betreten, gilt die Schleifenbedingung und wir nehmen an, dass die Invariante erfüllt ist, es gilt also die Invariante 1 <= i <= n UND 0 <= j <= n-i UND a_j = max{a_0, ..., a_j} und die Bedingung j < n-i.

Zu zeigen ist, dass die Invariante nach einer Iteration ebenfalls gilt. Am Ende der Iteration wird j um 1 erhöht, so dass unmittelbar vor der Erhöhung 1 <= i <= n UND 0 <= j+1 <= n-i UND a_{j+1} = max{a_0, ..., a_{j+1}} gelten müsste. Wegen der Schleifenbedingung j < n-i gelten die ersten beiden Ausdrücke in jedem Fall, so dass nur noch der letzte interessiert.

Der Ausdruck ist wahr, wenn die Bedingung im if-Statement nicht erfüllt war. Erster Fall erledigt :)

Schauen wir uns an, was im then-Zweig passiert: a_{j+1} := temp -> ok, noch nicht wirklich brauchbar. a_j := a_{j+1}, ok und temp := a_j, also werden a_j und a_{j+1} vertauscht. Dann gilt a_j = max{a_0, ..., a_{j+1}} und damit erst recht a_j = max{a_0, ..., a_j}, womit die Invariante ebenfalls erfüllt ist.
 
mihe7

mihe7

Top Contributor
OK, da in jeder Iteration j um 1 erhöht wird, j bei 0 beginnt, wird die Schleifenbedingung irgendwann nicht mehr erfüllt und die Schleife terminiert. Dann gilt I UND !B (s. oben) -> a_{n-i} = max {a_0, ..., a_{n-i}} gilt.
 
Kirby_Sike

Kirby_Sike

Top Contributor
Also für mich ist das irgendwie alles Schwarze Magie xD ich werde einfach den anderen Teil des Korrektheitsbeweises bei der Klausur hinschrieben und hierbei educated guessing machen
 
mihe7

mihe7

Top Contributor
Also für mich ist das irgendwie alles Schwarze Magie xD ich werde einfach den anderen Teil des Korrektheitsbeweises bei der Klausur hinschrieben und hierbei educated guessing machen
Ich kann mir nicht vorstellen, dass ihr in der Klausur wirklich einen Korrektheitsbeweis machen müsst - außer einen, der vielleicht schon mal drankam. Die Invarianten sind teilweise so besch... zu finden, da wäre die ganze Klausur rum.
 
Kirby_Sike

Kirby_Sike

Top Contributor
Ich kann mir nicht vorstellen, dass ihr in der Klausur wirklich einen Korrektheitsbeweis machen müsst - außer einen, der vielleicht schon mal drankam. Die Invarianten sind teilweise so besch... zu finden, da wäre die ganze Klausur rum.
Also in der Probeklausur war der Bubblesort drinne und angeblich kommt in der richtigen Klausur dann irgendwas „simples“ wie Maximum finden oder so idk xD ich werde da mir da schon irgendwas aus dem Ärmel ziehen xD
 
B

BestGoalkeeper

Bekanntes Mitglied
Also in der Probeklausur war der Bubblesort drinne und angeblich kommt in der richtigen Klausur dann irgendwas „simples“ wie Maximum finden oder so idk xD ich werde da mir da schon irgendwas aus dem Ärmel ziehen xD
Es kommt darauf an, wie umfangreich du die Invariante schreibst. Es sollte eigentlich genug Zeit für die Aufgaben da sein. Aber ich gebs zu, mir fallen diese Invarianten sofort ein, aber das ist nicht bei jedem so. Du solltest aber keinesfalls Angst vor der Klausur aufbauen... Schaffste schon. ;)

 
Anzeige

Neue Themen


Oben