Seite 1 von 1

Tote Funktion in VeriFun

Verfasst: 26. Mär 2009 11:42
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:

Re: Tote Funktion in VeriFun

Verfasst: 26. Mär 2009 12:00
von Tigger
Das Problem ist das deine Funktion divides für den Fall a=0 nicht terminiert.

Re: Tote Funktion in VeriFun

Verfasst: 26. Mär 2009 12:06
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.

Re: Tote Funktion in VeriFun

Verfasst: 26. Mär 2009 12:17
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.

Re: Tote Funktion in VeriFun

Verfasst: 26. Mär 2009 12:21
von xAx
verifun braucht bei deiner divides2 nicht wirklich einen terminierungsbeweis: es gibt keinen rekursiven aufruf.

Re: Tote Funktion in VeriFun

Verfasst: 26. Mär 2009 12:30
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.

Re: Tote Funktion in VeriFun

Verfasst: 26. Mär 2009 12:44
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.

Re: Tote Funktion in VeriFun

Verfasst: 26. Mär 2009 12:51
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.

Re: Tote Funktion in VeriFun

Verfasst: 26. Mär 2009 13:30
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 :(