T2: Beispiel 3

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!
Hallo
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 162
Registriert: 22. Apr 2015 19:03

T2: Beispiel 3

Beitrag von Hallo » 10. Sep 2016 18:13

Hi,

Ich habe mir Theorie 2 bspl 3 ausgesucht und dazu den Korrektheitsbeweis mal durchgeführt. Würde mich auf Feedback freuen :!: :!:

Input:
Ein Aufsteigen sortiertes Array nicht null sein darf. Ein integer Element Z.

Wohldefiniertheit:
Es gibt keine Instruktonen, die auf null zugreifen, somit treten keine NullPointerException auf. Es gibt keine Divisionen durch 0, und somit keine ArithmeticException. Ein Zugriff auf nicht existierende Arraykomponente kommt auch nicht vor und somit kein IndexOutOfBoundsException.

Terminierung:
Nach endlich vielen Rekursionsschritten Terminiert der Algorithmus falls der gesuchte Element x im Array gefunden wurde, oder falls die Variablen die für den Suchintervall links und rechts( l=i und r=j) auf der gleich Position im Array stehen.

Invariante = Induktionsbehauptung:
Unmittelbar nach einem rekursiven Schritt gilt, das l die Linke grenze des Suchintervalls bestimmt, r die Rechte und m genau auf der Mitte dieses Suchintervalls initialisiert wird, also m = (l+r) /2.

Induktionsanfang: (Funktioniert bei mir halt noch nicht so gut..)
****Ich weiss, das ich hier durch die zwei Rekursionsanker die Erfüllung der Invariante klären soll, ich weiß nicht genau wie..ich versuche es aber*****

Vor dem ersten rekursiven Schritt wird l mit 0 initialisiert und r mit array.length. Somit gilt auch, das m auf die Mitte des Intervalls (l+r) initialiert wird. Steht m auf der Position des gesuchten Element, wird m zurückgegeben. Stehen l und r auf der gleichen Position im Array, so besitzt das Array nur ein Element und man ist mit der Suche fertig.


Induktionsschritt :

Nach Induktionsvoraussetzung gilt, dass falls das Element im Array vorhanden ist, so ist es zwischen den zwei Grenzen l und r. In diesem rekursiven Schritt passiert nun, das falls der Wert auf dem die Variable m steht kleiner als den gesuchten Wert ist, ruft sich die Methode rekursiv wieder auf mit l = m+1, also die erste Hälfte des Arrays wird vernachlässigt. Falls der Wert auf dem m zugreift größer als den gesuchten Element ist, ruft sich die Methode wieder auf mit l-1 als linke Grenze des Suchintervalls.

Korrektheit:

Für den aller ersten Rekursionschritt ruft sich die Methode nochmal auf, mit den neugesetzten Parameter und liefert das Korrekte Ergebnis nach endlich viele Schritte.

Prof. Karsten Weihe
Moderator
Moderator
Beiträge: 1824
Registriert: 21. Feb 2005 16:33

Re: T2: Beispiel 3

Beitrag von Prof. Karsten Weihe » 11. Sep 2016 06:42

Hallo hat geschrieben: Wohldefiniertheit:
Es gibt keine Instruktonen, die auf null zugreifen
könnten,
Hallo hat geschrieben: somit treten keine NullPointerException auf.
Hallo hat geschrieben: Es gibt keine Divisionen durch 0, und somit keine ArithmeticException.
ArithmeticException kann auch andere Ursachen haben.
Hallo hat geschrieben: Terminierung:
Nach endlich vielen Rekursionsschritten Terminiert der Algorithmus falls der gesuchte Element x im Array gefunden wurde, oder falls die Variablen die für den Suchintervall links und rechts( l=i und r=j) auf der gleich Position im Array stehen.
Die Terminierung begründet sich immer durch die Variante. Diese sollte besser explizit formuliert und in die Begründung der Terminierung geeignet integriert werden, damit die Zusammenhänge dem Leser klar werden.
Hallo hat geschrieben: Invariante = Induktionsbehauptung:
Unmittelbar nach einem rekursiven Schritt gilt, das l die Linke grenze des Suchintervalls bestimmt, r die Rechte und m genau auf der Mitte dieses Suchintervalls initialisiert wird, also m = (l+r) /2.
Aus Ihrer Formulierung wird man wohl nicht Korrektheit des Outputs schließen können.

Ich hatte die Invariante so formuliert: Falls der gesuchte Wert überhaupt im Array ist, dann ist er im Intervall l+1..r-1.

Versuchen Sie es vielleicht damit noch einmal.

KW

Hallo
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 162
Registriert: 22. Apr 2015 19:03

Re: T2: Beispiel 3

Beitrag von Hallo » 11. Sep 2016 11:23

Ich habe hier es nochmal aufgeschrieben.
Um ehrlich zu sein, bei der Gesamtkorrektheit sowie den Induktionsschritt ist mir ein bisschen unklar wie ich da vorgehen soll.

Bei dem Induktionsschritt, denke ich mal ich soll da immer sagen, wie der Alogrithmus unmittelbar nach dem 1. rekursiven Schritt weitergeht. So habe ich das hier geschrieben.. :?

In der Textdatei Muster für Korrektheit steht für Korrektheit:
"Bei Rekursionen muss die Korrektheit aus der Aussage der Invariante für den allerersten rekursiven Aufruf folgen. Gerade wenn die Rekursion in eine eigene Methode ausgelagert wird, sind häufig noch Zusatzargumente notwendig."
Ich verstehe jedoch nicht, was sie mit Zusatzargumente meinen. : :roll:


Input:
Ein aufsteigend sortiertes Array, das ungleich null sein soll.
Ein Integer x.\


Wohldefiniertheit:
NullPointerException kann nicht sein,da es keine Zuweisungen gibt, die auf null zugreifen könnten.
ArithmeticException kann nicht sein, da die berechneten Variablen maximal so groß sind wie die Länge des Arrays, und somit kein Überlauf auftreten kann.

Variante:
j-i wird in jedem Rekursionssaufruf echt kleiner, somit verändert sich in jede Rekursion die Position der Variable m.


Terminierung:
Aufgrund der Variante wird die Abbruchbedingung a[m]==x oder j-i==0 (= Teilarray mit 1 Element) nach endlich vielen Rekursionsschritte erreicht.

Invariante:
Unmittelbar nach einen rekursiven Schritt gilt, das falls der gesuchte Element im Array enthalten ist, so ist er im Teilarray l+1( l = i = linke Grenze des Intervalls) bis r-1 (l = j = rechte Grenze des Intervalls) zu finden.

Induktionsanfang:
Die Rekursion bricht im Fall von l-r=0 oder a[m] = x, und liefert -1 bzw die Position des gesuchten Wertes x.

Induktionsschritt:
Nach Induktionsvoraussetzung gilt, das falls x im Array enthalten ist, so ist er zwischen dem Intervall r+1 bis i-1 zu finden. Somit ergibt sich, das falls die mittlere Variable nicht auf den gesuchten Wert zuweist, und r-l ungleich 0 sind, eine Fallunterscheidung passiert:
Ist a[m] kleiner als x, so ruft sich die Methode wieder mit r als m+1 auf, also die 1. Hälfte des Arrays wird vernachlässigt.
Ist a[m] größer x so ruft sich die Methode mit gleichem r, jedoch l-1 wieder auf.

Korrektheit:
Gilt der Algorithmus für den allerersten Rekursionsaufruf, so liefert er nach endlich vielen Rekursionsschritten das korrekte Ergebnis.

Prof. Karsten Weihe
Moderator
Moderator
Beiträge: 1824
Registriert: 21. Feb 2005 16:33

Re: T2: Beispiel 3

Beitrag von Prof. Karsten Weihe » 11. Sep 2016 14:48

Hallo hat geschrieben: Bei dem Induktionsschritt, denke ich mal ich soll da immer sagen, wie der Alogrithmus unmittelbar nach dem 1. rekursiven Schritt weitergeht.
In der Vorlesung und darüber hinaus hatte ich öfters versucht, folgendes zu kommunizieren: Gehen Sie beim Verstehen und bei der Analyse von rekursiven Methoden am Besten einfach von dem Code aus und vergessen Sie den zeitlichen Ablauf der Rekursion. Im Code muss es eine Fallunterscheidung geben mit mindestens einem Fall (meist auch nur ein Fall), in dem die Methode nicht rekursiv aufgerufen wird. Im Induktionsanfang argumentieren Sie, warum die Invariante in diesen Fällen eingehalten wird. Im Induktionsschritt argumentieren Sie, warum die Invariante in den anderen Fällen eingehalten wird, wobei Sie prüfen müssen, ob die Inputs der rekursiven Aufrufe der Input-Spezifikation entsprechen, und dann von der Annahme ausgehen dürfen, dass die rekursiven Aufrufe den korrekten Output für ihren Input liefern (diese Annahme ist die Induktionshypothese).
Hallo hat geschrieben: Ich verstehe jedoch nicht, was sie mit Zusatzargumente meinen. : :roll:
Wir unterscheiden ja häufig zwischen der eigentlichen Methode, die dann nicht selbst rekursiv ist, und einer rekursiven Hilfsmethode mit leicht erweiterter Parameterliste. Zum Beispiel Ihre Parameter l und r würden ja nicht zum Input der eigentlichen Suchmethode gehören, sondern erst zum Input der rekursiven Hilfsmethode.

Häufig werden in der eigentlichen Methode aber darüber hinaus noch weitere Operationen durchgeführt, die natürlich auch korrekt sein müssen. Beispiele dafür müssten Sie in den Übungsaufgaben finden. Die Argumente zur Korrektheit dieser Operationen sind Zusatzargumente über die Rekursion hinaus.
Hallo hat geschrieben: Wohldefiniertheit:
NullPointerException kann nicht sein,da es keine Zuweisungen gibt, die auf null zugreifen könnten.
ArithmeticException kann nicht sein, da die berechneten Variablen maximal so groß sind wie die Länge des Arrays, und somit kein Überlauf auftreten kann.
Im Fall, dass der Input ein Array ist und Sie auf etwas komplizierte Weise darauf arbeiten, ist natürlich IndexOutOfBoundsException besonders interessant.

Hallo hat geschrieben: Variante:
j-i wird in jedem Rekursionssaufruf echt kleiner, somit verändert sich in jede Rekursion die Position der Variable m.
Ihr erster Halbsatz ist die Variante, ok. Ihr zweiter Halbsatz scheint mir keinen ernsthaften Erkenntnisgewinn im Hinblick auf Korrektheit zu bringen?

Disclaimer für das folgende: Kann sein, dass ich mich mit i, j, l und r hier und da um 1 vertun werde, prüfe ich jetzt nicht nach.
Hallo hat geschrieben: Terminierung:
Aufgrund der Variante wird die Abbruchbedingung a[m]==x oder j-i==0 (= Teilarray mit 1 Element) nach endlich vielen Rekursionsschritte erreicht.
Ich stimme zu.
Hallo hat geschrieben: Invariante:
Unmittelbar nach einen rekursiven Schritt gilt, das falls der gesuchte Element im Array enthalten ist, so ist er im Teilarray l+1( l = i = linke Grenze des Intervalls) bis r-1 (l = j = rechte Grenze des Intervalls) zu finden.
Ich stimme zu, wobei mir nicht klar ist, wieso wir i und l bzw. j und r gleichzeitig haben sollten, jeweils eine der beiden Notationen reicht doch, oder?
Hallo hat geschrieben: Induktionsanfang:
Die Rekursion bricht im Fall von l-r=0 oder a[m] = x, und liefert -1 bzw die Position des gesuchten Wertes x.
Ich denke, die eigentlich spannende Frage lassen Sie aus: Warum ist das Ergebnis in beiden Fällen korrekt. Der eine Fall ist a[m]==x, in diesem Fall ist x gefunden und daher das Ergebnis offensichtlich korrekt. Der andere Fall ist r<l, und in diesem Fall folgt Korrektheit von -1 aus der Invariante: Wenn x nicht innerhalb des Intervalls l..r zu finden ist, sofern x überhaupt im Array ist, das Intervall l..r aber leer ist, dann kann x nicht im Array sein, und die Rückgabe ist wieder korrekt.
Hallo hat geschrieben: Induktionsschritt:
Nach Induktionsvoraussetzung gilt, das falls x im Array enthalten ist, so ist er zwischen dem Intervall r+1 bis i-1 zu finden. Somit ergibt sich, das falls die mittlere Variable nicht auf den gesuchten Wert zuweist, und r-l ungleich 0 sind, eine Fallunterscheidung passiert:
Ist a[m] kleiner als x, so ruft sich die Methode wieder mit r als m+1 auf, also die 1. Hälfte des Arrays wird vernachlässigt.
Ist a[m] größer x so ruft sich die Methode mit gleichem r, jedoch l-1 wieder auf.
Sie beschreiben, was die Methode macht, aber nicht, warum die Invariante eingehalten wird.

Ich würde es vielleicht so formulieren: Ist a[m] kleiner als x, dann folgt aus der aufsteigenden Sortierung des Arrays, dass x nicht im Intervall m..r sein kann. Daraus folgt: Falls x in l..r ist, dann ist x in l..m-1. Die Induktionsvoraussetzung besagt: Falls x im Array ist, ist es in l..r. Beides zusammen ergibt transitiv: Falls x im Array ist, ist x in l..m-1, was zu zeigen war. Der Fall, dass x größer a[m] ist, ist natürlich analog.

Die Induktionsvoraussetzung und die Voraussetzung, dass das Array aufsteigend sortiert sind, müssen ja irgendwo in die Argumentation eingehen. Es ist immer sinnvoll, sich für jede Voraussetzung klarzumachen, an welcher Stelle sie eingeht, und dort auch explizit mit ihr zu arbeiten, so wie ich das im vorherigen Absatz gemacht habe. Die Stelle ist im Prinzip leicht zu finden: da, wo die Methode falsch laufen würde, wenn die Voraussetzung nicht erfüllt wäre.
Hallo hat geschrieben: Korrektheit:
Gilt der Algorithmus für den allerersten Rekursionsaufruf, so liefert er nach endlich vielen Rekursionsschritten das korrekte Ergebnis.
"Gelten" ist kein Verb, das auf Algorithmen anwendbar ist, oder? Was meinen Sie wirklich?

KW

Hallo
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 162
Registriert: 22. Apr 2015 19:03

Re: T2: Beispiel 3

Beitrag von Hallo » 11. Sep 2016 15:32

Prof. Karsten Weihe hat geschrieben:"Gelten" ist kein Verb, das auf Algorithmen anwendbar ist, oder? Was meinen Sie wirklich?
Hier meine ich:
Solange der Algorithmus vor dem 1. rekursiven Aufruf nicht terminiert wurde, heißt das das die Invariante gehalten wurde und das Korrekte Ergebnis wird nach endlich viele Rekursionsschritte zurückgegeben.

Ist das so besser formuliert ?

Prof. Karsten Weihe
Moderator
Moderator
Beiträge: 1824
Registriert: 21. Feb 2005 16:33

Re: T2: Beispiel 3

Beitrag von Prof. Karsten Weihe » 11. Sep 2016 15:49

Hallo hat geschrieben: Solange der Algorithmus vor dem 1. rekursiven Aufruf nicht terminiert wurde
Das verstehe ich schon nicht.

KW

Hallo
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 162
Registriert: 22. Apr 2015 19:03

Re: T2: Beispiel 3

Beitrag von Hallo » 11. Sep 2016 16:05

Okay ich versuche es nochmal:

Falls der Algorithmus nicht vor dem aller ersten rekursiven Aufruf abbricht, bedeutet das das gesuchte Element nicht gefunden wurde und falls das gesuchte Element im Array enthalten ist, so ist es im Teilarray l+1 bis r-1 zu finden. Durch die Variante, das j-i in jedem Rekursionsschritt echt kleiner wird kommt der Algorithmus nach endlich vielen Schritten zur Abbruchbedingung an und das Korrekte Ergebnis liefert.

Ist das so besser? :oops:

Hallo
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 162
Registriert: 22. Apr 2015 19:03

Re: T2: Beispiel 3

Beitrag von Hallo » 12. Sep 2016 15:07

Kann ich bitte eine Antwort kriegen ? :)

Prof. Karsten Weihe
Moderator
Moderator
Beiträge: 1824
Registriert: 21. Feb 2005 16:33

Re: T2: Beispiel 3

Beitrag von Prof. Karsten Weihe » 12. Sep 2016 15:15

Hallo hat geschrieben: Falls der Algorithmus nicht vor dem aller ersten rekursiven Aufruf abbricht, bedeutet das das gesuchte Element nicht gefunden wurde
Ich verstehe nicht, was Sie damit meinen, dass der Algo vor dem allerersten Aufruf abbricht.

KW

Antworten

Zurück zu „AuD: Theoretische Aufgaben“