H
Hanno Foest
Guest
Am 22.12.22 um 12:42 schrieb Volker Bartheld:
Da passieren sie ansonsten noch zusätzlich. Die ganzen restlichen Fehler
loszuwerden halte ich schon für recht praktisch.
\"Sound\" heiÃt in diesem Kontext soviel wie \"logisch korrekt\", was
\"unsound\" heiÃt dürfte damit dann auch klar sein. Ist nicht so toll,
aber wenns nicht anders geht... ich denk mal, wenn man den Aufrià macht,
auch nur für ein Subset der möglichen Eingeben formal zu verifizieren,
wird vielleicht auch noch ein wenig Zeit dafür übrig sein, sich Gedanken
zu machen, ob der Rest in der Praxis wirklich ausgeschlossen ist.
Hanno
--
The modern conservative is engaged in one of man\'s oldest exercises in
moral philosophy; that is, the search for a superior moral justification
for selfishness.
- John Kenneth Galbraith
Es gibt schon ein paar formal verifizierte Kernel, Compiler und
Betriebssysteme. \"Simpel\" würde ich die nicht mehr nennen.
These techniques can be sound, meaning that the verified properties can
be logically deduced from the semantics, or unsound, meaning that there
is no such guarantee.
Genau. Auch kannst Du z. B. mit Simulink ein Modell entwickeln und Dir
das - unter der Annahme, daà Simulink fehlerfrei sei und ebenfalls Dein
Modell - in ausführbaren Code compilieren lassen. Da passieren die
Fehler dann eben auf einer Metaebene höher.
Da passieren sie ansonsten noch zusätzlich. Die ganzen restlichen Fehler
loszuwerden halte ich schon für recht praktisch.
\"A sound technique yields a result only once it has
covered the entire space of possibilities. An example of an unsound
technique is one that covers only a subset of the possibilities, for
instance only integers up to a certain number, and give a \"good-enough\"
result.\"
Letzteres finde ich eher mau... Korrekt ist die Software doch erst dann,
wenn sie für ALLE MÃGLICHEN Eingaben (und nicht nur alle erwarteten
Eingaben) das jeweils korrekte Ergebnis liefert.
Vielleicht schlieÃt man hier implizit die Existenz eines Filters ein und
setzt \"mögliche Eingaben\" = \"erwartete Eingaben\". Klassischer Fallstrick
bei Buffer Overflows und SQL Injection.
\"Sound\" heiÃt in diesem Kontext soviel wie \"logisch korrekt\", was
\"unsound\" heiÃt dürfte damit dann auch klar sein. Ist nicht so toll,
aber wenns nicht anders geht... ich denk mal, wenn man den Aufrià macht,
auch nur für ein Subset der möglichen Eingeben formal zu verifizieren,
wird vielleicht auch noch ein wenig Zeit dafür übrig sein, sich Gedanken
zu machen, ob der Rest in der Praxis wirklich ausgeschlossen ist.
Hanno
--
The modern conservative is engaged in one of man\'s oldest exercises in
moral philosophy; that is, the search for a superior moral justification
for selfishness.
- John Kenneth Galbraith