probleme mit verifun

baerchen
Computerversteher
Computerversteher
Beiträge: 382
Registriert: 24. Okt 2006 15:42

probleme mit verifun

Beitrag von baerchen »

ich kann in meinen statements, egal ob funktion oder lemma kein '=' benutzen. wenn ich das tue dann sagt mir verifun:

Code: Alles auswählen

Encountered "=0" at line x, column y.
Was expecting one of:
	<EOF>
	":" ...
wenn ichs durch ?0( .. ) ersetze dann funktionierts seltsamerweise.

ebenso scheint er nach eher zufälligem muster viele statements mit ähnlichen fehlermeldungen nicht zu akzeptieren, wenn ichs 1:1 nochmal abtippe funktioniert es dann von zeit zu zeit...

edit: verwende VeriFun3.2.2 unter kubuntu7.10
We can do this the hard way or my way ...which is basically the same thing!

Benutzeravatar
Maradatscha
Computerversteher
Computerversteher
Beiträge: 353
Registriert: 2. Okt 2006 18:53

Beitrag von Maradatscha »

Encountered "=0" <--- musst du ändern in "a = 0"
Lehrzeichen nicht vergessen! das könnte der Fehler sein

baerchen
Computerversteher
Computerversteher
Beiträge: 382
Registriert: 24. Okt 2006 15:42

Beitrag von baerchen »

ich gebe ja irgendwas in der form x = y ein. auch ob mit oder ohne leerzeichen macht keinen unterschied
We can do this the hard way or my way ...which is basically the same thing!

Simon Siegler
Computerversteher
Computerversteher
Beiträge: 369
Registriert: 16. Apr 2007 09:12

Beitrag von Simon Siegler »

Das Verhalten ist sicherlich nicht zufällig. Die Meldungen des Parsers sehen sich ähnlich, dennoch ist die konkrete Meldung und auch der konkrete Term notwendig, um nachvollziehen zu können, was daran fehlerhaft ist.

baerchen
Computerversteher
Computerversteher
Beiträge: 382
Registriert: 24. Okt 2006 15:42

Beitrag von baerchen »

zwischen jedes einzelne zeichen ein leerzeichen hilft. also beispielsweise statt all x,y:nat x=y
folgendes
all x , y : nat x = y
We can do this the hard way or my way ...which is basically the same thing!

Simon Siegler
Computerversteher
Computerversteher
Beiträge: 369
Registriert: 16. Apr 2007 09:12

Beitrag von Simon Siegler »

Das einzige Leerzeichen, dass dabei weggelassen werden kann, ist das vor dem ",". Alle anderen sind tatsächlich notwendig, da ":" und "=" auch innerhalb von Bezeichnern vorkommen könnten.

baerchen
Computerversteher
Computerversteher
Beiträge: 382
Registriert: 24. Okt 2006 15:42

Beitrag von baerchen »

ok im handbuch und insbesondere in den codebeispielen des tutorial stehts eben anders
We can do this the hard way or my way ...which is basically the same thing!

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

Beitrag von Christoph Walther »

baerchen hat geschrieben:ok im handbuch und insbesondere in den codebeispielen des tutorial stehts eben anders
Stimmt - beide sind für eine frühere systemversion geschrieben worden, aber wir haben bisher nicht die zeit für eine überarbeitung gefunden. Die sprachsyntax wurde geändert, dafür gibt es aber eine aktuelle beschreibung: "The L 1.0 Primer" auf der vf-seite unter "Download". Dort steht in kapitel 5.5 auch wann & wo man leerzeichen verwenden muß. Änderungen zum "User Guide" sind in "What's New in VeriFun" vermerkt (s. vf-seite unter "Download").

Das systemverhalten kann auch bei den Tutorial-Beispielen abweichen. Einfach hier im forum fragen, wenn man unsicher über das systemverhalten ist.

baerchen
Computerversteher
Computerversteher
Beiträge: 382
Registriert: 24. Okt 2006 15:42

Beitrag von baerchen »

hab probleme mit der ersetzung in negierten formeln.
ich habe in meinem beweis folgendes stehen:

hypothesen: b ist wahr, ¬ x = y
zielterm: ¬ f(x1) = y1

habe nun folgendes als lemma formuliert:
b ist wahr <=> f(x) = x
also in lemma-form:
lemma l1 <= all x : typ_x if{b, f(x) = x, ¬ f(x) = x}
l1 wird dann als wahr bewiesen

würde nun gerne machen:
¬ f(x1) = y1
(apply equation: l1)
¬ x1 = y1
true (da ¬ x1 = y1 ja schon bei den hypothesen steht)

was passiert is aber:
¬ f(x1) = y1
(apply equation: l1)
¬ f(if{b, f(x1) = x1, ¬ f(x1) = x1})= y1
(simplification: IH-1)
¬ f(x1) = y1

und ich bin wieder am anfang. was mach ich falsch?
We can do this the hard way or my way ...which is basically the same thing!

aderhold
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 212
Registriert: 21. Okt 2005 10:50

Beitrag von aderhold »

baerchen hat geschrieben:lemma l1 <= all x : typ_x if{b, f(x) = x, ¬ f(x) = x}

[...]

¬ f(x1) = y1
(apply equation: l1)
¬ f(if{b, f(x1) = x1, ¬ f(x1) = x1})= y1
(simplification: IH-1)
¬ f(x1) = y1
Hier muss sich ein Tippfehler eingeschlichen haben, denn das beschriebene Ergebnis nach "Apply Equation: l1" ist syntaktisch nicht korrekt. Der Goalterm müsste nach Anwendung der Gleichung f(x) = x aus l1 so aussehen:

¬ if{b, x1, f(x1)} = y1

Zur Erklärung: Apply Equation prüft nicht, ob die Vorbedingung b des Lemmas l1 tatsächlich erfüllt ist, sondern ersetzt f(x1) durch if{b, x1, f(x1)}. Wenn man nun noch nachweist, dass b erfüllt ist, vereinfacht sich der neue If-Ausdruck wie gewünscht zu x1 und man erhält ¬ x1 = y1. Wenn ¬ x1 = y1 bereits in den Hypothesen steht (im Posting war dagegen von ¬ x = y die Rede), sollte dieser Beweis gelingen.

Bevor "sollte gelingen" zu einem "wird gelingen" wird, muss man folgende Hindernisse aus dem Weg räumen:

1. Man muss die richtige Gleichung in der richtigen Richtung anwenden. Im Beispiel muss man also f(x) = x anwenden und nicht x = f(x).

2. Apply Equation muss an der richtigen Position angewendet werden. Dem zitierten Zwischenergebnis nach wurde möglicherweise x = f(x) an der Position des x1 angewendet. Richtig wäre dagegen, f(x) = x an der Position des f(x1) anzuwenden (denn das soll ja durch x1 ersetzt werden).

3. Die Vorbedingung b des anzuwendenden Lemmas muss wirklich erfüllt sein. Manchmal abstrahiert man im Kopf etwas zu viel (oder auch falsch) und meint nur, dass Vorbedingung b schon gezeigt wurde, obwohl noch ein (subtiler) Unterschied zwischen "Haben" und "Benötigen" ist.

4. Manchmal kann es passieren, dass VeriFun in der Simplification nach Apply Equation oder Use Lemma die Lemma-Anwendung im Wesentlichen "rückgängig" macht. Vielleicht ist das verwendete Lemma nicht hilfreich und wird deswegen "wegoptimiert". Sicherheitshalber kann man diese Simplification mit Prune abschneiden (nicht jedoch das Apply Equation) und mit Weak Normalization den Goalterm vereinfachen lassen, ohne dass VeriFun hierzu Lemmas oder Induktionshypothesen verwendet (siehe S. 73 im VeriFun User Guide).

Generell sollte es zur Lösung der Praktischen Übung 3 nicht notwendig sein, Lemmas von Hand anzuwenden. Wie in der Hörsaalübung demonstriert, sollte man nach Verifikation eines Hilfslemmas den noch offenen Beweisversuch des Ziellemmas komplett abschneiden und mit Verify neu starten, damit VeriFun selbstständig das Hilfslemma anwendet.

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

Beitrag von Christoph Walther »

baerchen hat geschrieben:hab probleme mit der ersetzung in negierten formeln.
Man kann nicht erkennen, was in dem beispiel gegeben ist und was gezeigt werden soll. Also einfach die definitionen der verwendeten prozeduren und lemmata mit dem 'Copy' befehl aus dem Program Menue kopieren und in das posting pasten. Dazu das lemma, das bewiesen werden soll.

Dann sehen wir weiter.

baerchen
Computerversteher
Computerversteher
Beiträge: 382
Registriert: 24. Okt 2006 15:42

Beitrag von baerchen »

Das ist der Zielterm:

Code: Alles auswählen

if{even(x1),
  if{even(y1), ¬ nat2byte(half(x1)) = nat2byte(half(y1)), true},
  if{even(y1), true, ¬ nat2byte(half(x1)) = nat2byte(half(y1))}}
Das sind die Hypotheses:

Code: Alles auswählen

¬ -(x1) = -(y1)
?+(y1)
?+(x)
Und das das Lemma:

Code: Alles auswählen

lemma unequal_nat2byte <= all x, y : nat
  if{¬ nat2byte(x) = nat2byte(y), ¬ x = y, true}
Soll ausdrücken nat2byte(x) != nat2byte(y) -> x != y

Und das die Folge der Anwendung:

Code: Alles auswählen

if{even(x1),
  if{even(y1),
    if{
     if{¬ nat2byte(half(x1)) = nat2byte(half(y1)),
       ¬ half(x1) = half(y1),
       true},
     ¬ nat2byte(half(x1)) = nat2byte(half(y1)),
     true},
    true},
  if{even(y1), true, ¬ nat2byte(half(x1)) = nat2byte(half(y1))}}
We can do this the hard way or my way ...which is basically the same thing!

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

Beitrag von Christoph Walther »

baerchen hat geschrieben:Und das das Lemma:

Code: Alles auswählen

lemma unequal_nat2byte <= all x, y : nat
  if{¬ nat2byte(x) = nat2byte(y), ¬ x = y, true}
Soll ausdrücken nat2byte(x) != nat2byte(y) -> x != y
Dieses lemma ist unbrauchbar, da es keine spezifische aussage über die prozedur 'nat2byte' trifft. Das lemma hat die form: "¬ nat2byte(x) = nat2byte(y) -> ¬ x = y", und als kontraposition geschrieben "x = y -> nat2byte(x) = nat2byte(y)". "x = y -> f(x) = f(y)" gilt aber für jede funktion f, nicht nur für 'nat2byte'.

Beispiel: Für "function f(x : nat) : nat <= * " (* = star) können Sie auch

lemma unequal_f <= all x, y : nat if{¬ f(x) = f(y), ¬ x = y, true}

beweisen, obwohl man über 'f' garnichts weiß!

Ihr lemma kann Ihnen also nicht bei der verifikation des byte-adders helfen. Man sieht das auch daran, daß VeriFun den ausdruck (*)

if{even(x1),
if{even(y1),
if{if{¬ nat2byte(half(x1)) = nat2byte(half(y1)),
¬ half(x1) = half(y1),
true},
¬ nat2byte(half(x1)) = nat2byte(half(y1)),
true},
true},
if{even(y1), true, ¬ nat2byte(half(x1)) = nat2byte(half(y1))}}

zu (**)

if{even(x1),
if{even(y1), ¬ nat2byte(half(x1)) = nat2byte(half(y1)), true},
if{even(y1), true, ¬ nat2byte(half(x1)) = nat2byte(half(y1))}}

vereinfacht. Kurzum, Sie haben das problem durch ein unbrauchbares lemma komplizierter gemacht, und VeriFun vereinfacht die sache wieder. Finden Sie lemmata, die spezifisch für die prozeduren sind.

Aber: (**) können Sie sowieso nicht beweisen. Wenn Sie den Disprover darauf anwenden, so erhalten Sie ein gegenbeispiel - die aussage (**) - und damit auch (*) - ist falsch. Es muß also irgendwo ein fehler stecken - entweder in Ihren prozedurdefinitionen oder in Ihren lemmata.

baerchen
Computerversteher
Computerversteher
Beiträge: 382
Registriert: 24. Okt 2006 15:42

Beitrag von baerchen »

dankeschön für die ausführliche antwort. hatte mich schon über den einfachen beweis gewundert.

** sollte allerdings durchaus richtig sein, es gelten ja noch die hypothesen von oben
We can do this the hard way or my way ...which is basically the same thing!

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

Beitrag von Christoph Walther »

baerchen hat geschrieben:** sollte allerdings durchaus richtig sein, es gelten ja noch die hypothesen von oben
Die hypothesen hatte ich beim test übersehen.

Antworten

Zurück zu „Archiv“