Bugs in der STL
-
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.
-
Obwohl man ja sagen muss, dass alle großen Leute deswegen groß geworden sind, weil sie eben nicht den Mainstream gegangen sind und wirklich so gut wie jeder gegen ihre Meinung war. Ich glaube daran wird sich auch in Zukunft nix ändern. Große Programme/Frameworks/Libs oder neue Algos etc. werden deswegen entstehen, weil jemand halt doch das Rad neu erfinden möchte und gegen die Meinung der meisten Entwickler handelt. Zu deutsch, einen großartigen Informatiker werden wir vielleicht daran erkennen, dass er hier ungemein aneckt und sich gegen die allgemeine Meinung aufbringt und bis zum Schluss sein Ding durch zieht.
Mit Mainstream wird die Menschheit nicht vorangebracht. Mainstream bedeutet Stillstand des Fortschritts, was ja nicht immer schlecht sein muss, denn es sichert das tägliche Leben.
-
Ja, ich seh's kommen, wie jemand von hier die Fields-Medaille entegennimmt und sich öffentlich bei Krümelkacker, Xin, Hustbaer, Volkard, Bashar, Nexus, Skymosho und den ganzen C++.de-Homies bedankt
-
Ich kann nicht erkennen, wo der Zusammenhang zu dem Gesagten besteht. Da hat wohl jemand reflexhaft auf das Wort Mainstream reagiert.
