* Martin Uecker wrote:
> On Wed, Feb 12, 2003 at 09:56:41PM +0000, Lutz Donnerhacke wrote:
>> > Letzteres ist auch bei abstrakter ("hochsprachlicher") Formulierung
>> > aufwendig bis unm�glich, ersteres wird nicht wesentlich aufwendiger.
>>
>> Eine formale Verifizierung der Abwesenheit von Fehlerklassen (bis hin zur
>> Abwesenheit aller Laufzeitfehler) ist heute schon m�glich und wird gemacht.
>> Jedoch kaum bei Open Source.
>
> Eigentlich nie, oder kennst Du ein Beispiel?
Das CA System von Mondex, Hubschrauber, Rakten und Flugtechnik.
> Aber Verifiziert wird auch seltenst bei Closed Source.
Das ist ein anderer Punkt.
> Und selbst dann hei�t "Abwesenheit aller Laufzeitfehler" auch nur, da�
> die Runtime-Umgebung nicht kollabiert, und keineswegs, da� das Programm
> zur Laufzeit keine Schei�e baut.
Es sind drei Schritte:
- Abwesenheit von Laufzeitfehler hei�t: Keine Bereichs�berschreitungen
f�r Feldgrenzen, �berl�ufe in der Arithmetik, keine Division durch Null,
etc. pp. Das kann man maschinell beweisen.
- Partielle Korrektheit. Das kann man maschinell beweisen.
- Totale Korrektheit. Das ist nach der partiellen Korrektheit leichter,
wird nicht maschinell angeboten.
Maschineller Beweis hei�t, da� man ca. 90% des Codes als Korrekt abharken
kann und der Rest mit konktreten Randbedingungen hochschl�gt.
> Programmen in einer Ada-Variante die Abwesenheit von Fehlern zu beweisen
> bringt IMHO wesentlich weniger, als von vornehein eher deklarative
> Programmiersprachen zu benutzen und die Zeit besser in deren Optimierung
> zu stecken.
;-) YMMV.
