Bugs in der STL
-
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.
-
Edit: Ach was solls ...
-
@knivil
Ja, ist besser wenn du es lässt. Du machst dich nämlich gerade massiv lächerlich.
-
Bashar schrieb:
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.
Und der Beweis dass das Programm der Definition entspricht ist dabei ebenso einfach? Glaub ich nicht.
-
decimad schrieb:
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.
Nein, es reicht, einen einzigen Fehler zu finden. Nicht dass das einfach ist -- aber üblicherweise massiv einfacher als Fehlerfreiheit zu beweisen (bzw. überhaupt erst möglich).
-
hustbaer schrieb:
Und der Beweis dass das Programm der Definition entspricht ist dabei ebenso einfach?
Nein, natürlich nicht.
-
Können wir das Thema beenden?
Entweder ist für knivil gerade ein Weltbild zusammen gebrochen, oder er ist Beratungsresistent geworden. Bei letzterem wird er weiter an seiner Methodik glauben und wir werden ihn bald in der Presse sehen, weil er einen Informatiker-Preis nach dem anderen abräumt. Um Geld muss er sich dann keine Sorgen mehr zu machen.
-
@Nexus: Wenn ein Fehler vorhanden ist, dann erscheint das natürlich noch am einfachsten von allen Problematiken. Aber sagen wir mal, wir haben ein fehlerfreies Programm - wie findest Du den Fehler? Wie beurteilst Du, ob es Sinn macht, sich auf die Suche zu machen und wann brichst Du ab? Dafür gibt es natürlich kein allgemeines Kriterium, denn dann hättest Du ja Fehlerfreiheit bewiesen. Hast Du bei Abbruch einen theoretischen Erkenntnisgewinn? Wenn man davon ausgeht, dass jedes Programm nur endlich viele Fehler hat, dann kommt man ja zwangsläufig an diesen Punkt.
Natürlich ist das Programm durch beheben der Fehler besser geworden, also war es eine nutzbringende Beschäftigung. Aber am Ende hat man doch nur Fehler gefunden oder die Suche aufgegeben, ohne Gewinn einer Aussage im Allgemeinen.
-
jemand hat den account von knivil gehackt. so behindert war der sonst nie
-
Bashar schrieb:
hustbaer schrieb:
Und der Beweis dass das Programm der Definition entspricht ist dabei ebenso einfach?
Nein, natürlich nicht.
Genau das meine ich ja.
Wenn der Beweis nicht einfach ist, dann kann er genau so fehlerhaft sein, wie ein Programm fehlerhaft sein kann.
Man tauscht damit bloss ein "na hoffentlich hat da keiner einen Fehler gemacht" gegen ein anderes "na hoffentlich hat da keiner einen Fehler gemacht" aus.Wenn man es also super-genau nimmt, dann kann man bei keinem nicht-trivialen Programm den endgültigen Beweis erbringen dass es fehlerfrei ist.
-
hustbaer schrieb:
Bashar schrieb:
hustbaer schrieb:
Und der Beweis dass das Programm der Definition entspricht ist dabei ebenso einfach?
Nein, natürlich nicht.
Genau das meine ich ja.
Wenn der Beweis nicht einfach ist, dann kann er genau so fehlerhaft sein, wie ein Programm fehlerhaft sein kann.Dann hab ich dich falsch verstanden. Ich hatte den Eindruck, du meintest, die Spezifikation sei genauso schwer wie das Programm. Und wenn ich das nochmal lese ...
D.h. du musst die Regeln in einer formalen Sprache ausdrücken.
In einer formalen Sprache, wie z.B. ... Lisp.
Und fällt dir was auf? Richtig, jetzt hast du ein Lisp Programm. Und dein toller, semi-universeller Beweis hat bewiesen dass dein XYZ Programm dem Lisp Programm entspricht... ist diese Interpretation auch gerechtfertigt.
Man tauscht damit bloss ein "na hoffentlich hat da keiner einen Fehler gemacht" gegen ein anderes "na hoffentlich hat da keiner einen Fehler gemacht" aus.
Es gibt auch sowas wie formale Beweise, die sich Schritt für Schritt (automatisch) verifizieren lassen.
-
@Bashar
In vielen Fällen ist eine formale, vollständige Spezifikation auch gleich viel Aufwand wie das Programm selbst - oder liegt zumindest in der selben Grössenordnung.
Denk nurmal an Software für diverse Unternehmens-Prozesse. Da kommt es oft vor dass der Chef mit einer formlosen Spezifikation daherkommt, und es dann erstmal Tage oder Wochen dauert bis diese in etwas verwandelt wurde das alle möglichen Fälle abdeckt/beschreibt. Und dann setzt man sich hin und tippt das Programm in 30 Minuten runter.Fälle wo so eine formale Spezifikation um Grössenordnungen leichter ist als die Implementierung bzw. das Design eines entsprechenden Algorithmus gibt es sicher auch. Mit denen hab' ich aber eher selten zu tun
----
Und ich meine, dass die wenigsten Spezifikationen mit denen real Programme in Auftrag gegeben werden, mit Programmen umsetzbar sind, die beweisbar sind, mit einem Beweis der wiederrum trivial (also z.B. vollautomatisch) verifizierbar ist.
-
Kann alles sein, weiß ich nicht, jedenfalls entspricht es der Mainstream-Meinung, soweit ich das erkennen kann. Da hab ich nichts mehr hinzuzufügen.
