[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