Funktion wird graud

qveXx
Mausschubser
Mausschubser
Beiträge: 64
Registriert: 2. Dez 2005 19:02

Funktion wird graud

Beitrag von qveXx »

Hallo,
beim Bearbeiten des Prak 3 ist folgende Sache aufgetreten:
Beim Ergänzen des letzten * wird aufeinmal die Funktion byte-add grau (anstatt grün) und das Lemma für byte-add is correct ebenfalls und die Möglichkeit es dann zu verifizieren ist nicht mehr gegeben.

Es blinkt vorher kurz zwischen blau und grau.

Ich habe beim letzten * im Vergleich zu den anderen * ein geschachteltes byte-add, kanns daran liegen?

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

Re: Funktion wird graud

Beitrag von aderhold »

qveXx hat geschrieben:Ich habe beim letzten * im Vergleich zu den anderen * ein geschachteltes byte-add, kanns daran liegen?
Das kann gut sein. Vereinfacht gesagt, bedeuten die Farben Folgendes: Bei einer grünen Prozedur wurde die Terminierung bewiesen. Bei einer blauen Prozedur liegt eine "Idee" zum Terminierungsnachweis vor, deren Korrektheit aber noch zu zeigen ist. Bei einer grauen Prozedur gibt es nicht einmal eine "Idee" zum Terminierungsnachweis.

Beispiel für eine graue Prozedur:

Code: Alles auswählen

function f(n : nat) : nat <=
f(n)
Ein geschachteltes byte-add ist zum Lösen der Aufgabe nicht erforderlich. Eine Umformulierung dieses "komplizierten" Falls sollte also helfen.

Benutzeravatar
m0ep
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 189
Registriert: 5. Okt 2006 22:52
Wohnort: Bensheim
Kontaktdaten:

Beitrag von m0ep »

Jup liegt am verschachtelten byte-add ... das gleiche hatte ich auch =)
Lasst mich Arzt, ich bin durch!

Predater
Neuling
Neuling
Beiträge: 6
Registriert: 10. Nov 2005 13:52
Wohnort: Groß-Zimmern

Beitrag von Predater »

Wir haben das selbe problem! Haben es sogar mit einer zusatzfunktion byte-add-overflow versucht allerdings immernoch das selbe prob mit den grauen funktionen!
Wo liegt den der ansatz dies ohne verschachtelung und ohne hilfsfunktion zu machen?
Schonmal vielen Dank für eure Mühe

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

Beitrag von aderhold »

Predater hat geschrieben:Wo liegt den der ansatz dies ohne verschachtelung und ohne hilfsfunktion zu machen?
Der Ansatz steht schon auf dem Übungsblatt:
  1. die höherwertigen Bits addieren (= 1 rekursiver Aufruf)
  2. den eventuell entstandenen Übertrag berücksichtigen.
Für Schritt 2 überlegt man sich, wie viel Übertrag bei der Addition zweier einzelner Bits maximal entstehen kann und wie man ihn mit einer von byte-add verschiedenen (schon vorhandenen) Funktion dazurechnen kann.

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

Beitrag von Christoph Walther »

m0ep hat geschrieben:Jup liegt am verschachtelten byte-add ... das gleiche hatte ich auch =)
Nur zur klarstellung: VeriFun kann auch mit geschachtelten rekursionen umgehen. Beispiel:

function g(x : nat) : nat <=
if ?0(x)
__then 0
__else if x > g(pred(x))
_______then g(g(pred(x)))
_______else *
______end_if
end_if

lemma g(x) = 0 <= all x : nat ?0(g(x))

Nur kann es eben gerade bei geschachtelten rekursionen passieren, daß eine hilfestellung durch den benutzer zum terminierungsnachweise solch einer prozedur erforderlich ist. Die aufgaben sind jedoch alle so gestaltet, daß VeriFun alles ohne benutzerinteraktion beweist, wenn die erforderlichen lemmata formuliert wurden. Wenn also jemand eine lösung mit geschachtelten prozeduren hinbekommt, dann ist das ok. Empfehlen würde ich solch einen versuch aber nicht, da dies sicher mehr arbeit macht, als zur lösung der aufgabe erforderlich ist.

Antworten

Zurück zu „Archiv“