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

[Oliver Bandel]

On Tue, Sep 27, 2005 at 04:09:23PM +0200, Axel Wei wrote:
[...]
>             / 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?
[...]

Bei funktionaler Programmierung hat man den Vorteil, daß es keine
Seiteneffekte gibt und dadurch kann man das sicher verifizieren.
Bei imperativem Programmieren ist es nicht sicher gestellt, daß
eine Funktion auch immer das selbe Resultat bringt, wenn man
sie mehrfach aufruft. DESWEGEN sind bzgl. Programmverifikation
die funktionalen Ansätze wichtig.



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

Aha, sehr interessanter Hinweis. :)


Gruß,
   Oliver