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.
