Praktische Übung 4: qsort sorts lemma

Benutzeravatar
Gnomix
Computerversteher
Computerversteher
Beiträge: 306
Registriert: 31. Okt 2005 08:44

Praktische Übung 4: qsort sorts lemma

Beitrag von Gnomix »

Ist das Lemma korrekt ?
Denn ich bekomme vom Disprover alle Teilbäume als false angezeigt, wenn ich die Äste, die blau bleiben damit überprüfe.

Christoph Walther
Dozentin/Dozent
Beiträge: 86
Registriert: 1. Nov 2005 18:51

Re: Praktische Übung 4: qsort sorts lemma

Beitrag von Christoph Walther »

Ein lemma ist falsch, wenn das lemma den zustand 'falsified' erhält. Dies erkannt man an der rot-färbung des lemma-icons im Program Viewer. Falls dies bei Ihnen der fall ist, so haben sie mindestens eine der hilfsprozeduren falsch implementiert.

Der Disprover ersetzt alle allquantifizierten variablen eines lemmas durch konkrete werte (= konstruktorgrundterme), für die das lemma nicht gilt. Anders gesagt: Der Disprover erzeugt einen test, der scheitert, denn diese instanz des lemmas kann zu 'false' ausgewertet werden. Um herauszubekommen, wo Ihr fehler steckt, können Sie folgendermaßen vorgehen:

Doppelklick auf einen vom Disprover erzeugten 'refute!'-knoten im Proof Window - dadurch wird der Evaluation Viewer geöffnet, und Sie sehen eine instanz des lemmas, die falsch ist. Durch drücken des 'Down'-buttons (bzw. pfeil-nach-unten) im Evaluation Viewer sehen Sie schritt für schritt, wie die lemmainstanz zu 'false' ausgerechnet wird. Wenn Sie dabei die ergebnisse dieser berechnungen mit Ihren erwartungen vergleichen, so finden Sie den fehler in Ihrer implementierung der hilfsprozeduren.

Benutzeravatar
MisterD123
Geek
Geek
Beiträge: 811
Registriert: 31. Okt 2006 20:04
Wohnort: Weiterstadt

Re: Praktische Übung 4: qsort sorts lemma

Beitrag von MisterD123 »

seine frage bezog sich glaube ich mehr auf "ist das lemma korrekt vorgegeben" - ich würde aber auch mal tippen, dass eher die prozeduren falsch sind ;)

Benutzeravatar
Gnomix
Computerversteher
Computerversteher
Beiträge: 306
Registriert: 31. Okt 2005 08:44

Re: Praktische Übung 4: qsort sorts lemma

Beitrag von Gnomix »

Vielen Dank für die Hinweise. Ich werde meinen Fehler suchen und falls ich ihn nicht beheben kann weitere Fragen stellen.

Benutzeravatar
Gnomix
Computerversteher
Computerversteher
Beiträge: 306
Registriert: 31. Okt 2005 08:44

Re: Praktische Übung 4: qsort sorts lemma

Beitrag von Gnomix »

Also ich habe zwar einen Fehler in larger entdeckt,
da diese Funktion nicht einfach nur die größeren Elemente zurückgab,
sondern auch die gleichen. :oops:
Allerdings hat mich das nicht wirklich weiter gebracht,
ich kann jetzt sogar das Lemma "qsort_sorts lemma" mit dem Disprover direkt widerlegen. :shock:

Ich habe sogar von ganz vorne nochmal angefangen. :cry:

Pyron
Windoof-User
Windoof-User
Beiträge: 36
Registriert: 17. Dez 2005 17:15
Wohnort: Darmstadt

Re: Praktische Übung 4: qsort sorts lemma

Beitrag von Pyron »

Das "Qsort sorts lemma" war bei mir anfangs auch nicht zu beweisen und der Disprover arbeitete gegen mich,
aber ich hatte meine Fehler nicht in der larger/smaller-Prozedur, sondern in den n "kleiner gleich" Liste - und n "größer gleich" Liste - Prozeduren. "Größer gleich" sei nun mit diesem Symbol auf Aufgabe 4.1.c) ersetzt ;)
Überprüfe doch diese ebenfalls auf ihre Richtigkeit.

Ich hänge nun beim Qsort sorts und finde keine Lemmata, die mir weiterhelfen..

Viel Erfolg

Benutzeravatar
Gnomix
Computerversteher
Computerversteher
Beiträge: 306
Registriert: 31. Okt 2005 08:44

Re: Praktische Übung 4: qsort sorts lemma

Beitrag von Gnomix »

Also ich habe jetzt alle meine Funktionen mit Eingaben getestet, mit Hilfe des Interpreters. :|

Dabei habe ich etwas lustiges festgestellt, die natürlichen Zahlen gehen nur bis 42. :shock:

Ich konnte nicht feststellen, dass eine meiner Funktionen falsch sein sollte. :?

Mspringer
Nerd
Nerd
Beiträge: 555
Registriert: 19. Okt 2006 14:41
Wohnort: Darmstadt / Alzenau
Kontaktdaten:

Re: Praktische Übung 4: qsort sorts lemma

Beitrag von Mspringer »

Wenn die Lemmas immer noch disproovebar sind, dann sind deine Funktionen immer noch falsch. Bei uns hats jedenfalls funktioniert, alles zu beweisen.

Als Tipp könntest du dir auch mal eine alte Diplomarbeit eines Assistenten ansehen.

Benutzeravatar
Gnomix
Computerversteher
Computerversteher
Beiträge: 306
Registriert: 31. Okt 2005 08:44

Re: Praktische Übung 4: qsort sorts lemma

Beitrag von Gnomix »

Danke für den Tipp.
Meinen Fehler habe ich gefunden. Ich hatte "kleiner-gleich" zu umständlich modelliert.
Ich hatte statt einfach "nicht größer", tatsächlich "kleiner oder gleich" modelliert, was im restlichen modell zu einem Fehler führte.

Allerdings frage ich mich, wenn die Aufgabe Thema einer Diplomarbeit war, ist dass dann nicht zuviel für ein Praktikum?

Mspringer
Nerd
Nerd
Beiträge: 555
Registriert: 19. Okt 2006 14:41
Wohnort: Darmstadt / Alzenau
Kontaktdaten:

Re: Praktische Übung 4: qsort sorts lemma

Beitrag von Mspringer »

Naja Thema der Diplomarbeit war ja Gerneralisierung. Aber einige interessante Abschnitte fürs Praktikum sind auch drin gewesen ;)

Benutzeravatar
Gnomix
Computerversteher
Computerversteher
Beiträge: 306
Registriert: 31. Okt 2005 08:44

Re: Praktische Übung 4: qsort sorts lemma

Beitrag von Gnomix »

Achso, ok, ich dachte die Sache mit Quicksort wäre ein Hauptteil gewesen.

Das mit Qsort habe ich jetzt auch hinbekommen, nachdem ich ein paar hilfslemmas erzeugt habe und dann noch mal generalisiert habe.

Allerdings komme ich bei der Sache mit Permutation nicht ganz zurecht, ich verstehe schon, was ungefähr gemacht werden soll, aber dazu habe ich schon einen neuen Thread eröffnet, da es eine andere Aufgabe ist.

Antworten

Zurück zu „Archiv“