2a: abs

Bei Postings zu Aufgabe Nr. x auf Blatt Nr. y lassen Sie Ihr Betreff bitte mit "y.x: " beginnen, gefolgt von einer möglichst präzisen Überschrift, danke!

Moderator: Algorithmen und Datenstrukturen

Forumsregeln
Bei Postings zu Aufgabe Nr. x auf Blatt Nr. y lassen Sie Ihr Betreff bitte mit "y.x: " beginnen, gefolgt von einer möglichst präzisen Überschrift, danke!
Benutzeravatar
LordMaddhi
Nichts ist wie es scheint
Beiträge: 23
Registriert: 20. Apr 2017 11:57
Wohnort: Darmstadt, Hessen

2a: abs

Beitrag von LordMaddhi » 24. Mai 2017 11:45

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).
Ich bin nicht die Signatur. Ich putze hier nur.

invariant
Mausschubser
Mausschubser
Beiträge: 65
Registriert: 6. Mai 2017 19:01

Re: 2a: abs

Beitrag von invariant » 24. Mai 2017 12:10

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ß

Benutzeravatar
LordMaddhi
Nichts ist wie es scheint
Beiträge: 23
Registriert: 20. Apr 2017 11:57
Wohnort: Darmstadt, Hessen

Re: 2a: abs

Beitrag von LordMaddhi » 24. Mai 2017 12:24

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.
Ich bin nicht die Signatur. Ich putze hier nur.

invariant
Mausschubser
Mausschubser
Beiträge: 65
Registriert: 6. Mai 2017 19:01

Re: 2a: abs

Beitrag von invariant » 24. Mai 2017 14:34

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

Gruß

Benutzeravatar
LordMaddhi
Nichts ist wie es scheint
Beiträge: 23
Registriert: 20. Apr 2017 11:57
Wohnort: Darmstadt, Hessen

Re: 2a: abs

Beitrag von LordMaddhi » 24. Mai 2017 14:45

Ok, dankeschön :)
Ich bin nicht die Signatur. Ich putze hier nur.

Antworten

Zurück zu „AuD: Theoretische Aufgaben“