[linux-l] POSIX und busybox (was: Subtilitäten von find und xargs)

Oliver Bandel oliver at first.in-berlin.de
Sa Nov 17 12:16:59 CET 2007


Zitat von Steffen Dettmer <steffen at dett.de>:

[...]
>
> > Also quasi das Halteproblem von hinten aufgezäumt: Was ist mit
> > 100% verifizierbaren Programmen noch berechenbar?
>
> Na ja, das Halteproblem für Programme beliebiger Komplexität kann man
> immer lösen, wenn man dazu ein westenlich komplexeres Program nehmen
> kann.

Ja. Dann muss aber das komplexere Programm ggf. auch geprüft werden.
Da es komplexer ist, ist es möglicherweise wesentlich schwerer,
es zu prüfen. ;-)


> Im Extremfall, in der das wesentlich komplexere Program alle
> aufzählt (damit funktioniert der normale Haltsatz nicht, weil kein
> Programm das Halteprogramm selbst benutzen kann, weil es ja dann
> komplexer sein müsste, als das Halteentscheideprogramm, aber genau das
> Gegenteil war ja die Bedingung). Damit kann man also beliebig komplexe
> Algoritmen machen.

Denke ich auch.


Eigentlich müssten purely functional programs
komplett automatisch prüfbar sein.

Program-Verifizierer gibt es ja.
(Aber die können ja auch Bugs enthalten ;-))

Also ganz kann man dem Problem dann nicht entrinnen ;-)



Aber hier mal praktisch:


  http://coq.inria.fr/



Ciao,
   Oliver



Mehr Informationen über die Mailingliste linux-l