Korrektheitsbeweis: isAscending

[fy06keju]

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]

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]

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.

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

Ok.

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.

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

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

Ok.

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

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.

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

Ok.

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.

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]

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