# Invariante eines Algorithmus



## Kirby.exe (6. Okt 2020)

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:


----------



## BestGoalkeeper (6. Okt 2020)

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.exe (6. Okt 2020)

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


----------



## BestGoalkeeper (6. Okt 2020)

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...


----------



## mihe7 (6. Okt 2020)

BestGoalkeeper hat gesagt.:


> 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.


Nö, schau nochmal genau hin


----------



## Kirby.exe (6. Okt 2020)

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 ?


----------



## BestGoalkeeper (6. Okt 2020)

ja


----------



## mihe7 (6. Okt 2020)

Nö


----------



## BestGoalkeeper (6. Okt 2020)

mihe7 hat gesagt.:


> Nö


----------



## mihe7 (6. Okt 2020)

Schaut Euch mal an, was die innere Schleife macht.


----------



## BestGoalkeeper (6. Okt 2020)

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 (7. Okt 2020)

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 <= i <= n` UND
`0 <= j <= n-i` gilt UND
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 <= i <= n` UND
`a_{n-i} <= a_{n-i+1} <= ... <= a_{n-1}` UND
`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.


----------



## BestGoalkeeper (7. Okt 2020)

BestGoalkeeper hat gesagt.:


> 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.


mihe7 hat gesagt.:


> der Korrektheitsbeweis steht natürlich noch aus.


Mach das mal.  Ist danach auch gefragt?


----------



## BestGoalkeeper (7. Okt 2020)

BestGoalkeeper hat gesagt.:


> und 0<=j<=i<=n.


Das muss glaube ich lauten: und 0<=j<=len(A)-i<=n. Oder man lässt das <=len(A)-i ganz weg...


----------



## Kirby.exe (7. Okt 2020)

BestGoalkeeper hat gesagt.:


> Das muss glaube ich lauten: und 0<=j<=len(A)-i<=n. Oder man lässt das <=len(A)-i ganz weg...


Ich wollte gerade sagen n = len(A) also ist ja len(A)-1 überflüssig


----------



## mihe7 (7. Okt 2020)

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.


----------



## BestGoalkeeper (7. Okt 2020)

Wo ist denn jetzt der Beweis?


----------



## mihe7 (7. Okt 2020)

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.exe (7. Okt 2020)

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


----------



## BestGoalkeeper (7. Okt 2020)

Kirby_Sike hat gesagt.:


> Also für mich ist das irgendwie alles Schwarze Magie


Ich habe schon Professoren erlebt, die die, die dies behaupteten, aus der Vorlesung geschmissen haben.


----------



## mihe7 (7. Okt 2020)

Kirby_Sike hat gesagt.:


> 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.exe (7. Okt 2020)

mihe7 hat gesagt.:


> 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


----------



## mihe7 (7. Okt 2020)

Kirby_Sike hat gesagt.:


> 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


Ja, irgendwas ganz simples, ansonsten wirst Du da ja nicht fertig.


----------



## BestGoalkeeper (7. Okt 2020)

Kirby_Sike hat gesagt.:


> 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. 









						Loop invariants can give you coding superpowers
					

A loop invariant is a simple yet powerful tool for designing, testing, modifying, documenting and proving code correct.




					yourbasic.org
				





			loop-invariants
		









						What is a loop invariant?
					

I'm reading "Introduction to Algorithm" by CLRS. In chapter 2, the authors mention "loop invariants". What is a loop invariant?




					stackoverflow.com


----------

