D120.de/forum

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

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.

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 ..."