Lutz Donnerhacke:
[Verifikation]
> > 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.
Abdeckung im Bezug auf was? Lines of Code? Nett aber eher uninteressant da man
dergleichen durch klassische Tests mit coverage-Analyse auch erreicht.
Im Bezug auf Fehlerklassen? Glaube ich nicht. Bzw. habe bei den SPARKs hierzu
nichts gefunden was einem Beweis dieser Aussage auch nur nahe kommt. Und ohne
Beweis ist so eine Aussage eher wertlos.
> 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.
Wenn man automatisiert so weit kommt w�re dies �u�erst wertvoll. Ich w�rde
ohne einen Beweis dieser These aber Magenschmerzen bekommen.
> > Hast Du Pointer auf "aktuelles"?
>
> www.sparkada.com
Den pointer auf die selbst �berpr�fbare "Demo" habe ich �bersehen. Nach kurzem
Querlesen bin ich wirklich beeindruckt, wieviele tolle Dinge damit gemacht
wurden. Nach etwas l�ngerem Querlesen f�llt mir auf da� sie zumindest ein
gutes Marketing haben. Ebenfalls �bersehen habe ich wohl den Part in welchem
sie Regress zusichern, sollten ihre claims �bertrieben sein.
Zusammengefasst - es sieht den letzten 50 magic bullets leider recht �hnlich.
> >> Jedoch kaum bei Open Source.
> >
> > *g* work vs. fun...
>
> Es ist Fun, zuverl�ssige Software zu schreiben. Es ist noch mehr Fun,
Nicht wenn man zun�chst zu toolmonger mutieren mu� ;).
> bewiesenerma�en partiell korrekte Software zu schreiben (das leistet SPARK
> nur, wenn man formale Specs baut, z.B. in Z)
Man m�chte bewiesenerma�en korrekte Software schreiben. Alles andere scheint
mir eher formalisierter Selbstbetrug, sorry.
Gr��' G�del von mir,
Dietz
