Lab4 - Task3 - Aufgabe 2.6

florian.k
Neuling
Neuling
Beiträge: 5
Registriert: 3. Dez 2012 22:34

Lab4 - Task3 - Aufgabe 2.6

Beitrag von florian.k »

Zunächst einmal Danke für die letzte Frage bezüglich des Konstruktors.

Wir sind nun fast fertig. Es fehlt lediglich der Proof, dass add die Invariante von min einhält. Wir arbeiten nun seid 3 Tagen daran und kommen einfach nicht weiter. Die add Methode wurde von uns im Zuge von Task 3 minimal angepasst, aber sie dürfte die Invariante nicht verletzen.

Wurden Probleme bei dieser Aufgabe erwartet oder sollte es hier eigentlich ohne Probleme gehen.
Wir würden uns über eine Kleine Hilfestellung oder einen Tipp freuen.

Grüße,
Florian

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Lab4 - Task3 - Aufgabe 2.6

Beitrag von Nathan Wasser »

Wenn Aufgabe 2.5 zu bewältigen war, dann ist in Aufgabe 2.6 eigentlich nichts neues. Eventuell wurden die Invarianten aus Aufgabe 1 nicht alle korrekt eingeführt, sprich entweder zu stark (also falsch) oder zu schwach (also keine Hilfe beim Beweisen anderer Invarianten). Oder die Änderungen an der Methode add waren zu groß.

Eventuell kann ein Tutor helfen.

errt
Mausschubser
Mausschubser
Beiträge: 61
Registriert: 18. Okt 2012 19:12

Re: Lab4 - Task3 - Aufgabe 2.6

Beitrag von errt »

Zumindest haben wir nun schon verschiedenste Änderungen versucht, ohne hier weiter zu kommen oder einen Fehler finden zu können. Insbesondere haben wir an der Methode add wirklich nichts relevantes geändert, was hier Probleme bereiten sollte.
Einen Tutor haben wir heute bereits aufgesucht, der konnte uns aber nach einiger Suche auch nicht helfen, da das entsprechende Briefing noch nicht stattgefunden habe und ihm noch keine Musterlösung zur Verfügung stünde.

Benutzeravatar
mmi1991
Computerversteher
Computerversteher
Beiträge: 349
Registriert: 20. Okt 2011 18:46
Wohnort: Hattersheim

Re: Lab4 - Task3 - Aufgabe 2.6

Beitrag von mmi1991 »

Wir hatten ein ähnliches Problem…
Habt ihr an die Invariante gedacht, die besagt, dass je zwei verschiedene Instanzen zwei unterschiedliche Arrays referenzieren?
Ophasentutor SoSe 2014, WiSe 2015/16
Alle Angaben wie immer ohne Gewähr

errt
Mausschubser
Mausschubser
Beiträge: 61
Registriert: 18. Okt 2012 19:12

Re: Lab4 - Task3 - Aufgabe 2.6

Beitrag von errt »

Arrgh. Und dabei steht es drüber. Lesen müsste man halt können. Naja, danke auf jeden Fall, das löst das Problem. Kann mir jemand erklären, warum genau diese Invariante für diesen Beweis notwendig ist, für die anderen aber nicht?

Benutzeravatar
mmi1991
Computerversteher
Computerversteher
Beiträge: 349
Registriert: 20. Okt 2011 18:46
Wohnort: Hattersheim

Re: Lab4 - Task3 - Aufgabe 2.6

Beitrag von mmi1991 »

Sonst könnte man von Highscore erben, unter bestimmten Bedingungen eine neue Highscore-Instanz erzeugen und das eigene Arrayobjekt (das ist protected) auf dessen Arrayobjekt verweisen lassen.
Das würde nat. dafür sorgen, dass die Variable min inkonsistent sind.

Ich bin eher überrascht, dass KeY in der Lage ist, auch solch (zwar abstrusen, aber dennoch möglichen) Fälle zu beachten.
Ophasentutor SoSe 2014, WiSe 2015/16
Alle Angaben wie immer ohne Gewähr

Asfaloth
Windoof-User
Windoof-User
Beiträge: 27
Registriert: 7. Nov 2012 10:36

Re: Lab4 - Task3 - Aufgabe 2.6

Beitrag von Asfaloth »

Hallo,

ich bekomme die folgende Fehlermeldung bei KeY:

Code: Alles auswählen

Method created(maze.Highscore) not found!
Ich erhalte die Meldung, wenn ich das Array Highscores auf mehrere Instanzen prüfen will.

Hat jemand eine Idee, wie man das Problem lösen kann?

Danke,
Andreas

bekmel
Neuling
Neuling
Beiträge: 3
Registriert: 21. Feb 2013 18:09

Re: Lab4 - Task3 - Aufgabe 2.6

Beitrag von bekmel »

Hallo

Eine andere Frage...
Wie kann es sein, dass ein forall mit a >= b erfolgreich ist und ein zusätzliches exists mit den selben Rahmenbedingungen aber a == b fehlschlägt?
Forall mit a > b schlägt aber auch fehl :-/

Vielen Dank
Bekir

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Lab4 - Task3 - Aufgabe 2.6

Beitrag von Nathan Wasser »

Sagen wir mal es gilt a >= b. Daraus lässt sich weder schließen, dass a > b, noch a == b. Es muss zwar eins davon gelten, aber welches davon lässt sich erstmal nur daraus nicht ableiten.

Ähnliches gilt bei deiner Frage. Darüber hinaus ist aus deiner Frage nicht klar welche Variablen mit welchen Quantoren in welcher Reihenfolge vorkommen sollen, was das ganze noch etwas unklarer macht.

Antworten

Zurück zu „Archiv“