Korrektheitsbeweis: isAscending

fy06keju
Neuling
Neuling
Beiträge: 7
Registriert: 5. Sep 2016 16:52

Korrektheitsbeweis: isAscending

Beitrag von fy06keju » 17. Sep 2016 23:53

Guten Abend, ich habe für die Aufgabe 3.3.1 isAscending(iterativ für PartiallyUsedArray) ein Korrektheisbeweis geführt.
Würde mich sehr auf eine Antwort bzw. Feedback freuen.

hier erstmal mein Code:

Code: Alles auswählen

public boolean isAscending(PartiallyUsedArray<T> array, Comparator<T> cmp) {
  for(int i=0; i< array.numberOfUsedSlots; i ++) 
    if(cmp.compare(array.theArray[i+1] < array.theArray[i])< 0)
      return false;
      return true; }

Korrektheitsbeweis

Funktion: überprüft ob das Array aufsteigend sortiert ist.

Input: ein teilweise besetztes Array 'array' , ein Comparator cmp vom Typ T

Output: true, wenn die Schlüsselworte im array korrekt aufsteigend sortiert ist, sonst false.

Variante: i wird in jedem Schritt um eins erhöht

Terminierung: da die Anzahl der Schlüsselwerte eines Arrays endlich sieht, wird nach endlich vielen Schritten die Abbruchbedingung i = array.numberOfUsedSlots erreicht.

Invariante: nach i >=0 Interationen sind alle Schlüsselwerte des teilweise besetzten Arrays im Indexbereich [0...i+1] nach korrekter Reihenfolge überprüft.

Induktionsanfang: unmittelbar vor dem ersten Iterationsschritt ist i=0 und somit wurden trivialerweise 0 Elemente nach korrekter Reihenfolge überprüft

Induktionsschritt: nach der Induktionsvoraussetzung gilt, dass unmittelbar vor der i-ten Interation alle Schlüsselwerte im Indexbereich [0..i] korrekt überprüft wurden. Anhand eines Comparators wird nun in der i-ten Iteration das Element an der i+1 Position mit dem Wert an Position i verglichen.
Falls array.theArray[i+1] < array.theArray[i+1], so ist definitionsgemäß das Array nicht in korrekter Reihenfolge gebildet, sodass korrekterweise false zurückgegeben wird. Wenn tatsächlich der Schlüsselwert an Position i+1 größer ist als der Schlüsselwert an Position i, so wird true zurückgeliefert.
Also bleibt die Invariante in jedem Fall erhalten.

Korrektheit: Aufgrund der Variante und Abbruchbedingung wird nach endlich vielen Iterationsschritten der Algorithmus terminieren. Da die Invariante bis zur Terminierung erhalten bleibt folgt die Korrektheit.

yokop
Windoof-User
Windoof-User
Beiträge: 28
Registriert: 13. Apr 2016 12:49

Re: Korrektheitsbeweis: isAscending

Beitrag von yokop » 18. Sep 2016 10:48

fy06keju hat geschrieben:

Code: Alles auswählen

public boolean isAscending(PartiallyUsedArray<T> array, Comparator<T> cmp) {
  for(int i=0; i< array.numberOfUsedSlots; i ++) 
    if(cmp.compare(array.theArray[i+1] < array.theArray[i])< 0)
      return false;
      return true; }
Ich nehme mal an, dass das < bei dem cmp.compare ein , seien soll.

Ich meine einen Fehler entdeckt zu haben, denn du prüfst, ob i < array.numberOfUsedSlots, in der Schleife an sich greifst du dann aber auf die Komponente array.theArray[i+1] zu, welche nach Definition des partiellen Arrays zwar existiert, jedoch nur im Bereich 0..numberOfUsedSlots-1 Schlüsselwerte stehen. Also kommt deine Methode auf ein falsches Ergebnis, da dieses Element (normalerweise das jeweilige null-Element des Datentyps) mit verglichen wird.

Prof. Karsten Weihe
Dozentin/Dozent
Beiträge: 1824
Registriert: 21. Feb 2005 16:33

Re: Korrektheitsbeweis: isAscending

Beitrag von Prof. Karsten Weihe » 18. Sep 2016 13:09

fy06keju hat geschrieben:

Code: Alles auswählen

public boolean isAscending(PartiallyUsedArray<T> array, Comparator<T> cmp) {
  for(int i=0; i< array.numberOfUsedSlots; i ++) 
    if(cmp.compare(array.theArray[i+1] < array.theArray[i])< 0)
      return false;
      return true; }
Ich stimme yokops vorhergehendem Posting zu.
fy06keju hat geschrieben: Korrektheitsbeweis
Funktion: überprüft ob das Array aufsteigend sortiert ist.
Ok.
fy06keju hat geschrieben: Input: ein teilweise besetztes Array 'array' , ein Comparator cmp vom Typ T
In einer echten Projektsituation sollte man so etwas schreiben wie: "ein teilweise besetztes Array gemäß Abschnitt ??? der Doku ???", in der AUD ist der Kontext klar, also ok.
fy06keju hat geschrieben: Output: true, wenn die Schlüsselworte im array korrekt aufsteigend sortiert ist, sonst false.
Abgesehen vom Numerus-Fehler ok.

Zur Klarstellung würde sich anbieten zu schreiben: "... korrekt aufsteigend sortiert gemäß cmp.compare ...".
fy06keju hat geschrieben: Variante: i wird in jedem Schritt um eins erhöht
Ok.
fy06keju hat geschrieben: Terminierung: da die Anzahl der Schlüsselwerte eines Arrays endlich sieht, wird nach endlich vielen Schritten die Abbruchbedingung i = array.numberOfUsedSlots erreicht.
Ok, bis auf das Verb mit falscher Semantik (Ihr Projektleiter oder Kunde später wird nicht den besten Eindruck von Ihnen bekommen). Bei Kommentierung einer Java-Methode bietet sich an, die Java-Syntax für Gleichheit zu verwenden, also "==" statt "=".
fy06keju hat geschrieben: Invariante: nach i >=0 Interationen sind alle Schlüsselwerte des teilweise besetzten Arrays im Indexbereich [0...i+1] nach korrekter Reihenfolge überprüft.
Könnte man vielleicht besser formulieren, weil Sie eher den Algorithmus nacherzählen, aber in diesem Fall ok.
fy06keju hat geschrieben: Induktionsanfang: unmittelbar vor dem ersten Iterationsschritt ist i=0 und somit wurden trivialerweise 0 Elemente nach korrekter Reihenfolge überprüft.
Ok.
fy06keju hat geschrieben: Induktionsschritt: nach der Induktionsvoraussetzung gilt, dass unmittelbar vor der i-ten Interation alle Schlüsselwerte im Indexbereich [0..i] korrekt überprüft wurden. Anhand eines Comparators wird nun in der i-ten Iteration das Element an der i+1 Position mit dem Wert an Position i verglichen.
Falls array.theArray[i+1] < array.theArray[i+1], so ist definitionsgemäß das Array nicht in korrekter Reihenfolge gebildet, sodass korrekterweise false zurückgegeben wird. Wenn tatsächlich der Schlüsselwert an Position i+1 größer ist als der Schlüsselwert an Position i, so wird true zurückgeliefert.
Also bleibt die Invariante in jedem Fall erhalten.
Ok.
fy06keju hat geschrieben: Korrektheit: Aufgrund der Variante und Abbruchbedingung wird nach endlich vielen Iterationsschritten der Algorithmus terminieren. Da die Invariante bis zur Terminierung erhalten bleibt folgt die Korrektheit.
Hier rächt sich jetzt, dass Sie Wohldefiniertheit ausgelassen haben, denn je nachdem, wie die Comparator-Klasse mit Parameter null umgeht, kann es eine NullPointerException geben. Und falls das teilweise besetzte Array im aktuellen Moment gerade vollbesetzt ist, gibt es vorher schon eine IndexOutOfBoundsException.

KW

fy06keju
Neuling
Neuling
Beiträge: 7
Registriert: 5. Sep 2016 16:52

Re: Korrektheitsbeweis: isAscending

Beitrag von fy06keju » 18. Sep 2016 14:22

yokop hat geschrieben:
fy06keju hat geschrieben:

Code: Alles auswählen

public boolean isAscending(PartiallyUsedArray<T> array, Comparator<T> cmp) {
  for(int i=0; i< array.numberOfUsedSlots; i ++) 
    if(cmp.compare(array.theArray[i+1] < array.theArray[i])< 0)
      return false;
      return true; }
Ich nehme mal an, dass das < bei dem cmp.compare ein , seien soll.


Ich meine einen Fehler entdeckt zu haben, denn du prüfst, ob i < array.numberOfUsedSlots, in der Schleife an sich greifst du dann aber auf die Komponente array.theArray[i+1] zu, welche nach Definition des partiellen Arrays zwar existiert, jedoch nur im Bereich 0..numberOfUsedSlots-1 Schlüsselwerte stehen. Also kommt deine Methode auf ein falsches Ergebnis, da dieses Element (normalerweise das jeweilige null-Element des Datentyps) mit verglichen wird.
Aha..wenn ich die for-schleife so ändere greife ich nun nur auf die Schlüsselwerte im Beriech 0..numberOfUsedSlots-1 zu oder?

for(int i=0; i< array.numberOfUsedSlots -1 ; i++) {
if(cmp.compare(array.theArray[i+1], array.theArray) < 0) return false;
...

Antworten

Zurück zu „Archiv“