1. Praktikum: Wann bin ich fertig mit dem Beweis?

PaddyG
Mausschubser
Mausschubser
Beiträge: 50
Registriert: 9. Okt 2009 10:29

1. Praktikum: Wann bin ich fertig mit dem Beweis?

Beitrag von PaddyG »

Hallo,

eine kurze Frage zu den Praktika:

Wenn ich VeriFun dazu "überreden" kann, alles grün anzuzeigen, mir also der Beweis attestiert wird, bin ich dann definitv fertig und ist der Beweis mathematisch korrekt?

Oder könnte es sein, dass man VeriFun täuscht, indem man Dinge erfindet oder wegfallen lässt?
Bzw. wie sieht dass dann im Testat aus?

Gruß
Patrick

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

Re: 1. Praktikum: Wann bin ich fertig mit dem Beweis?

Beitrag von Christoph Walther »

PaddyG hat geschrieben:Wenn ich VeriFun dazu "überreden" kann, alles grün anzuzeigen, mir also der Beweis attestiert wird, bin ich dann definitv fertig ...
Ja.
PaddyG hat geschrieben: ... und ist der Beweis mathematisch korrekt? Oder könnte es sein, dass man VeriFun täuscht, indem man Dinge erfindet oder wegfallen lässt?

Wenn es nicht so wäre, so wäre VeriFun fehlerhaft. Denn zur spezifikation des systems gehört, daß alle lemmta, die bewiesen wurden (=> grün) auch wahr sind im sinne der semantik von L (=> Kapitel 12).

Ob die implementierung korrekt ist, ist streng genommen nicht bekannt. Dies würde eine verifikation des gesamtsystems erfordern. Bei erfolg hätte man dann korrektheit, natürlich relativ zur korrekten implementierung von JAVA, des verwendeten betriebssystems und der zugrunde liegenden hardware.

Das einzige, was mit sicherheit gesagt werden kann, ist, daß es noch niemandem gelungen ist ein falsches lemma mit dem aktuellen system zu beweisen. Vor jahren hatten wir einen fehler in der Induktionsregel. Damit war es tatsächlich möglich ein falsches induktionsaxiom zu formulieren, mit dem dann ein falsches lemma bewiesen werden konnte.

Sollten Sie es tatsächlich schaffen eine aufgabe mit hilfe eines falschen lemmas zu lösen, dann wird Ihnen daraus kein strick gedreht. Im gegenteil, dann bekommen sie noch einen extra bonus für ihre klausurnote, versprochen.

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

Re: 1. Praktikum: Wann bin ich fertig mit dem Beweis?

Beitrag von Nathan Wasser »

PaddyG hat geschrieben:Wenn ich VeriFun dazu "überreden" kann, alles grün anzuzeigen
Wenn Sie es schaffen, ok, aber bei Aufgabe 1.1(d) würde ich nicht versuchen das Lemma zu beweisen, sondern tun was in der Aufgabenstellung steht: "Widerlegen Sie das Lemma ..."

Antworten

Zurück zu „Archiv“