Formale/Mathematische Methoden in der Softwareentwicklung
-
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.
-
Das siehst du leider falsch.
Ich meine mit Programmzustand etwas anderes als du.
Ausführungszeitpunkt einen beliebig großen Zustand durch die verschachtelten Funktionsaufrufe haben
Das meine ich eben nicht. Und Turingmaechtigkeit ist hier nicht zentrales Thema, da es mir nicht um beliebige Programme geht.
in the presence of higher-order functions
Ja, das ist schwierig. Aber Neil Mitchell ist eben den anderen Weg gegangen und hat das higher-order-program in ein first-order-program umgewandelt (+ strictness analysis). Das ist ziemlich einfach. So heisst der Titel des Videos: Losing Functions Without Gaining Data - Another Look at Defunctionalisation, das erste war nicht das, was ich meinte. Das Video von 26 Minuten fand ich sehr interessant
In ML oder Haskell ist das Typsystem aequivalent zu einem Theorembeweiser. Damit laesst sich schon viel machen. Zieht man zu den Typen noch mehr Informationen hinzu, kann man noch mehr machen ...
-
knivil schrieb:
Ich meine mit Programmzustand etwas anderes als du.
Ja, eben das falsche
. Nur weil es in rein funktionellen Programmiersprachen keine expliziten Zustandsvariablen gibt, heißt das nicht, dass es keinen Zustand gibt ;).
-
Ja, aber darum muss ich mir doch keine Gedanken machen.
-
Danke für eure Beiträge. Habe mich nun etwas in Haskell eingearbeitet und bin relativ begeistert, wie formal man die Programmierung gestalten kann. Werde mich nun zunächst eingehender mit dieser Sprache beschäftigen.