2a: abs

[LordMaddhi]

Hallo,
ist meine Beweis so korrekt? :

Spezialisierung:
- Vorbedingung: a ist ein korrekt gebildetes Integer-Array (auch a == null möglich)
- Output: Array mit Beträgen der Zahlen aus a[0]...a[a.length - 1]
- Nachbedingung: keine

Elemente des Korrektheitsbeweises:
- Wohldefiniertheit:
- Division durch 0: --
- Arithmetischer Überlauf: --
- lesender/schreibender Zugriff auf null: ja, aber wird in der Methode behandelt
- lesender/schreibender Zugriff auf nichtexistente Arraykomponente: ja, aber wird in der Methode behandelt
- Würfe von anderen RunTimeExceptions: --
- Variante: i wird um eins erhöht
- Abbruchbedingung: Schleife (bzw. Methode) bricht ab, wenn alle Array-Elemente durchlaufen worden sind (wenn i == a.length)
- Invariante: Nach h >= 0 Iterationen gilt: result enthält die Beträge der Zahlen aus a[0]...a[ i ] mit i = h - 1.



Beweis:
- Induktionsanfang: Nach h = 0 Iterationen gilt: result enthält Beträge von a[0]...a[ i ] mit i = 0-1 = -1 => leere Aussage => korrekt
- Induktionsvoraussetzung: Nach h-1 Iterationen gilt: return enthält Beträge der Zahlen von a[0]...a[ i ] mit i = h-2.
- Induktionsschritt: Nach h-1 Iterationen gilt: (Invariante:) return enthält Beträge der Zahlen von a[0]...a[ i ] mit i = h-2.
In der h-ten Iteration wird das Element a[i+1] mit i = h-2 "bearbeitet" (Betrag in result eingefügt.)
Damit enthält result die Beträge von a[0]...a[h-1], was der Invariante entspricht.

Kombination der Teilschrittte:
- Terminierung: Aus Abbruchbedingung und Variante folgt: Da i in jedem Schritt um 1 erhöht wird, entspricht i zu einen gewissen Zeitpunkt
der Abbruchbedingung (i == a.length) => Algo terminiert.
- Korrektes Endergebnis: Aus Invariante und Abbruchbedingung folgt: Wenn die Abbruchbedingung eintritt, gilt mit der Invariante, dass result die Beträge von a[0]...a[a.length - 1] enthält (entspricht dem Output).

[invariant]

Wenn der Algorithmus korrekt wäre, wäre das wohl ein ganz guter Beweis.
Ist er aber leider nicht
- Vielleicht an der Stelle nochmal genauer hinschauen.
Vielleicht den Induktionsschritt sauberer aufschreiben : Was passiert für die einzelnen Fälle? Element >= 0, Element < 0, oder Element == null.
Dann fällt der Fehler vielleicht schon auf.

Abbruchbedingung könnte besser als i >= a.length angegeben werden. Ist aber hier durch i++ nicht unbedingt notwendig.

Gruß

[LordMaddhi]

Danke für die Antwort.
Ich bin dabei von einem korrekten Algo ausgegangen

Die Fehler bei dem hier vorliegenden sind meiner Meinung nach:
- es werden nur Beträge der Zahlen < 0 in result eingetragen (Zahlen >= 0 werden nicht behandelt -> if-Abzweigung fehlt)
- wenn die Zahl gleich null ist, wird 0 eingefügt, was meiner Meinung nach falsch ist, da null != 0. Ich hätte weiterhin null eingefügt.

[invariant]

Das ist korrekt.
Was bei gleich null passiert sollte am besten spezifiziert werden. Also angeben was mit diesen Zahlen passiert.

Gruß

[LordMaddhi]

Ok, dankeschön