* Dietz Proepper wrote: >> Eine formale Verifizierung der Abwesenheit von Fehlerklassen (bis hin zur >> Abwesenheit aller Laufzeitfehler) ist heute schon m�glich und wird gemacht. > > Das Ganze war auch schon von 15 Jahren m�glich und wurde (zumindest auf > dem Papier) auch gemacht. Leider kann man einfach zeigen das "alle" > automatisch nicht geht. Schon sind wir wieder bei harter Handarbeit, > diese ist fehlertr�chtig und keine prinzipielle Verbesserung �ber > "n-Augen".
Ich rede von einem automatisierten Beweis der Laufzeitfehlerfreiheit, der eine Abdeckung von �ber 90% erreicht. Die wenigen Zeilen, die in solchen Prjekten dann noch �brigbleiben werden mit klaren Randbedingungen angegeben, so da� man sich �berlegen kann, ob es wirklich notwendig ist, den 32bit Sekundenz�hler der Uptime eines medizinischen Ger�ts tats�chlich auf �berlauf zu testen. > Hast Du Pointer auf "aktuelles"? www.sparkada.com >> Jedoch kaum bei Open Source. > > *g* work vs. fun... Es ist Fun, zuverl�ssige Software zu schreiben. Es ist noch mehr Fun, bewiesenerma�en partiell korrekte Software zu schreiben (das leistet SPARK nur, wenn man formale Specs baut, z.B. in Z)
