1. Foren
  2. Kommentare
  3. Software-Entwicklung
  4. Alle Kommentare zum Artikel
  5. › Saarländer erforschen…

Correctnes by construction

  1. Thema

Neues Thema Ansicht wechseln


  1. Correctnes by construction

    Autor: Saarländer 17.02.10 - 19:23

    Beweisen ist ein paar Zehnerpotenzen schneller als früher.
    Moores Law sei Dank.

    "Der falsche Glaube an die exponentielle Fehlerzunahme hat die VLSI-Technologie 10 Jahre verzögert". Wir könnten die Chips von in 10 Jahren schon heute haben !

    Beweisen ist möglich.
    Der Trick ist nicht, jeden cripple-crap-PHP-Code beweisen zu wollen.
    Der Trick ist: Du kriegst den Auftrag nur, wenn Du bewiesenen Code ablieferst inclusive Beweisen und Logs und Traces usw.
    D.h. Du programmierst gleich Beweiserfreundlich. Damit wird Gödel zur Legende. Denn ich brauche und will gar nicht jeden Code beweisen. Sondern ich bestelle bewiesenen Code bei der Ausschreibung. har har har.

    Sowas was Statiker jeden Tag bei Gebäuden und Brücken machen und durchrechnen. Halt bei Software.

    Auch beweist man verschiedene Dinge. Und zwar je nachdem, was man braucht. Maximaler Speicherplatz bei Bloat-Fox, maximale Stacktiefe, Anzahl der TCP-Connects.
    Anzahl der SMS, die man braucht, um eine Feuerwehr-wagen-Meldung an die Feuerwehr-Zentrale zu senden.
    Anzahl und Dauer des Kommunikation zum Mars usw.
    Unanfälligkeit gegen Buffer-Overflows usw.

  2. Re: Correctnes by construction

    Autor: IT-Kunstentdecker 17.02.10 - 19:25

    Du schreibst wie er!

  3. Re: Correctnes by construction

    Autor: Oaktrail 17.02.10 - 20:59

    Das 4augen-Prinzip oft nicht Leistung liefert, hast Du ein paar Golem-Meldungen höher bei "lex-linux's lame" lesen dürfen.

    Und das man besser anständig planen soll, kann man im Forum auch lesen.

  4. Re: Correctnes by construction

    Autor: Der Blub 17.02.10 - 23:43

    Jaja Gödel wird nicht zur Legende, Gödel ist legendär...
    Man siga, hol dir ein gutes Buch über theoretische Informatik und dann wirst du vielleicht im Ansatz merken, was für ein Stuss du laberst

  5. Re: Correctnes by construction

    Autor: IT-Kunstentdecker 18.02.10 - 00:17

    Was? Ô_ó

  6. Re: Correctnes by construction

    Autor: Saarländer 18.02.10 - 00:35

    Bei Dächern und Wintergärten "beweist" Du statisch (nicht statiSTIsch), das sie Schnee-Lasten von z.b. 120 kg/m^2 vertragen.

    Und man "beweist" z.B. das Wind-lasten bei XX km/h bei z.b. UMTS-Antenne ohne das die Antenne in die Innenstadt fliegt und Leute zermatscht oder abgerissene Teile Fußgängern Körperteile rausfetzen oder halt Autos beschädigen.

    Eine Sat-Schüssel darf man dann bald wegen Versicherung nicht mehr anbringen. Weil die Orkantornados durch Klima-Erwärmung sie sowieso bald abreissen werden.

    Ich glaube, Du solltest erst mal Gödel verstehen.

    Man kann automatisch nicht ALLE Programme beweisen.
    Das heisst aber nicht, das man keine bewiesene Software abliefern kann. Wenn Du eine Vorlesung besucht hast, wüsstest Du genug Beispiele wo krass stundenlang bewiesen wurde. Oft nur Laufzeit. Manchmal Korrektheit. Halt nicht automatisch. Aber ALGORITHMEN (nicht Programme) muss man sowieso (mit der Hand selber) beweisen.
    Du schreibst dann also Software, wo der Software-Beweiser mit klar kommt.
    Probleme gibts dann damit, was überhaupt bewiesen werden soll. Das ist aber erst mal ein anderes Problem. Nämlich ein Spezifikations-Fehler.

    Das ist wie Einstein. Da haben manche Leute nämlich die falsche Vorstellung, das Impuls und Materie(?) oder was auch immer nicht schneller als Lichtgeschwindigkeit gehen. Eines davon geht aber schneller. Das andere geht halt nicht schneller, weil Lichtgeschwindigkeit die Grenze ist und man endlos Energie bräuchte. Ich glaube, Heise hatte das mal erwähnt.

    Und noch was: Die meisten Sprachen sind z.B. LALR(1) weil die Parser sonst zu aufwendig werden.
    Das heisst aber nicht, das man keine LALR(2)- oder LL(2)-Programme schreiben kann. Man muss dann dem Compiler halt "Tipps" geben. Bei .NET geht das vielleicht nicht. Aber bei Java gibts Annotationen. Damit ginge das. Bei Java ist das natürlich nicht nötig. Aber es könnte ja mal Konfigurations- oder Computer-Sprachen geben, wo man dadurch übersichtlicheren Code hin bekäme und es einem das wert wäre.

    Aber solche Themen sind natürlich nur für Leute, die wirklich Theorie-Vorlesungen besucht haben. Die anderen heulen gleich rum das sie zu dumm sind.

    Ein Stealth-Fighter schickt fast keine Radarstrahlen zurück. Aber es strahlt sie an die Umgebung ab.
    Ein Radargerät pingt in die Richtung vom Fighter(weil es sich dreht also überall hin) und das zweite Radargerät kriegt die zerstreuten Signale. TV-Bericht: "Die neuen kleinen Antennen auf den Radaranlagen weisen auf die neue Vernetzgung von Radarstationen gegen Stealth-Fighter hin".
    Und so ein Inder meinte: Mit meinem tollen Wetter-Radar (deutsche Radarstation) sehe ich den Stealhfighter auch am Kondenswasser.

    Ein optisches Gerät kann nicht feiner auflösen als die Wellenlänge oder sowas. Das krasse Super-Mikroskop wofür evtl. ein Deutscher (IBM Schweiz?) den Nobelpreis bekommen hat, arbeitet daher mit ZWEI UNABHÄNGIGEN Optischen Messgeräten und kann dadurch feiner "schauen" als die Wellenlänge womit es arbeiten muss.

    Lern es endlich: Physikalische Probleme umgeht man, wenn einem ein Weg einfällt.
    Und bei Gödel geht das auch.

    Du baust Dir ja keine Flügel an die Arme.
    Du beschleunigst einen Auftriebs-Körper (Flugzeug-Flügel) indem Du volle Kanne vorwärts fährst, und dadurch die Mühle hochkommt. "Das ist doch voll dumm. Nach vorne fahren damit ich hoch komme. Ich glaube nicht an Flugzeuge."

    Oder halt die Flügel schnell um eine Achse drehst und sie Rotoren nennst und die Mühle Hubschrauber.

    Leute wie Du hätten sich vielleicht Nerd-Kappen gebaut wo die Propeller oben am Kopf sind und Dich nach oben ziehen sollen... Cessna und die Wright-Brothers hingegen haben die Flügel nach vorne zeigen lassen. Das waren halt keine Dumm-Nerds.

  7. Re: Correctnes by construction

    Autor: Wyv 18.02.10 - 10:01

    >>Das heisst aber nicht, das man keine bewiesene Software >>abliefern kann.

    Richtig. Aber der Anspruch dadurch nur noch bewiesene Software abzuliefern, ist dadurch trotzdem nicht haltbar. Das wird spätestens bei der Benutzerinteraktion zu einem Problem.

  8. Re: Correctnes by construction

    Autor: Saarländer 18.02.10 - 10:55

    Wyv schrieb:
    --------------------------------------------------------------------------------
    > >>Das heisst aber nicht, das man keine bewiesene Software >>abliefern
    > kann.
    >
    > Richtig. Aber der Anspruch dadurch nur noch bewiesene Software abzuliefern,
    > ist dadurch trotzdem nicht haltbar. Das wird spätestens bei der
    > Benutzerinteraktion zu einem Problem.

    Was soll daran ein Problem sein.
    Man beweist, das nur saubere Zustände erreicht werden können.

    Wenn benutzte (M$-)Libs unsicher sind, ist das was anderes.
    Daher gibts ja diese Vor-Bedingungen.
    Die Nachbedingungen sind dann im Prinzip Annotationen, was überhaupt bewiesen werden soll.
    Assertions (?). In Eifel ist das üblich. Durch Annotationen in Java wäre das auch mal nett.
    Dann könnte man jede zehnte Transaktion mit eingeschalteten Assertions laufen lassen, um zu sehen, ob was schief geht oder eine böse Library falsche Parameter oder unzulässige Daten liefert: "Ich will -5 Waschmaschinen bestellen. Überweis das Geld auf meine Kreditkarte".

    Bei User-Daten stellt sich die Frage, ob sie überprüfbar sind. Aber dann ist das u.U. kein informatisches Problem. Z.B. ob jemand seine Bestellung bezahlen kann und anklickt "ich werde bezahlen" kann es ja gelogen sein. Oder Bestell-Nomaden usw.

    Bei Fremd-Daten und Fremd-Formaten wie z.b. Bildern in Browsern hat man solche Probleme auch. Seit neuestem auch häufiger mit PDF-Dokumenten. Aber auch sowas sollte auch machbar sein.
    Das ist aber eher eine andere Sorte Problem. Bzw. mangelnde Definition und Überprüfung der Vorbedingungen.

    Korrektur im letzten Absatz:
    Falsch: "Flügel nach vorne zeigen lassen"
    Richtig: "Propeller nach vorne zeigen lassen"

  9. Re: Correctnes by construction

    Autor: 16Bitiges Bit 19.02.10 - 14:45

    Java hat doch auch Assertions.

  1. Thema

Neues Thema Ansicht wechseln


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

Stellenmarkt
  1. Knipping Kunststofftechnik Gessmann GmbH, Gummersbach
  2. Nord-Micro GmbH & Co. OHG a part of Collins Aerospace, Frankfurt am Main
  3. PDV-Systeme GmbH, Dachau
  4. ZIEHL-ABEGG SE, Künzelsau

Golem pur
  • Golem.de ohne Werbung nutzen

Anzeige
Spiele-Angebote
  1. 4,96€
  2. 47,49€
  3. 1,99€
  4. 4,99€


Haben wir etwas übersehen?

E-Mail an news@golem.de


In eigener Sache: Aktiv werden für Golem.de
In eigener Sache
Aktiv werden für Golem.de

Keine Werbung, kein unerwünschtes Tracking - kein Problem! Wer Golem.de-Inhalte pur nutzen möchte, hat neben dem Abo Golem pur jetzt eine weitere Möglichkeit, Golem.de zu unterstützen.

  1. Golem Akademie Von wegen rechtsfreier Raum!
  2. In eigener Sache Wie sich Unternehmen und Behörden für ITler attraktiv machen
  3. In eigener Sache Unser Kubernetes-Workshop kommt auf Touren

Need for Speed Heat im Test: Temporausch bei Tag und Nacht
Need for Speed Heat im Test
Temporausch bei Tag und Nacht

Extrem schnelle Verfolgungsjagden, eine offene Welt und viel Abwechslung dank Tag- und Nachtmodus: Mit dem Arcade-Rennspiel Heat hat Electronic Arts das beste Need for Speed seit langem veröffentlicht. Und das sogar ohne Mikrotransaktionen!
Von Peter Steinlechner

  1. Electronic Arts Need for Speed Heat saust durch Miami

Fritzbox mit Docsis 3.1 in der Praxis: Hurra, wir haben Gigabit!
Fritzbox mit Docsis 3.1 in der Praxis
Hurra, wir haben Gigabit!

Die Fritzbox 6591 Cable für den Einsatz in Gigabit-Kabelnetzen ist seit Mai im Handel erhältlich. Wir haben getestet, wie schnell Vodafone mit Docsis 3.1 tatsächlich Daten überträgt und ob sich der Umstieg auf einen schnellen Router lohnt.
Ein Praxistest von Friedhelm Greis

  1. Kabelnetz Ausgaben für Docsis 3.1 nicht sehr hoch
  2. Nodesplits Vodafone bietet 500 MBit/s für 20 Millionen Haushalte
  3. Sercomm Kabelmodem für bis zu 2,5 GBit/s vorgestellt

  1. Intel Ponte Vecchio: Sechs 7-nm-Xe-GPUs pro Aurora-Node
    Intel Ponte Vecchio
    Sechs 7-nm-Xe-GPUs pro Aurora-Node

    Intel hat seine 7-nm-Xe-Grafikmodule erläutert: Die heißen intern Ponte Vecchio, nutzen diverse Packaging-Techniken sowie Stapelspeicher und werden in multipler Form gekoppelt. Zusammen mit Sapphire-Rapids-CPUs bilden sie die Basis des Aurora-Exaflops-Supercomputers.

  2. Abgeordnete: CDU-Parteitag soll Huawei Verbot beschließen
    Abgeordnete
    CDU-Parteitag soll Huawei Verbot beschließen

    Eine Reihe von weniger bekannten CDU-Mitgliedern will weiter eine Beteiligung von Huawei am 5G-Ausbau verhindern. Doch der Ausbau mit Huawei-Technik in Deutschland ist bereits in vollem Gang.

  3. Zu niedrig: HP lehnt Übernahmeangebot von Xerox ab
    Zu niedrig
    HP lehnt Übernahmeangebot von Xerox ab

    HP Inc sieht sich mit 33 Milliarden US-Dollar von Xerox stark unterbewertet. Der Verwaltungsrat ist aber offen, andere Optionen für ein Zusammengehen mit Xerox zu erörtern.


  1. 01:00

  2. 23:59

  3. 20:53

  4. 20:22

  5. 19:36

  6. 18:34

  7. 16:45

  8. 16:26