Theorietestat #2: Substractor

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!
LukasPhysiker
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 111
Registriert: 6. Mai 2017 13:05

Theorietestat #2: Substractor

Beitrag von LukasPhysiker » 6. Mai 2017 13:18

Hallo,

auf Theorietestat #2 sollen wir für die Methode substract der Klasse Substractor (auf S.8/9) beweisen, dass der Algorithmus korrekt ist. Da die nächste Aufgabe sein soll, zu zeigen, dass pow nicht korrekt arbeitet, soll ich davon ausgehen, dass Substractor fehlerfrei sein soll? Das ist sie meiner Meinung nach nämlich nicht.

Erstmal kompiliert die Klasse so überhaupt nicht! Eclipse meckert: "The operator > is undefined for the argument type(s) java.lang.Number, java.lang.Number". Wenn ich Number durch int ersetze, dann kompiliert es wenigstens.

Wenn ich jetzt als Beispiel den Array (10,100,2) als Input eingebe, dann ist der Output (10,2,2). Man sieht, dass nicht jede Zahl kleiner ist als die darauffolgende Zahl, was vor allem daran liegt, dass die Zahl, mit der die vorherige Zahl verglichen wurde, danach selbst möglicherweise verkleinert wird und dann wieder kleiner ist als die vorherige Zahl. Und 2 ist auch nicht (echt) kleiner als 2. Man sollte in der if-Abfrage besser => statt > schreiben.

Das ganze wird natürlich umso schlimmer, wenn man negative Zahlen eingibt...

Ist das ein Fehler, oder sollen wir beim "Beweisen der Korrektheit" auch manchmal Fehler im Algorithmus finden?

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

Re: Theorietestat #2: Substractor

Beitrag von invariant » 6. Mai 2017 19:09

Hallo,

Grundsätzlich sollen beim Korrektheitsbeweis auch Fehler im Algorithmus erkannt werden.

Bei der von Ihnen genannten Aufgabe ist das allerdings bei der Formulierung ein bisschen schief gegangen. In der neuen Version wurde es überarbeitet.

Das die Klasse nicht komplimierbar ist ist wahr, sollte in diesem Fall besser ein Comparator verwendet werden, wird u.U. gleich auch noch geändert ;)
Die Intention sollte aber klar sein - gehen sie für den Moment einfach von einem Zahlenvergleich aus.

Was negative Zahlen angeht : Das wäre etwas das im Korrektheitsbeweis erwähnt werden sollte.

Gruß Jannik

Anton Haubner
Neuling
Neuling
Beiträge: 5
Registriert: 21. Apr 2017 09:35

Re: Theorietestat #2: Substractor

Beitrag von Anton Haubner » 15. Mai 2017 16:30

Ich hätte zu dieser Aufgabe auch noch eine Frage:

Soweit ich es verstanden habe, soll in AuD die Invariante immer abhängig von der Anzahl bisheriger Iterationen formuliert werden ("h"). Hier scheint es mir jedoch sinnvoller (notwendig?), die Invariante abhängig vom Zähler i zu formulieren.

Ist diese Annahme korrekt und die Notwendigkeit, die Iterationsanzahl "h" zu verwenden, also nicht so streng?

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

Re: Theorietestat #2: Substractor

Beitrag von invariant » 15. Mai 2017 17:38

Es soll von der Zahl der Iterationen also h abhängig sein.
Das ist in dieser Aufgabe nicht ganz so einfach, i hängt mit der Zahl der Iterationen und in diesem Fall dem Input zusammen.
Also es ist definitiv möglich die Invariante von der Zahl der Iterationen zu machen. Von i abhängig zu sein, wäre wohl auch in der Induktion nicht mehr so schön, da ja eine variable Anzahl an Iterationen zusammengefasst würden.
Vielleicht mal überlegen wieviele Iterationen i gleich bleibt bis es erhöht wird.

Ist vielleicht als Übung nicht schlecht sich damit auch mal an einem komplizierteren Beispiel zu versuchen.

Gruß

Anton Haubner
Neuling
Neuling
Beiträge: 5
Registriert: 21. Apr 2017 09:35

Re: Theorietestat #2: Substractor

Beitrag von Anton Haubner » 15. Mai 2017 20:43

Hi, Danke für die Antwort!

Naja, wenn a > a[i+1], dann bleibt i gleich für diese Anzahl k an Iterationen:
\(k = \left\lfloor \frac{a_i}{a_{i+1}} \right\rfloor, \quad a_i > a_{i+1}\)

Dennoch bin ich mir nicht sicher, ob diese Erkenntnis hilft. Vielleicht bin ich ja grade etwas schwer von Begriff, allerdings kann die Situation a > a[i+1] beliebig oft innerhalb eines Array-Durchlaufs auftreten. Entsprechend ist es unmöglich allein durch die Anzahl der Iterationen h die aktuelle Position im Array zu bestimmen. Das führt dazu, dass ich keine Aussage treffen kann in der Art "Der Array ist nach Output-Spezifikation korrekt transformiert bis Index f(h) - 1."

Um eine Funktion f(h) zu entwerfen, welche mir den aktuellen Index bestimmt, müsste ich wieder andere Daten als h in die Invariante aufnehmen. In diesem Fall wäre das der Array a (allerdings nur die Originaleingabe. Da der Array in-place editiert wird, gehen hier während des Algorithmus Informationen verloren.).

Evtl. bin ich auch auf dem Holzweg, meine Invariante so formulieren zu wollen, dass sie ausdrückt, bis zu welcher Stelle der Array "korrekt umgeformt" wurde.

Um nochmal ein Beispiel zu untersuchen:
Der Array [3,2,4,5] wäre nach 2 Iterationen im Algorithmus bis Index 1 vorgedrungen, somit ist er bis einschließlich Index 1-1=0 korrekt transformiert worden zu [1, 2, 4, 5].

Der Array [2,3,4,5] wäre nach 2 Iterationen bis Index 2 vorgedrungen. Ich könnte aussagen, dass er bis einschließlich Index 2-1=1 korrekt transformiert wurde (keine Änderung).

Somit sollte ich, ohne zumindest den originalen Array hinzuzuziehen, allein mit h nicht aussagen können, bis zu welcher Stelle ein korrektes Zwischenergebnis vorliegt. Ist das allerdings nicht die Forderung, die von der Invariante gestellt wird?

Grüße

(P.S. ich glaube das Problem ist hier evtl. auch, dass eigentlich zwei geschachtelte Schleifen/Iterationen vorliegen)
Zuletzt geändert von Anton Haubner am 15. Mai 2017 20:57, insgesamt 1-mal geändert.

UnkownIdentity
Erstie
Erstie
Beiträge: 11
Registriert: 7. Mai 2017 14:58

Re: Theorietestat #2: Substractor

Beitrag von UnkownIdentity » 15. Mai 2017 20:49

Hallo zusammen,

auch ich habe immer noch Schwierigkeiten eine allgemeine Invariante für die Aufgabe zu formulieren. Ich denke es ist klar, dass i maximal für eine weitere Iteration nicht erhöht wird (wenn ich a[i+1] von a abziehe, ist a in der nächsten Iteration in jedem Fall kleiner als a[i+1], so dass i dann erhöht wird). Dennoch sehe ich nicht, wie es möglich ist eine korrekte Invariante aufzustellen welche die Elemente im Array in Beziehung stellt.

Angenommen zum Zeitpunkt h-2 gilt, dass a <= a[i+1], so dass i inkrementiert wird.
Es können nun zwei Fälle in Iteration h-1 auftreten:

(I) Für das neue i gilt: a > a[i+1].
- Daraus folgt, dass a in Iteration h-1 um a[i+1] reduziert wird und i nicht inkrementiert.
- Damit gilt in Iteration h nun zunächst wieder a <= a[i+1], so dass i inkrementiert wird. Nach Iteration h habe ich also wieder ein neues i, so dass ich zwar sagen kann dass a[i-1] <= a, aber nicht dass a <= a[i+1], da ich über das neue a[i+1] ja noch nichts weiß.

(II) Für das neue i gilt: a <= a[i+1].
- Daraus folgt, dass a in Iteration h-1 nicht verändert wird, und i inkrementiert
- Für das neue i in Iteration h können nun wieder zwei Fälle auftreten:
- (II/A) a[i] > a[i+1], weshalb a[i] noch in Iteration h verringert wird, so dass gilt a[i] <= a[i+1], aber nicht a[i-1] <= a[i] weil ich a[i] verändert habe
- (II/B) a[i] <= a[i+1], weshalb i noch in Iteration h inkrementiert wird. Damit kann ich zwar sagen, dass a[i-1] <= a[i], was ich ja eben nachgewiesen habe. Aber die Aussage a[i] <= a[i+1] kann ich nicht beurteilen, da ich mir as Element a[i+1] noch gar nicht angesehen habe. Das i wurde ja gerade frisch inkrementiert. (selber Fall wie oben)

Für Fall (I) und (II/B) kann ich zwar eine gemeinsame Invariante aufstellen, Fall (II/A) kriege ich aber nicht mit rein. Habe ich jetzt irgendwo einen Denkfehler?

LG

Nachtrag:
Der erste Denkfehler war schon bei der Annahme dass i nur für höchstens eine Iteration gleich bleibt, wie durch meinen Vorredner jetzt widerlegt worden ist. Aber dennoch bleibt das Problem bestehen, dass ich zum Zeitpunkt einer Iteration nie weiß wie sich die Daten an einer durch i bestimmten Position zueinander verhalten, weil ich die Daten ja permanent veränderre - oder eben auch nicht.

An meinen Vorredner: ich glaube mit dem in Abhängigkeit von der Zahl d. Iterationen stellen ist gemeint, dass man sagt "Nach h>=0 Iterationen gilt..." statt "Nach i>= Iterationen gilt...". Innerhalb der Invariante kannst du dann wieder beliebig auf den eigentlichen Zählparameter i zugreifen. So jedenfalls mein Verständnis, andernfalls ergebe sich ja die durch dich beschriebene Problematik dass ich anhand von h nie weiß wo ich im Array jetzt eigentlich bin.

Macavity
Windoof-User
Windoof-User
Beiträge: 27
Registriert: 27. Apr 2015 19:56

Re: Theorietestat #2: Substractor

Beitrag von Macavity » 16. Mai 2017 11:19

Was ist denn wenn man [2,0] als array eingibt? Dann terminiert der Algorithmus meiner Ansich nach gar nicht. Dann gilt immer a > a[i+1] und durch die Subtraktion von 0 von a wird das auch nicht verändert.

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

Re: Theorietestat #2: Substractor

Beitrag von invariant » 16. Mai 2017 15:49

Hallo,

wie schon bemerkt ist das Beispiel nicht ganz trivial - also keine Panik falls das nicht sofort gelingt.

Kurze Vorbemerkung - steht noch nicht explizit drin - die Zahlen des Arrays sind alle größer 0 als Vorbedingung des Algos.

Zum einen Input mit einbeziehen - ja geht ansonsten hier nicht sonderlich sauber. Also einfach das Array zum Zeitpunkt der Eingabe als a' oder so definieren.

Noch ein paar Hinweise:

Invariante abhängig vom Iterationszähler
i abhängig vom Input Array und Iterationszähler - da wieder der Hinweis wie lange "verweilt" der Algo auf einem Index
Dann in der Invariante kann zum einen eine Aussage für die Elemente a[0]...a[i-1] getroffen werden. (a ist hierbei das Ausgabearray)
Es kann auch noch eine Aussage über a getroffen werden - dort wurden evtl. schon Elemente abgezogen in der h-ten Iteration


Variante hat mehr als nur einen Teil ;)

Hoffe das hilft weiter ansonsten fragen.

Gruß

Antworten

Zurück zu „AuD: Theoretische Aufgaben“