[linux-l] Verifizierbarkeit bei Rekursion (was: FP/Java vs. OCaml)

[Axel Weiß]

Am Dienstag, 27. September 2005 13:11 schrieb olafBuddenhagen at gmx.net:
> Verifikation ist bei imperativen Sprachen schwierig,
> aber mit gewissen Einschränkungen machbar. Wenn man auf Rekursion und
> noch irgendwas verzichtet, ist ADA verifizierbar.

Hi Olaf,

ist der Verzicht auf Rekursion denn Voraussetzung für Verifizierbarkeit? 
Wo hast Du das denn her?

Ich war bisher immer der Meinung, dass sich rekursive Funktionen 
generell leichter verifizieren lassen als nichtrekursive, sind sie doch 
eine Untermenge[1]. Ich will dabei mal voraussetzen, dass die 
Mathematik, gegen die zu verifizieren ist, ebenfalls rekursiv dasteht, 
sonst macht das ja wenig Sinn. Z.B. für den größten gemeinsamen Teiler 
zweier Zahlen:

            / b               falls a = 0
ggt(a,b) = {
            \ ggt(b mod a, a) sonst

Das ist die Mathematik, hübsch beweisbar. In C sieht das etwa so aus:

unsigned ggt(unsigned a, unsigned b){
	if (a == 0) return b;
	return ggt(b % a, a);
}

Sieht irgendwie ziemlich ähnlich aus, oder? Kann man das verifizieren?

			Axel

[1] Jede rekursive Funktion lässt sich nichtrekursiv aufschreiben, 
umgekehrt geht das aber nicht immer.

-- 
Humboldt-Universität zu Berlin
Institut für Informatik
Signalverarbeitung und Mustererkennung
Dipl.-Inf. Axel Weiß
Rudower Chaussee 25
12489 Berlin-Adlershof
+49-30-2093-3050
** www.freesp.de **