Ein Betriebssystem-Kernel mit Korrektheitsbeweis
-
Hallo,
habe gerade in ct einen kurzen Artikel darüber gelesen und hier gibt es mehr Info dazu. Mich würde interessieren, ob jemand die Korrektheitsbeweise beruflich oder aus Spass (:)) macht? Ich würde sagen, bringt doch alles nichts, heute eine Funktion geschrieben, morgen musste was ändern, später einen "Workaround" eingebaut usw.
-
Kann man das für ein HobbyOS einsetzen? Kostenloses Tool?
-
Naja, ob der Beweis korrekt ist?
Ich habe schon gehört, das Leute Doktor Arbeiten an Universitäten geschrieben haben. Und als jemand das als Diplom Arbeit umsetzen sollte hat er rausgefunden, das so nicht machbar war.
-
Ohja, ich erinnere mich ...
Es ist möglich, wenn sich alle Methoden an ein Schema halten, die Korrektheit jeder einzelnen Rückgabe zu überprüfen. Aber sogar automatisiert hat das enormen Zeitaufwand erfordert und parallelisierte Systeme unberücksichtigt gelassen.
Würde mich fast wundern, wenn die Fortschritte so enorm gewesen wären ...
-
Da fällt mir das schöne Zitat ein:
There are two ways of constructing a software design: One way is to make it so simple that there are obviously no deficiencies, and the other way is to make it so complicated that there are no obvious deficiencies. The first method is far more difficult.
C. A. R. Hoare
CACM 24(2) 1981, 75-83
-
Erhard Henkes schrieb:
Kann man das für ein HobbyOS einsetzen? Kostenloses Tool?
Das Tool heißt anscheinend Isabelle und auf der Seite kann man es herunterladen. Hm, ob man für dieses Tool auch einen Korrektheitsbeweis gemacht hat und wenn ja, mit welchem Tool...
-
abc.w schrieb:
Hm, ob man für dieses Tool auch einen Korrektheitsbeweis gemacht hat und wenn ja, mit welchem Tool...
Das Tool hat auch den ersten Compiler erstellt. Es nennt sich Mensch
-
abc.w schrieb:
Erhard Henkes schrieb:
Kann man das für ein HobbyOS einsetzen? Kostenloses Tool?
Das Tool heißt anscheinend Isabelle und auf der Seite kann man es herunterladen. Hm, ob man für dieses Tool auch einen Korrektheitsbeweis gemacht hat und wenn ja, mit welchem Tool...
Isabelle has a so-called LCF-style small kernel architecture. This means that the correctness of the whole system depends ultimately on a very small part of it, which must be trusted / verified by hand. Also, since Isabelle can generate proof terms, it's possible to check Isabelle proofs using an independent proof term checker if need be. There's no such thing as an absolute proof, of course, but a small kernel augmented with proof terms is the next best thing.