Bugs in der STL
-
@nwp3
Dein getKmInM zeigt finde ich ganz gut das eigentliche Problem.
Das kann man in C++ nämlich sehr einfach "sicher" hinbekommen. Indem man Längen nicht als Integers behandelt, sondern einen eigenen Typ dafür macht.Jetzt kannst du natürlich argumentieren "ja, aber C++ lässt es mich eben auch falsch schreiben". Und genau das ist das Problem: jede Sprache wird dich "falsche" Dinge hinschreiben lassen, die formal korrekt sind. Weil die Frage ob etwas "falsch" ist davon abhängt was man haben wollte. Und die Programmiersprache kann das ja schlecht wissen. Wüsste sie es, dann müsste man ja nichts mehr programmieren.
-
Achjeh...
Bashar schrieb:
Die Definition von Korrektheit ist, dass das Verhalten einer vorgegebenen Funktion entspricht.
Ja, genau da liegt der Hund begraben.
Die "vorgegebenen Funktion" muss erstmal exakt formuliert werden.
Und wie nennt man das? Das nennt man Programm. (OK, man kann es auch anders nennen, Algorithmus, Formel - whatever. Macht aber keinen echten Unterschied - ist im Endeffekt alles das selbe.)Deine Argumentation läuft auf "works as implemented == korrekt" hinaus.
Mit dieser Definition von korrekt kann ich aber nichts anfangen, die ist für nix gut.
-
hustbaer schrieb:
Achjeh...
Bashar schrieb:
Die Definition von Korrektheit ist, dass das Verhalten einer vorgegebenen Funktion entspricht.
Ja, genau da liegt der Hund begraben.
Die "vorgegebenen Funktion" muss erstmal exakt formuliert werden.
Und wie nennt man das? Das nennt man Programm. (OK, man kann es auch anders nennen, Algorithmus, Formel - whatever. Macht aber keinen echten Unterschied - ist im Endeffekt alles das selbe.)Doch, das macht einen grundlegenden Unterschied, weil ein Algorithmus effektiv und normalerweise auch effizient sein muss. Siehe mein Sortierbeispiel. Es gibt viele Probleme, deren Lösung einfach zu definieren aber schwer zu finden ist.
-
Mann Jungs, das einzig interessante hier im Thread war doch, ob knivil auch nur mit Wasser kocht (nachdenken und testen). Ob er das Resultat als fehlerfrei betrachtet oder auch nicht ist doch völlig Rille für unser aller weiteres Vorgehen.
Um hier wirklich eine fruchtbare Diskussion auf theoretisch abstraktem Niveau zu führen, denkt doch ein jeder (ich nehme mich da nicht aus) zu wenig über seine Kommentare nach und dann verliert sich alles in punktuellen Korrekturen etc...
Ist es nicht genug?
-
knivil schrieb:
freien Wildbahn
Haeh? Es gibt mindestens eine Firma, die in ausgewaehlten Bereichen die Fehlerfreiheit wahrscheinlich garantieren kann: http://corp.galois.com/ . Ich arbeite nicht dort, deswegen ist das keine sichere Aussage.
Können sie oder können sie nicht?
Ein wahrscheinlich ist ein bisschen schwach
Die Webseite lädt bei mir aber nicht, was nicht unbedingt für Fehlerfreiheit spricht PS:
Du behauptest fehlerfreie Software wäre kein Problem, aber ein Beispiel für Fehlerfreie Software liefern kannst du nicht. Mhm...
-
Du behauptest fehlerfreie Software wäre kein Problem
Nein, das behaupte ich nicht. Ich widerspreche der Aussage, das fehlerfreie Software nicht unmoeglich ist, und in speziellen Faellen wenig Aufwand bedeutet. Diese speziellen Faelle sind nicht trivial und sehr verschieden von "Hello World".
aber ein Beispiel für Fehlerfreie Software liefern kannst du nicht.
Bspw. Space Shuttle Software. So, aber das ist nicht die Software von der ich eigentlich nicht rede oder reden moechte, da die verfuegbaren Ressourcen fuer das Projekt nicht mit einem Kalibriertool bspw. korrelieren.
knivil auch nur mit Wasser kocht
Nee, es geht mir nicht um mich. Euch anscheinend schon. Das Beispiel kommt aus meiner "Erfahrung" und ihr wollt mir nachweisen, dass ich halluziniere. Es geht auch nicht um immer und allgemein auch nicht.
Was soll der Scheiss, warum wird mein Standpunkt absichtlich verzerrt? Nur damit eurer Gebasche besser passt ... Hand hoch, wer Software fuer Medizinprodukte herstellt!
Die Webseite lädt bei mir aber nicht, was nicht unbedingt für Fehlerfreiheit spricht
Ich haette gern einen formalen Beweis, dass die Seite bei dir nicht laedt. Ich glaube du halluzinierst.
-
knivil schrieb:
Bspw. Space Shuttle Software. So, aber das ist nicht die Software von der ich eigentlich nicht rede oder reden moechte, da die verfuegbaren Ressourcen fuer das Projekt nicht mit einem Kalibriertool bspw. korrelieren.
Es gibt viele prominente Beispiele von Fehlern in Raketen-Software.
Hand hoch, wer Software fuer Medizinprodukte herstellt!
Ich hab auch ein paar Beispiele aus der Medizin wo Softwarefehler zu richtig bösen Fehlern geführt haben.
ich warte weiter auf ein Beispiel. Ein einziges Beispiel.
Kann ja nicht so schwer sein, oder?
-
Und ich dachte, Dein Standpunkt wäre, dass fehlerfreie Software nicht unmöglich wäre! Jetzt widersprichst Du diesem Standpunkt?
-
hustbaer schrieb:
@nwp3
Dein getKmInM zeigt finde ich ganz gut das eigentliche Problem.
Das kann man in C++ nämlich sehr einfach "sicher" hinbekommen. Indem man Längen nicht als Integers behandelt, sondern einen eigenen Typ dafür macht.Wenn man einen eigenen Typ macht, dann ist dort auch die getKmInM-Funktion drin, genauso falsch wie vorher. Es ist natürlich sinnvoll dafür einen Typen zu machen, weil man nur noch an einer Stelle diesen Fehler machen kann, aber man kann ihn trotzdem machen.
Dagegen hilft möglichst viele Leute mit Ahnung drüber kucken lassen und hoffen, dass es wem auffällt.
Unit-Tests könnten den Fehler auch finden. Oder 2 Implementierungen, wo dann ein System versucht einen Widerspruch zu finden und man dann nachprüfen kann wer recht hatte. Und hoffen, dass niemals in beiden Implementierungen der gleiche Fehler vorkommt.
Alles zu viel hoffen.
decimad schrieb:
Mann Jungs, das einzig interessante hier im Thread war doch, ob knivil auch nur mit Wasser kocht
Ist mir egal womit knivil kocht. Interessant ist, ob man die Korrektheit von Software beweisen kann.
Folgender Ansatz funktioniert ganz gut: Unterteilung in Fehlerklassen. Fehlerklassen Lexik/Syntax kriegt der Compiler hin, Semantik mit Einschränkungen. Bufferoverflows, Memory Leaks, Race Conditions und Integer Overflows kann man per Unit Test testen, indem man alle gültigen Eingaben durchprobiert und es nachprüft, dauert nur etwas.
Sanity Checks können grobe Fehler wie eine falsche Umrechnung finden, aber versagen bei falschen plausibel aussehenden Resultaten.
Rundungsfehler kriegt man sicher auch weg, indem man immer in eine Richtung rundet und dann einen Bereich angibt, in dem das Ergebnis liegt.Am Ende gibt man dann eine Liste von Fehlerklassen an und kann jeweils sagen, ob es einen Fehler in dieser Fehlerklasse geben kann. Man kriegt nicht alle Fehlerklassen weg und man kann auch nicht garantieren alle Fehlerklassen betrachtet zu haben, aber es ist ein Anfang.
Es gibt noch einen Punkt der eigentlich aus der Security Ecke kommt. Man hat formal bewiesen, dass der neue elektronische Personalausweis unknackbar ist. 3 Wochen später wurde er geknackt. Was ist passiert? Im Beweis stand eine Annahme, die man kaputt gemacht hat. Irgendwo wurde irgendwas am Ausweis verändert, was im Beweis nicht vorgesehen, aber praktisch möglich war. So ein Beweis macht es übrigens allgemein recht einfach Lücken zu finden, weil man die Voraussetzungen durchgeht und eine davon kaputt machen kann.
-
@mwp3: Um seine Aussagen einzuschätzen, war es extrem wichtig, dieses Detail zu erfahren. Deshalb kann ich nicht nachvollziehen, weshalb es Dich nicht interessiert hat. Offenbar werden hier ja dieselben Worte für unterschiedliche Sachverhalte verwendet.
-
knivil schrieb:
Hand hoch, wer Software fuer Medizinprodukte herstellt!
Was hast du mit deinen Medizinprodukten? Sind die iwie besonders? Bei uns (meiner Stadt) in der Zahnklinik läuft SAP. Was auf den Microcontrollern der Beatmungssysteme läuft, keine Ahnung.
Zum nachdenken... Wenn ein Beatmungssystem ausfällt, stirbt wie bei den meisten Produkten zur medizinischen Versorgung meist nicht mehr als einer. Bei automatisch gesteuerten Waffensystemen leicht ein ganzer Wohnblock und in der zivilen Luftfahrt und auf der Schiene, führen Softwarefehler schnell zu großen Unglücken!
Also bilde dir bitte nichts auf deine Medizinsoftware ein
-
junta schrieb:
Also bilde dir bitte nichts auf deine Medizinsoftware ein
Genau, gib es dem Clown. Auch belächelte Webprodukte können ab einer bestimmten Größe einen nicht unerheblichen wirtschaftlichen Schaden anrichten. Man stelle sich nur mal vor, es gibt stundenlang kein Google, oder Facebook. Oder gleich gar kein Internet, weil ein Router fehlerhaft ist
Das zieht mit Sicherheit Suizidfälle nach sich!
-
ich warte weiter auf ein Beispiel. Ein einziges Beispiel.
Kann ja nicht so schwer sein, oderDoch, du kannst nur omnioeserweise die Website nicht oeffnen. Weiterhin sitze ich gerade vor einem und benutze es. Weiterhin ... Meinst du, dass beispielsweise fehlerfreie Software einer Hydraulikpumpe grosse Wellen in den Nachrichten schlaegt?
Es gibt viele prominente Beispiele von Fehlern in Raketen-Software.
Und wieviele prominente Beispiele fehlerfreier Raketensoftware gibt es? Liegt das eher daran, dass sie nicht in den Nachrichten diskutiert wird, weil eben keine Katastrophe ausgeloest wurde.
führen Softwarefehler schnell zu großen Unglücken!
Softwarefehler fuehren in der Regel dazu, dass das Produkt nicht zugelassen wird bzw. die Zulassung entzogen wird ohne das irgendwer zu schaden kommt.
-
junta schrieb:
Wenn ein Beatmungssystem ausfällt
Schlechtes Beispiel, sowas geht auch gut von Hand. Bei einer HLM wär es schon schwerer, da ist man zügig hirntot, wenn man gerade am Herz rumfummelt.
-
knivil schrieb:
Doch, du kannst nur omnioeserweise die Website nicht oeffnen. Weiterhin sitze ich gerade vor einem und benutze es. Weiterhin ... Meinst du, dass beispielsweise fehlerfreie Software einer Hydraulikpumpe grosse Wellen in den Nachrichten schlaegt?
dh also du kannst kein Beispiel nennen.
Und nochmals: nur weil die Software nicht explodiert, ist sie noch lange nicht fehlerfrei. Die meiste Software ist sehr stabil und weist sehr wenige Fehler auf. Und wenn es spezial software für einen sehr engen Markt ist und es nur wenige Installationen gibt - dann werden viele Fehler in der Software garnicht erst entdeckt.
-
dh also du kannst kein Beispiel nennen.
Ich habe genannt, du akzeptierst es nur nicht.
dann werden viele Fehler in der Software garnicht erst entdeckt
Weil sie vielleicht auch nicht drin sind? Warum sollten in einem uebrschaubarem Programm fuer einen Mikrokontroller unbedingt Fehler sein. Ich sehe keine Unmoeglichkeit darin, in bspw. 5000 Zeilen (oder 10000 oder ... ) Code keinen Fehler zu machen. Dann gibt es die zahlreichen Progrmmier-Contest-Portale. Alle akzeptierten Loesungen sind gemaess der der gegeben Spezifikation fehlerfrei. Unter gegebenen Constraints wird eine bestimmte Eingabe in die geforderte Ausgabe transformiert.
Und nochmals: nur weil die Software nicht explodiert, ist sie noch lange nicht fehlerfrei.
Und nochmals: weil es viele Beispiele explodierender Systeme durch Softwarefehler gibt, heisst das noch lange nicht, dass alle Software fehlerhaft ist.
-
Auch Medizinsoftware ist nicht fehlerfrei, genauso wenig wie Software für das Militär, Flugzeuge und die NASA.
-
Dass eine Software nicht fehlerfrei ist, muss man auch erstmal beweisen. Dabei stößt man wahrscheinlich im Allgemeinen auf dieselben Probleme, die man hat zu beweisen, dass eine Software fehlerfrei ist.
Keine Aussage der Unbeweisbarkeit von irgendwie definierter Fehlerfreiheit impliziert, dass es kein unter der Definition fehlerfreies Programm gibt.
Ich verwette meinen Arsch drauf - dass es unter realistischer Definition von Fehlerfreiheit - eine Menge Programme auf dieser Welt gibt, die fehlerfrei sind. Da sind dann so Fälle ausgeschlossen wie die spontane Physikveränderung, oder dass die Software auch nach Ende des Universums oder bei Zerstörung der Hardware noch laufen soll. Schon der Fall der Synchronisierung auf einen unterschiedlichen Takt ist heikel...
Aber andererseits gehe ich auch nicht davon aus, dass mein Programm fehlerfrei ist, nur weil ich ein bisschen nachgedacht habe (es ist immerhin zu 99.999% der Fälle so, dass mein nächster Gedanke Unsinn ist) und die Komponenten die full coverage unit tests bestehen, die ich ersonnen habe. Daher versuche ich zumindest auch üblicherweise nur ein möglichst großes Vertrauen zu gewinnen...
-
knivil schrieb:
dh also du kannst kein Beispiel nennen.
Ich habe genannt, du akzeptierst es nur nicht.
Nein. Du hast eine Webseite verlinkt auf der die Firma die diese betreibt groß einen Disclaimer schreibt dass alle Informationen auf dieser Seite "AS IS" sind und sie keine "LIABILITY" übernehmen.
Das ist kein Beweis einer Fehlerfreien Software. Sorry.
Und nochmals: weil es viele Beispiele explodierender Systeme durch Softwarefehler gibt, heisst das noch lange nicht, dass alle Software fehlerhaft ist.
Es heisst aber auch nicht dass eine nicht explodierende Software Fehlerfrei ist. Du kannst alle Spezifikationen erfüllen und trotzdem Fehler haben.
Wenn ich eines gelernt habe über Programmierung, dann das überall Fehler drin sein können. Ich habe schon Maschinensteuerungen gesehen die 20 Jahre Fehlerfrei gelaufen sind aber dennoch Fehler enthalten haben (die erst aufgefallen sind als andere Hardware verwendet wurde).
-
Eine Firma die ihren Kunden fehlerfreie Software garantiert ist unseriös.
