Formale/Mathematische Methoden in der Softwareentwicklung
-
Hallo,
habe vor Kurzem mein Informatikstudium an der Uni begonnen und mir gefällt die Exaktheit der Mathematik und deren Wahrheitsfindung mittels Beweismethoden. In der Softwareentwicklung hingegen wird, auch in der Industrie, oft viel nach dem Prinzip "Trial and Error" rumprobiert.
Ich habe mich gefragt, ob man die Exaktheit der Mathematik nicht auf Teilbereiche der Softwareentwicklung anwenden könnte. Gibt es hier irgendwelche Ansätze? Die theoretische Informatik fokusiert ja Berechenbarkeit und Komplexität. Gibt es aber auch Methoden, die mehr auf die problemorientierte Entwicklung ausgerichtet sind?
Beispiele:
- Kann man die Korrektheit eines beliebigen (Teil)programms beweisen?- Kann man die Äquivalenz zweier Programme formal zeigen?
Beispiel: zwei ineinander geschachtelte Schleifen, welche n Operationen durchführen, werden umgeformt, sodass der Programmcode anders ist, jedoch für jede Eingabe dasselbe Ergbenis liefert.- Könnte man ein Kalkül entwerfen, das die Effizienz (verteilter) Softwarearchitekturen untersucht? Gibt es ein formales Kalkül, welches Aussagen zu objektorientierten Architekturen liefert? Beispielsweise zur Untersuchung entstehender Kopplungs-/Abhängigkeitsgrade beim Einsatz / Weglassen bestimmter Patterns
Ich denke, man versteht in etwa, worauf ich hinaus will. Mich würden theoretische Ansätze interessieren, die es zu diesen Themen gibt, sofern sie überhaupt durchführbar sind.
Hoffentlich sind meine Fragen nicht zu naiv
Vielen Dank
-
Ja, solche Techniken gibt es, aber dies ist in der Regel nur bei Sprachen ohne Seiteneffekte praktisch durchführbar. Warte mal bis du funktionale Programmierung machst, da wird das dann gemacht. Ein funktionales Programm liest sich dann auch ungefähr so wie Mathematik.
-
sarge0 schrieb:
- Kann man die Korrektheit eines beliebigen (Teil)programms beweisen?
-
In der imperativen Programmierung ist das schwierig. Willkommen in der Funktionalen Programmierung. -> "Algebra of Programming" aber als Einstieg ist wohl jedes Buch zu Haskell oder Scheme ganz gut.
Kann man die Äquivalenz zweier Programme formal zeigen?
Im Allgemeinen nicht.
Warte mal bis du funktionale Programmierung machst
Wurde bei uns nie behandelt. Musste ich mir selbst aneignen.
Zum Hoare-Kalkuel: Es ist eher unpraktikabel.
-
Es gibt ein ganzes Teilgebiet der Informatik die sich damit befasst. Das Gebiet nennt sich Formale Methoden und wahrscheinlich gibts sogar einen Lehrstuhl an deiner Uni der sich damit beschäftigt.
Um eine deiner Fragen zu beantworten: es ist nicht möglich die Korrektheit eines beliebigen Programms zu beweisen. Das Problem ist äquivalent zum Halteproblem und damit nicht entscheidbar.
Einen schönen Einblick in das Gebiet gibt das Buch Formale Modelle der Softwareentwicklung | ISBN: 9783834806697.
-
Ich habe nur das Inhaltsverzeichnis gelesen, bin aber wenig begeistert.
-
Hallo,
Danke für eure Beiträge.
Das mit dem Buch klingt interessant, das hätte ich mir als Einstieg vielleicht mal angesehen.@knivil: Vielleicht kannst du kurz deine Kritik erläutern, warum du wenig begeistert bist?
-
Das Problem: In der Informatik sind alles formale Methoden. Aber sie sind "weich" ohne jede Garantie. Gerade die Ansaetze modell-driven oder test-driven sind fuer mich eher unbefriedigend und Thema des Buches ist eben Modellchecking. Weiterhin scheint es eher eine Einfuehrung in Tools zu sein, als etwas handfestes. Aber Tools Ansaetze und Technologie aendern sich staendig. Petrinetze sind okay, aber dafuer braucht man sich dieses Buch wohl nicht zu kaufen. Die Einfuehrung in Java am Ende halte ich fuer ueberfluessig, da gibt es bessere. Der Preis: 35 Euro fuer 300 Seiten wuerde ich persoenlich aus den genannten Gruenden nicht ausgeben.
Da es immer noch um Programme geht und diese in einer Sprache geschrieben werden muessen, sollte die Sprache eben schon "Beweisbarkeit" unterstuetzen. Das bieten funktionale Sprachen (prinzipiell auch mit imperativen Sprachen moeglich, aber wesentlich aufwendiger). Deswegen ist es wohl fuer den Anfang guenstig, eine solche Sprache zu lernen. Haskell oder ML (OCaml) sind z.B. geeignet. Wohl oder uebel gehts dann weiter Richtung Lambda-Kalkuel. Buecher, Literatur als auch Videolectures gibt es als Einfuehrung in diese Sprachen reichlich. Da sind zum einen die SCIP video lectures zu nennen oder von Erik Mejer unter http://www.cs.nott.ac.uk/~gmh/book.html . Auch braucht man sich nicht jedes Buch zu kaufen, da viele im Internet verfuegbar sind. Entweder illegal als eBook oder eben frei als Html. Von deutschen Uebersetzungen rate ich aber ab. Wenn du soweit bist, dann findest du wahrscheinlich den weiteren Weg selbst.
PS: Ich habe mir 2 Buecher nachtraeglich gekauft, die mir sehr gut gefallen haben, obwohl ich sie schon durchgearbeitet hatte.
-
Agda oder Epigram wären Kandidaten für Sprachen, die deinen Wünschen nahe kommen.
-
Naja, ein wenig muß man noch relativieren. Normalerweise sind die Spezifikationen viel viel fehlerhafter als die Übersetzung der Spezifikationen in Code.
-
Es gibt viele Ansätze formale Methoden einzusetzen. Hier wird noch recht viel Forschung betrieben und es ist noch gar nicht klar was am erfolgversprechendsten ist.
Nur um ein paar konkrete Projekte zu nennen:
http://research.microsoft.com/en-us/projects/specsharp/krml160.pdf
http://www.key-project.org/
http://www.event-b.org/
http://klee.llvm.org/
http://www.microsoft.com/whdc/devtools/tools/sdv/default.mspx
-
Und wenn man weg von den imperativen Sprachen geht, bekommt man das meiste geschenkt.
-
ja, wir freuen uns alle, wenn das Zeitalter der echten OOP endlich anbricht.
-
Für den Bereich Model Checking finde ich folgendes Buch ganz empfehlenswert:
-
knivil schrieb:
Und wenn man weg von den imperativen Sprachen geht, bekommt man das meiste geschenkt.
-
Klar habe ich mir angesehen, um was es geht. Ersten zwei Links: ... of object-oriented ... . Automatisch generierte Tests ... QuickCheck fuer Haskell wurde auch fuer viele andere Sprachen (z.B. C#) portiert und angepasst, es ist leicht mit einem Codecoveragetool zu koppeln wie HPC. Und Brian Beckman meinte in einem Interview, Scheme schon mal auf Kernelebene fuer Scheduling eingesetzt zu haben. Die Tools fuer diverse Dialekte von ML sind noch wesentlich maechtiger, habe ich mir sagen lassen, aber noch keine Erfahrung damit gemacht
Jetzt kann man natuerlich ein Modell erstellen, es verifizieren und daraus sich sein Programm generieren. Oder aber Korrektheit per Konstruktion erzwingen. Ersteres ist nur ungemein schwieriger.
Und du hast dir meinen Beitrag nicht durchgelesen? Es gibt nur formale Methoden in der Informatik oder gar keine ...
-
Das Halte-Problem ist auch für funktionale Programmiersprachen unentscheidbar.
Auch sind funktionale Programmiersprachen nicht generell besser für Verifikationsansätze geeignet als imperative Programmiersprachen. So ist z.B. zur Zeit predicate abstraction als Verifikationstechnik sehr modern und dessen berühmtester Vertreter BLAST (http://mtc.epfl.ch/software-tools/blast/index-epfl.php) unterstützt keine Rekursion.
Desweiteren wird in der Praxis nunmal hauptsächlich in objekt-orientierten bzw. imperativen Sprachen programmiert. Deshalb besteht ein großes wirtschaftliches Interesse daran, insbesondere für imperative Programmiersprachen praxistaugliche Verifikationstools zu entwickeln.
-
Das Halte-Problem ist auch für funktionale Programmiersprachen unentscheidbar.
Fuer beliebige Programme ja, aber darum geht es nicht. Wenn ich aber per Konstruktion Fehler ausschliesse (bzw. stark vermeide).
Auch sind funktionale Programmiersprachen nicht generell besser für Verifikationsansätze geeignet als imperative Programmiersprachen.
Doch, da die Sprache schon vieles ausschliesst, dass in imperativen beachtet werden muss. Hindley–Milner Typsystem etc. keinen Zustand ... Auch brauche ich im Nachhinein nicht verifizieren, da es per Konstruktion korrekt ist. Beispiel: Haskell Symposium 2008. Neil Mitchell: Not All Patterns, But Enough - an automatic verifier for partial but sufficient pattern matching
Predicate abstraction is a technique that is used to prove properties of infinite state systems.
Tja, und wenn man gar keinen oder nur sehr wenig Zustand wie bei funktionalen Sprachen hat, dann kann man sich das sparen.
Desweiteren wird in der Praxis nunmal hauptsächlich in objekt-orientierten bzw. imperativen Sprachen programmiert.
Zeit zum Umdenken! Aber einem Manager das klar zu machen ist schwierig. Javaprogrammierer sind ja so billig.
-
wie wär's damit: Softwaresysteme vor allem einfach und klar zu formulieren.
Fehler verstecken sich bevorzugt in schwer verständlichen, mißverständlichen, überkomplexen oder sonstwie unklaren Gegenden des Quellcodes.
Abhilfe erfordert den Einsatz von Programmiersprachen, die von syntaktischem Ballast und überflüssigem Klein-Klein befreit sind.
Das ist sogar unabhängig von den Programmierparadigmata, eher eine prinzipielle Frage: wieviel Syntax ist wirklich nötig, um ein Programm zu formulieren ? Das dürfte oft überraschend wenig sein.
-
Wie du "Fehler" per Konstruktion ausschließen willst, musst du mir aber noch erklären ;). Dein Paper habe ich mir allerdings auch nicht angeschaut.
Tja, und wenn man gar keinen oder nur sehr wenig Zustand wie bei funktionalen Sprachen hat, dann kann man sich das sparen.
Das siehst du leider falsch. Auch beim funktionalen Programmiersprachen kann man zu einem bestimmten Ausführungszeitpunkt einen beliebig großen Zustand durch die verschachtelten Funktionsaufrufe haben. Wenn das nicht so wäre, könnte man nicht das unendlich (beliebig) große Band einer Turingmaschine simulieren, und die Programmiersprache wäre nicht Turning-vollständig.
Es mag ja sein, dass ihr an eurem Lehrstuhl (oder ein anderer) eine tolle neue Verificationstechnik für funktionale Programmiersprachen entwickelt habt, allerdings sollte man ihmo trotzdem auf dem Teppich bleiben und nicht allen anderen Ansätzen die Existenzberichtigung absprechen.
PS:
Paper das dein Paper zitiert: Static contract checking for Haskell:Program errors are hard to detect and are costly both to programmers who spend significant efforts in debugging, and for systems that are guarded by runtime checks. Static verification techniques have been applied to imperative and object-oriented languages, like Java and C#, but few have been applied to a higher-order lazy functional language, like Haskell. In this paper, we describe a sound and automatic static verification framework for Haskell, that is based on contracts and symbolic execution. Our approach is modular and gives precise blame assignments at compile-time in the presence of higher-order functions and laziness.
Das klingt fast so, als ob die Autoren es auch schwieriger ansehen, static analysis bei funktionalen Programmiersprachen zu betreiben.
