Abo
  1. Foren
  2. Kommentare
  3. OpenSource
  4. Alle Kommentare zum Artikel
  5. › Qualität von Open-Source-Software…

Schön Beweisbarkeit wird kommen

  1. Thema

Neues Thema Ansicht wechseln


  1. Schön Beweisbarkeit wird kommen

    Autor: Siga9876 24.09.09 - 11:00

    Sowas ist nett. Gute Software ist eine Ächtung aller miesen Lame-Progger.
    Interessant wenn man sieht, das samba,tor,ruby auf der Super-Liste überguter Software stehen.

    Beweisbarkeit wird kommen.
    Die Methoden sind i.d.R. eine Bildschirmseite. Die Rechenleistung ist seit früher massiv vermehrt (verdoppelt alle 15-18 Monate) so das Beweise möglich sind.

    Weiteres in meinen anderen Postings zu beweisbarkeit.
    Nur weil Leute theorien gödel falsch verstehen, diskutier ich hier nicht mit denen.

    Es geht nicht darum, jedes Programm zu checken.
    Das Eich-Amt misst/eicht ja auch nur gewerbliche Waagen.
    Ein Projekt möchte gern bewiesen sein, dann kann es den code auch beweiser-freundlicher schreiben.
    Es geht nicht darum, jeden zufällig zusammengewürfelten C-Code der compilierbar ist, zu beweisen.

    Und Korrektheit ist nur ein Peanut. Zahl der Plattenzugriffe, bandbreite auf begrenzter Bus-Bandbreite usw. sind genau so wichtige Metriken die man ggf. beweisen möchte.

  2. Re: Schön Beweisbarkeit wird kommen

    Autor: we 24.09.09 - 11:10

    Und wo ordnen wir dabei Firefox ein? Ist ja auch Open Source. Gleichzeitig aber vollkommen unbrauchbar und vermutlich was den Code angeht total vergurkt.

  3. Re: Schön Beweisbarkeit wird kommen

    Autor: Siga9876 24.09.09 - 11:18

    Deswegen nehme ich normalerweise Opera.

    google-Reader geht in Firefox viel besser und Amazon hat EINEN Link beim Marketplace reinstellen wo man leider auch firefox nehmen muss.

    Ich habe auch nirgendwo behauptet, das Open Source besser wäre.
    Hier gehts um Beweisbarkeit und nicht um Open Source.

    Allerdings könnten natürlich geschulte sweeper-teams beweiser-hints bzw. conditions/vor-nachbedingungen an kernel-module dranhängen. oder halt "anti-beweise" wo klar wird, das spacko-treiber-progger mal wieder scheisse gebaut hat.
    beides macht sinn (fehler finden, beweise bauen).

  4. Re: Schön Beweisbarkeit wird kommen

    Autor: RaiseLee 24.09.09 - 11:29

    Seit wann ist der unbrauchbar?

  5. Re: Schön Beweisbarkeit wird kommen

    Autor: Tingelchen 24.09.09 - 13:27

    Ein Tool kann niemals die Richtigkeit oder Korrektheit eines anderen Tools beweisen. Denn dazu müste es erst einmal sich selber die Richtigkeit oder Korrektheit beweisen. Das geht aber nicht ;)


    Daher sind solche Tools zwar Praktisch aber niemals ein Ersatz für ausführliche Beta Tests.

  6. Re: Schön Beweisbarkeit wird kommen

    Autor: Siga9876 24.09.09 - 14:10

    Häh ?

    Ein Beweis ist eine endliche Ableitungskette.
    Das Tool kann so kommunistisch, cdu-freundlich, gehirnamputiert, likes, rechts, oben unten, falsch-rum sein wie es will.
    Wenn es eine endliche !KORREKTE! Ableitungs-Kette erzeugt, die den Beweis erbringt, ist egal, wie herum das Tool ist.

    Das ist der "Trick" dabei. Einen !maschinellen! Beweis (bzw. Ableitungs-Kette) kann man IMMER Überprüfen. So wie man beispielsweise die linke und rechte Seite einer Bilanz zusammenzählen kann und gucken kann, ob beide Seiten exakt denselben Wert liefern (was sie müssen).

    Es gibt Beweise, die man lange für welche hielt, aber doch keine waren. Aber das waren halt keine maschinell überprüfbaren Ableitungsketten.

    Das ist dann eher so wie wenn man im Multiple Choice was ankreuzt was richtig oder falsch ist, aber seine Rechnung nicht auf dem Prüfungsblatt (oder Bei-Blatt) ablegen muss. Was man für Kopfrechnung nicht muss, aber bei richtigeren Prüfungen höherer "DAN"-Level/Schulstufen/UNI schon.

    Bei maschinellen Beweisen ist die Überprüfung geilerweise aber möglich.
    So wie gute Zitate/Plagiatismus auch einfach erkennbar ist. Bei den guten Zitaten ist eine [Hanswurst 1998]-Quellen-Angabe. Böse Zitate sind dasselber aber ohne Quellenangabe. Das ist so ähnlich wie "selbstjustierend", weil man Plagiatismus-Checker-Tools auch mit guten/korrekten Texten checkern kann.

    Du hast aber indirekt Recht, das ein fehlerhaftes Tool i.d.R. fehlerhafte also ungültige Beweise abliefern wird.
    So wie Bundeswehrsoldaten die zickzacklinien bei Umfragen/IQ-Tests ankreuzen, zu denen sie "zwangsrekrutiert" oder mit einer Flasche Bier/Packung Schokolade/Zigaretten geködert wurden.

  7. Re: Schön Beweisbarkeit wird kommen

    Autor: Arti 24.09.09 - 17:37

    Siga9876 schrieb:
    --------------------------------------------------------------------------------

    > Beweisbarkeit wird kommen.

    Nein. Nur die Beweisbarkeit, dass die Implementierung des Spezifikation entspricht, aber wie willst Du beweisen, dass die Spezifikation korrekt ist? Du kannst das Beweisproblem immer weiter nach Vorne verlagern, aber wenn Du beim Menschen angekommen bist, geht es nicht weiter. Somit sind autom. Beweissysteme IMHO relativ sinnlos.

    Arti

  8. Re: Schön Beweisbarkeit wird kommen

    Autor: Siga9876 24.09.09 - 19:04

    Spezifikation schreiben ist also sinnlos. Na super Einstellung.

    Man beweist nicht nur die Spezifikation.
    Man beweist viel geilere Sachen: Das diese Implementierung mit einer bestimmten Bandbreite auskommt. ODer bestimmte Latenz-Anforderungen erfüllt. oder pro Client maximal x Blöcke von der Platte braucht weshalb man garantieren kann, das der durchsatz für x,000 Flugzeuge und FlugZeug-Routen-Lotsen-Software reicht.

    Amis haben fette vermutlich überlastete Infrastrukturen die noch nicht ansatzweise zusammengebrochen sind. Dafür brauchts nichtmal terroristen. der fette stromausfall vor ein paar Jahren der ganze bundesländer/us-staaten oder dieses Jahr Hamburg stromfrei legte, beweisen es.

    Na gut. Egal. Beweisen muss so laufen wie bart simpson der mit irgendjemand anderem im wettbewerb steht und "ich kann auch bungejumpen" "Ich kann über den fluss springen" "Ich kann über die stromleitung spazieren" "ich kann mit dem skateboard über die chemikalen-tanks skatern"... ständig eskaliert.
    Wenn man mal Modelle für attacken hat (was nicht notwendig bedeutet das andere attacken nicht gehen), kann man alle software unterziehen. und im öffentlichen/sicherheitskritischen(flugzeuge, krankenhaus,...) bereich sollte man es einfach machen.

    Du hast aber vollkommen Recht, das die Spezifikation ein Risikofaktor ist.
    Aber zu beweisen, das keine buffer-overflows, keine lecks,... (bekannter Sorte) vorhanden sind, ist auch schon mal etwas.

  9. Re: Schön Beweisbarkeit wird kommen

    Autor: Alois Hintername 24.09.09 - 20:32

    > Du kannst das Beweisproblem immer weiter nach Vorne verlagern
    Ja, bis zur Ursuppe. Deshalb gibt es leckere Sachen wie Axiome, Methodik und anderes wissenschafftliches Vodoo. Man munkelt gar, selbst angewandte Mathematik funktioniere ohne pseudointellektuelles Zerreden.

  10. Re: Schön Beweisbarkeit wird kommen

    Autor: Siga9876 24.09.09 - 23:49

    Spacken haben Angst vor Neuem, weil es ihre evolutionsmößig hinterwäldlerische Existenz bedroht.

    Das ist kein Zerrede. Da gehts darum, absichtlich minderwertig zu proggern.

    Immer weiter verlagern geht auch nicht. Da hat er vermutlich Unrecht. ABer er hat Recht, das man sehr genau wissen muss, was man beweisen will.
    Boyer-Moore-Buch über ihren Beweiser (für eine !eingeschränkte! Logik) gabs das Beispiel von Sortieralgorithmen: Da hat der Beweiser bewiesen, das der Sortieralgorithmus korrekt ist. Doof nur das der Algorithmus nur die leere Liste lieferte. Da hat man in der Spezifikation vergessen, reinzuschraiben, das die Elemente nicht nur sortiert sein müssen (das hatte man nicht vergessen), sondern auch alle Elemente die vorher drin ware, auch nach dem Sortieren drin sein müssen.
    Die einfachste sortierte Liste ist halt die leere Liste.
    Von daher ist das Argument mit der schlechten Spezifikation schon korrekt.

    Bei Optimierung sieht man schnell, das man z.b. x1>=0 vergessen hat, wenn plötzlich negative Werte rumkommen z.b. für Umsatz-Optimale Müsli-Mischungen. Aber in Realität dürften viele Optimierungssysteme mit leicht falschen Parametern gefüttert sein so das nicht wirklich die optimale Lösung ausgespuckt wird. Fällt halt bei 20 oder mehr Variablen nicht weiter auf.

    Man müsste immer doppelt und dreifach drübergucken.
    Und bei Standard-Libs sollte es NULL/KEINE Buffer-Overflows, NULLpointer-Fehler usw. mehr geben. Sowas sollte Steinzeit sein.

    Und das etwas die Specs erfüllt, heisst nicht, das es bei fehlerhaften Daten keine Buffer-Overflows hat. Aber genau geht es ja auch: AUCH den Schutz vor Buffer-overflows bei bösen Daten.

  11. Re: Schön Beweisbarkeit wird kommen

    Autor: Hello_World 25.09.09 - 00:11

    > Denn dazu müste es erst einmal sich selber die Richtigkeit oder Korrektheit beweisen.
    Blödsinn, das kann ein Mensch machen.

  12. Re: Schön Beweisbarkeit wird kommen

    Autor: Der Kaiser! 25.09.09 - 02:56

    > Ein Tool kann niemals die Richtigkeit oder Korrektheit eines anderen Tools beweisen. Denn dazu müste es erst einmal sich selber die Richtigkeit oder Korrektheit beweisen. Das geht aber nicht ;)
    Kommt auf die Komplexität des Tools an. ^^

    ___

    Die ganz grossen Wahrheiten sind EINFACH!

    Wirkung und Gegenwirkung.
    Variation und Selektion.
    Wie im grossen, so im kleinen.

  13. FULLACK! (kwT.)

    Autor: Der Kaiser! 25.09.09 - 03:01

    > bei Standard-Libs sollte es NULL/KEINE Buffer-Overflows, NULLpointer-Fehler usw. mehr geben. Sowas sollte Steinzeit sein.
    Mich wundert das der Compiler nicht die Programme auf sowas checkt!

    ___

    Die ganz grossen Wahrheiten sind EINFACH!

    Wirkung und Gegenwirkung.
    Variation und Selektion.
    Wie im grossen, so im kleinen.

  14. Re: FULLACK! (kwT.)

    Autor: Siga9876 25.09.09 - 09:51

    Der Kaiser! schrieb:
    --------------------------------------------------------------------------------
    > > bei Standard-Libs sollte es NULL/KEINE Buffer-Overflows,
    > NULLpointer-Fehler usw. mehr geben. Sowas sollte Steinzeit sein.
    > Mich wundert das der Compiler nicht die Programme auf sowas checkt!

    In moderneren Sprachen gibts im Speicher herumpoken ja nicht mehr. Danke.

    Wenn man gcc -Wall (iirc) einschaltet, kriegt man auch bessere Fehlermeldungen.

    Früher gabs separat z.b. "lint" dafür. Weil die Kisten lahm waren und man zillionen Zeilen übersetzen musste ("make world" bei ***BSD als Beispiel) hat man Code-Checking und einfach nur schnell mal compilieren getrennt gehalten. Dann hat man code-checking einfach sein lassen... Spacken-progger-Pack.

    Momentan ist es leider immer noch eine Einstellung anständig programmieren zu wollen. Spacken-Progger-Packs sollte aber nix anderes übrig bleiben.

    Davon abgesehen sollte man mehr configuren (rollen/Datenbasiert) und automatisiert 90% des codes erzeugen und nur echte Aufgaben wirklich seölber proggern. aber in vielen business-bereichen ist es eh nur daten verschieben und z.b. in der warenwirtschaft die bestellten produkte im bestand herunterzählen. oder kfz-nummern mit versicherungsnummern und adresse des auto-eigentümers verbinden. Das macht die primitive datenbank.
    das konfiguriert man einmal und ein billiger ScreenDesigner macht die CSS für die Daten für die Bürger-interfaces und beamten-interfaces. aber so weit ist proggertum leider noch nicht.
    im praktikum habe ich sowas wie javadoc "erfunden" und mir aus kommentaren die doku in latex automatisiert zusammengestellt.
    sowas wie hibernate (natürlich primitiver) hätte ich mir auch erfunden, wenns das nicht schon gäbe.
    jetzt fehlt noch rollen+daten und primitiv-software wird/bleibt primitiv. und alle haben einen nutzen.

  15. Re: FULLACK! (kwT.)

    Autor: Der Kaiser! 26.09.09 - 01:20

    >>> bei Standard-Libs sollte es NULL/KEINE Buffer-Overflows, NULLpointer-Fehler usw. mehr geben. Sowas sollte Steinzeit sein.

    >> Mich wundert das der Compiler nicht die Programme auf sowas checkt!

    > In moderneren Sprachen gibts im Speicher herumpoken ja nicht mehr. Danke.
    Man sollte aber bei Bedarf das trotzdem machen können.

    ___

    Die ganz grossen Wahrheiten sind EINFACH!

    Wirkung und Gegenwirkung.
    Variation und Selektion.
    Wie im grossen, so im kleinen.

  1. Thema

Neues Thema Ansicht wechseln


Um zu kommentieren, loggen Sie sich bitte ein oder registrieren Sie sich. Zum Login

Stellenmarkt
  1. EHRMANN AG, Oberschönegg
  2. NÜRNBERGER Versicherung, Nürnberg
  3. Pfennigparade SIGMETA GmbH, München
  4. Hessisches Ministerium der Finanzen, Frankfurt am Main

Golem pur
  • Golem.de ohne Werbung nutzen

Anzeige
Hardware-Angebote
  1. täglich neue Deals bei Alternate.de
  2. 49,70€
  3. (reduzierte Überstände, Restposten & Co.)


Haben wir etwas übersehen?

E-Mail an news@golem.de


Recruiting: Wenn das eigene Wachstum zur Herausforderung wird
Recruiting
Wenn das eigene Wachstum zur Herausforderung wird

Gerade im IT-Bereich können Unternehmen sehr schnell wachsen. Dabei können der Fachkräftemangel und das schnelle Onboarding von neuen Mitarbeitern zum Problem werden. Wir haben uns bei kleinen Startups und Großkonzernen umgehört, wie sie in so einer Situation mit den Herausforderungen umgehen.
Von Robert Meyer

  1. Recruiting Alle Einstellungsprozesse sind fehlerhaft
  2. LoL Was ein E-Sport-Trainer können muss
  3. IT-Arbeit Was fürs Auge

Garmin Fenix 6 im Test: Laufzeitmonster mit Sonne im Herzen
Garmin Fenix 6 im Test
Laufzeitmonster mit Sonne im Herzen

Bis zu 24 Tage Akkulaufzeit, im Spezialmodus sogar bis zu 120 Tage: Garmin setzt bei seiner Sport- und Smartwatchserie Fenix 6 konsequent auf Akku-Ausdauer. Beim Ausprobieren haben uns neben einem System zur Stromgewinnung auch neue Energiesparoptionen interessiert.
Ein Test von Peter Steinlechner

  1. Fenix 6 Garmins Premium-Wearable hat ein Pairing-Problem
  2. Wearable Garmin Fenix 6 bekommt Solarstrom

Manipulierte Zustimmung: Datenschützer halten die meisten Cookie-Banner für illegal
Manipulierte Zustimmung
Datenschützer halten die meisten Cookie-Banner für illegal

Nur die wenigsten Cookie-Banner entsprechen den Vorschriften der DSGVO, wie eine Studie feststellt. Die Datenschutzbehörden halten sich mit Sanktionen aber noch zurück.
Ein Bericht von Christiane Schulzki-Haddouti

  1. Chrome & Privacy Google möchte uns in Zukunft anders tracken
  2. Tracking Google und Facebook tracken auch auf vielen Pornoseiten
  3. Android Apps kommen auch ohne Berechtigung an Trackingdaten

  1. Elektromobilität: Stromwirtschaft will keine Million öffentlicher Ladesäulen
    Elektromobilität
    Stromwirtschaft will keine Million öffentlicher Ladesäulen

    Verkehrsminister Scheuer will günstige Elektroautos stärker fördern, Vizekanzler Olaf Scholz fordert "so was wie ein Eine-Million-Ladesäulen-Programm". Doch die Stromversorger warnen vor einer "überdimensionierten Ladeinfrastruktur".

  2. Saudi-Arabien: Drohnenangriffe legen halbe Erdölproduktion lahm
    Saudi-Arabien
    Drohnenangriffe legen halbe Erdölproduktion lahm

    Drohnen aus dem Jemen sollen die wichtigste Erdölraffinerie Saudi-Arabiens in Brand gesetzt haben. Die USA beschuldigen den Iran, die Huthi-Rebellen mit der Waffentechnik ausgerüstet zu haben.

  3. Biografie erscheint: Union lehnt Asyl für Snowden weiter ab
    Biografie erscheint
    Union lehnt Asyl für Snowden weiter ab

    US-Whistleblower Edward Snowden hätte weiterhin nichts dagegen, Russland in Richtung Deutschland zu verlassen. Doch Schutz vor einer Auslieferung in die USA kann er hierzulande nicht erwarten.


  1. 14:21

  2. 12:41

  3. 11:39

  4. 15:47

  5. 15:11

  6. 14:49

  7. 13:52

  8. 13:25