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

[Steffen Dettmer]

* Oliver Bandel wrote on Sat, Nov 17, 2007 at 12:16 +0100:
> 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.

Na gut, aber das geht logisch ja nicht. Wenn man auf NICHTS vertraut
oder aufbauen kann, kann man auch nichts damit machen :)

> Da es komplexer ist, ist es möglicherweise wesentlich schwerer,
> es zu prüfen. ;-)

na ja, und diese schwierigere Prüfung würdest Du auch wieder prüfen
wollen, stimmts? :)

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

Na ja, theoretisch kann man ja jeden endlichen deterministischen
Algorithmus (wobei endlich für mögliche Eingaben, Zustandsraum
[Laufzeit] und damit Ausgaben gilt) prüfen (und damit auch automatisch).
Man kann ja alles aufzählen und prüfen.

Praktisch geht das natürlich meistens überhaupt nicht, weil man dazu
dann Millarden von Jahren bräuchte oder sowas. Ein weiteres Problem ist
auch, dass man oft gar nicht so einfach alle möglichen Ausgaben
bestimmen kann (dazu macht man ja das Programm; könnte man es so prüfen,
bräuchte man es vielleicht gar nicht :)).

Allerdings sind die Eingaben viele Programme (logisch gesehen) 
unendlich (auch wenn natürlich der RAM etc begrenzt ist, man könnte ja
andere Maschine nehmen - eine unendliche, sofern man eine zur Hand hat).

Das kann man nicht mal theoretisch prüfen, weil man annimmt, dass keine
unendlich grossen Maschinen (Automaten) existieren :)

Bei deklarativen Sprachen (also z.B. funktionalen) kann man das Programm
einfacher prüfen, weil es ja den Lösungsweg gar nicht beschreibt,
sondern das Ergebnis. Praktikabel ist das aber wohl auch nur in
einfachen Anwendungen.

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

Ja, gibts sowas?

> Aber hier mal praktisch:
> 
>   http://coq.inria.fr/

Interessant. Hab mal angefangen, dass Tutorial zu lesen, bin aber nicht
allzuweit gekommen... Wie man ein Programm damit beweisen sollte, ist
mir unklar. Na ja, Programmbeweise sind wohl eh nur ein sehr
theoretisches Konstrukt :)

Für z.B. unit test Testfallerstellung (Klassenbildung oder sowas) soll
es auch Programme geben, aber Klassenbildung ist ja so schon nicht
trivial, kann mir nicht vorstellen, wie ein Programm das hinkriegen
will. Oder läuft das dann tausend Jahre, bis es durch ist? :)

oki,

Steffen

-- 
Dieses Schreiben wurde maschinell erstellt,
es trägt daher weder Unterschrift noch Siegel.