Seite 1 von 1

2a: abs

Verfasst: 24. Mai 2017 11:45
von 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).

Re: 2a: abs

Verfasst: 24. Mai 2017 12:10
von 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ß

Re: 2a: abs

Verfasst: 24. Mai 2017 12:24
von 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.

Re: 2a: abs

Verfasst: 24. Mai 2017 14:34
von invariant
Das ist korrekt.
Was bei gleich null passiert sollte am besten spezifiziert werden. Also angeben was mit diesen Zahlen passiert.

Gruß

Re: 2a: abs

Verfasst: 24. Mai 2017 14:45
von LordMaddhi
Ok, dankeschön :)