Tote Funktion in VeriFun

Steven
Kernelcompilierer
Kernelcompilierer
Beiträge: 425
Registriert: 2. Sep 2008 10:00
Wohnort: Frankfurt am Main

Tote Funktion in VeriFun

Beitrag von Steven »

Ich kann in VeriFun reproduzierbar eine Funktion anlegen, die ein graues Prozedur-Icon bekommt (VeriFun konnte also keine Maßterme erzeugen), bei der andererseits aber auch die Funktion "Set Termination" im Kontextmenü sowie im Hauptmenü deaktiviert ist. Der Code ist eigentlich recht simpel:

function divides2(a : nat, b : nat) : bool <=
if b > a
then divides(a, minus(b, a))
else if ?0(b)
then true
else if a = b
then true
else false
end_if
end_if
end_if

Das Verhalten ist 100%ig reproduzierbar - einfach den Code per Copy&Paste in VeriFun übertragen. Ist das ein Bug oder muss ich meine Maßterme hier anders angeben?

Nachtrag: Die verwendete Funktion divides sieht so aus und bekommt automatisch ein blaues Prozeduricon:

function divides(a : nat, b : nat) : bool <=
if a > b
then false
else if ?0(b)
then true
else divides(a, minus(b, a))
end_if
end_if

minus sieht so aus und wird ebenfalls automatisch blau:

function minus(a : nat, b : nat) : nat <=
if ?0(b)
then a
else if b > a
then 0
else pred(minus(a, pred(b)))
end_if
end_if

PS: Über Sinn und Unsinn dieses Konstrukts kann man natürlich diskutieren, die Terminierung sollte aber schon beweisbar sein :) Nach ein paar weiteren Versuchen glaube ich inzwischen recht fest an einebn Bug :shock:
Zuletzt geändert von Steven am 26. Mär 2009 12:02, insgesamt 1-mal geändert.

Benutzeravatar
Tigger
Kernelcompilierer
Kernelcompilierer
Beiträge: 404
Registriert: 26. Okt 2007 17:35
Wohnort: Hofheim
Kontaktdaten:

Re: Tote Funktion in VeriFun

Beitrag von Tigger »

Das Problem ist das deine Funktion divides für den Fall a=0 nicht terminiert.

Steven
Kernelcompilierer
Kernelcompilierer
Beiträge: 425
Registriert: 2. Sep 2008 10:00
Wohnort: Frankfurt am Main

Re: Tote Funktion in VeriFun

Beitrag von Steven »

Dann erkennt VeriFun also, dass ich eine Funktion benutze, deren Terminierung noch nicht bewiesen ist (divides) und zwingt mich erst dazu, das zu beweisen, bevor ich überhaupt mit dem Beweis der davon abhängigen Funktion (divides2) anfangen darf? Das macht Sinn, hätte ich so aber nicht vermutet. Klar, ich kann keinen Terminierungsbeweis von divides2 *abschließen*, ohne die Terminierung von divides zu zeigen, aber dass ich nicht mal anfangen darf...
PS: Dass das Beispiel sinnlos ist, ist klar. Mir ging es darum, was VeriFun daraus macht.

Benutzeravatar
Tigger
Kernelcompilierer
Kernelcompilierer
Beiträge: 404
Registriert: 26. Okt 2007 17:35
Wohnort: Hofheim
Kontaktdaten:

Re: Tote Funktion in VeriFun

Beitrag von Tigger »

Naja, wenn VeriFun zeigen will, dass eine Funktion terminiert, stellt es ja die Terminierungshypothese auf und versucht sie dann per Induktion zu beweisen. Bei divides kann er die Terminierungshypothese aufstellen (bedient sich dabei der terminierenden Prozesdur minus), scheitert aber am Beweis, da divides selbst nicht terminiert. Bei divides2 hingegen scheitert er bereits an der Aufstellung der Terminierungshypothesen, da Beweise nur mit terminierende Prozeduren geführt werden können (also nicht über divides). Deswegen wäre es hier auch überflüssig einen Maßterm anzugeben, da der Beweis sowieso nicht geführt werden könnte.

Der genaue Sachverhalt steht auf Folie 5 in Foliensatz 8.
Zuletzt geändert von Tigger am 26. Mär 2009 12:22, insgesamt 1-mal geändert.

xAx
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 157
Registriert: 6. Mär 2008 17:20

Re: Tote Funktion in VeriFun

Beitrag von xAx »

verifun braucht bei deiner divides2 nicht wirklich einen terminierungsbeweis: es gibt keinen rekursiven aufruf.
Nichts ist wie es scheint!
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
Zuletzt geändert von xAx am 14. Mär 2009 16:17, insgesamt 99-mal geändert.

Benutzeravatar
Tigger
Kernelcompilierer
Kernelcompilierer
Beiträge: 404
Registriert: 26. Okt 2007 17:35
Wohnort: Hofheim
Kontaktdaten:

Re: Tote Funktion in VeriFun

Beitrag von Tigger »

ok, ich VERMUTE das VeriFun zusätzlich zu den rekuriven Terminierungshypothesen auch Terminierungshypothesen für den Basisfall (also alle die keinen Rekursiven Aufruf enthalten) aufstellt, wobei hier die Bedingung ist, dass (wenn) nur terminierende Prozeduren aufgerufen werden. Andernfalls wäre es ja leicht möglich, die Terminnation von Prozeduren zu beweisen, die andere, nicht terminierende Prozeduren benutzen, nachzuweisen.
Zuletzt geändert von Tigger am 26. Mär 2009 12:49, insgesamt 2-mal geändert.

Steven
Kernelcompilierer
Kernelcompilierer
Beiträge: 425
Registriert: 2. Sep 2008 10:00
Wohnort: Frankfurt am Main

Re: Tote Funktion in VeriFun

Beitrag von Steven »

Tigger hat geschrieben:Edit: Fehler von mir, für nicht-rekursice Prozeduren gibt es tatsächlich keine Terminierungshypothesen.
Das ist merkwürdig. Es gilt: Wenn alle Terminierungshypothesen bewiesen wurden, terminiert die Prozedur. Die leere Menge von Aussagen ist immer wahr, also terminiert divides2, was aber nicht sein kann, da es divides aufruft, das nicht immer terminiert.

Benutzeravatar
Tigger
Kernelcompilierer
Kernelcompilierer
Beiträge: 404
Registriert: 26. Okt 2007 17:35
Wohnort: Hofheim
Kontaktdaten:

Re: Tote Funktion in VeriFun

Beitrag von Tigger »

Steven hat geschrieben:
Tigger hat geschrieben:Edit: Fehler von mir, für nicht-rekursice Prozeduren gibt es tatsächlich keine Terminierungshypothesen.
Das ist merkwürdig. Es gilt: Wenn alle Terminierungshypothesen bewiesen wurden, terminiert die Prozedur. Die leere Menge von Aussagen ist immer wahr, also terminiert divides2, was aber nicht sein kann, da es divides aufruft, das nicht immer terminiert.
Stimmt, deswegen habe ich o.g. Vermutung angestellt.

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

Re: Tote Funktion in VeriFun

Beitrag von Christoph Walther »

Steven hat geschrieben:Ich kann in VeriFun reproduzierbar eine Funktion anlegen, die ein graues Prozedur-Icon bekommt (VeriFun konnte also keine Maßterme erzeugen), bei der andererseits aber auch die Funktion "Set Termination" im Kontextmenü sowie im Hauptmenü deaktiviert ist.
Die systemverhalten ist ok (also kein bug) & wird auf seite 40 - 41 in

http://www.inferenzsysteme.informatik.t ... Oct-02.pdf

erklärt. "Set Termination" ist auf prozeduren mit status "ignored" nicht anwendbar. Dazu muß die prozedur mindestens den status "ready" erhalten.
Steven hat geschrieben:Dann erkennt VeriFun also, dass ich eine Funktion benutze, deren Terminierung noch nicht bewiesen ist (divides) und zwingt mich erst dazu, das zu beweisen, bevor ich überhaupt mit dem Beweis der davon abhängigen Funktion (divides2) anfangen darf?
Genauso ist es.
Steven hat geschrieben:Das macht Sinn, hätte ich so aber nicht vermutet.
Schade, daß sie sinnvolle sachen in VeriFun nicht vermuten :(

Antworten

Zurück zu „Archiv“