Was sind gängige formale Techniken, um die Richtigkeit des Funktionscodes zu beweisen?

10

Ich möchte Beweise für Teile eines Haskell-Programms liefern, das ich im Rahmen meiner Abschlussarbeit schreibe. Bisher habe ich jedoch kein gutes Nachschlagewerk gefunden.

Graham Huttons Einführungsbuch Programming in Haskell ( Google Books ), das ich beim Lernen von Haskell gelesen habe, geht auf einige Techniken ein, um über Programme wie z

  • Gleichungsdenken
  • Verwenden nicht überlappender Muster
  • Liste Induktion

in Kapitel 13, aber es ist nicht sehr ausführlich.

Gibt es Bücher oder Artikel, die Sie empfehlen können und die einen detaillierteren Überblick über formale Prüftechniken für Haskell oder anderen funktionalen Code bieten?

reference-request proof-techniques functional-programming books software-verification FK82
quelle

Antworten:

5

Eine der De-facto-Methoden zum Nachweis von Ergebnissen in der funktionalen Programmierung ist die Gruppe von Richard Bird.

Insbesondere fordern Sie einen eingehenden oder zumindest umfassenderen Ansatz für das Argumentationsgleich und die Listeninduktion, der in den Vorlesungen über konstruktive funktionale Programmierung beschrieben wird .

Im Allgemeinen befasst sich der Text "Algebra of Programming" von Bird und de Moor auch mit der Korrektheit funktionaler Algorithmen wie Optimierungs- und dynamischen Programmierproblemen.

Wenn Sie auf andere nützliche Ressourcen für dieses Problem stoßen, erwähnen Sie diese bitte. Vielleicht können wir diesen Beitrag in ein Wiki verwandeln.

Musa Al-hassy
quelle
Vielen Dank! Klar, wenn ich mehr Ressourcen finde, werde ich sie meinem Beitrag hinzufügen.
FK82
6

Sie können mit beginnen

Zu den Themen gehören grundlegende Konzepte der Logik, computergestützte Theoremprüfung, der Coq-Proof-Assistent, funktionale Programmierung, Betriebssemantik, Hoare-Logik und statische Systeme. Die Ausstellung richtet sich an ein breites Spektrum von Lesern, von fortgeschrittenen Studenten bis hin zu Doktoranden und Forschern. Es wird kein spezifischer Hintergrund in Logik oder Programmiersprachen angenommen, obwohl ein gewisser Grad an mathematischer Reife hilfreich sein wird.

Sie können die Teile der Programmiersprachtheorie überspringen (oder überfliegen) und nur lernen, wie man mit formalen Beweisen vom Vorwort bis zu den Grundsätzen umgeht. Das Buch ist wirklich gut geschrieben und aufschlussreich.

Dann möchten Sie vielleicht fortfahren

In diesem Band erfahren Sie, wie Sie Sortieralgorithmen, binäre Suchbäume, ausgeglichene binäre Suchbäume und Prioritätswarteschlangen spezifizieren und überprüfen (deren Richtigkeit beweisen). Bevor Sie dieses Buch verwenden, sollten Sie sich mit diesen Algorithmen und Datenstrukturen vertraut machen, die in jedem Standardlehrbuch für Algorithmen für Studenten verfügbar sind. Sie sollten das gesamte Material in Software Foundations Volume 1 (Logic Foundations) verstehen.

Ein Hinweis zur Warnung: VFA befindet sich noch in der Beta-Version!

Anton Trunov
quelle
(Ihr zweiter Link führt an die falsche Stelle.) Außerdem gibt es in Agda eine verifizierte funktionale Programmierung . die Agda verwendet, formal eine Programmiersprache, aber Unicode verwendet und daher der mathematischen Notation näher kommt.
Musa Al-hassy
Korrigiert, danke. Ja, ich habe VFPiA gelesen, aber es ist nicht nach meinem Geschmack.
Anton Trunov
Vielen Dank für Ihre Antwort! Ich denke, es gibt ein Missverständnis. Ich suche nicht nach funktionalen Techniken zum Testen von Algorithmen (wie zum Beispiel einem Proof-Assistenten), sondern nach Techniken zum Testen von funktionalem Code (zum Beispiel zum Beweisen einer korrekten funktionalen Implementierung eines bestimmten Algorithmus). @ MusaAl-hassy Antwort ist sehr nah an meiner gewünschte Antwort. Falls ich es verpasst habe und die von Ihnen zitierten Bücher auch diesen Aspekt behandeln, würde es Ihnen etwas ausmachen, die relevanten Kapitel hinzuzufügen?
FK82
@ FK82 Hier ist ein Theorem app_assoc : ∀ l1 l2 l3 : natlist, (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)aus dem Kapitel Listen . Sieht dieses Beispiel so aus, wie Sie es interessieren? Sie beginnen mit der funktionalen Programmierung in Coq, gehen dann aber zu den Überlegungen über die Eigenschaften von funktionalen Programmen über. Die Kapitel von Vorwort bis IndPrinciples behandeln beide, und ich würde sagen, dass Programmierung und Argumentation dort miteinander verflochten sind.
Anton Trunov
1
@ FK82 (1) Ich stimme diesem Kommentar voll und ganz zu. (2) Vielleicht möchten Sie sich das Buch "Mit Haskell funktional denken" (2015) von R. Bird ansehen. Das Buch enthält unzählige Beispiele für Überlegungen zu Haskell. (3) Auch "Pearls of Functional Algorithm Design" (2010) desselben Autors kann Ihnen hilfreich sein.
Anton Trunov
5

Es stellt sich heraus, dass eine ausgezeichnete Quelle für Beweisverfahren und Beispiele für den Beweis von Dingen über reine Funktionssprachen Beweisassistenten sind, die normalerweise als Teil ihrer Spezifikationssprache eine reine Funktionssprache enthalten, auf der es möglich ist, gleich zu argumentieren.

Vielleicht möchten Sie ein Buch wie Certified Programing with Dependent Types konsultieren, um eine ausführliche Einführung in diese Art von Argumentation in einem bestimmten Proof-Assistenten, nämlich Coq, zu erhalten.

Cody
quelle
Vielen Dank! Ich suche speziell nach Techniken in Haskell . Mein Beitrag wurde so bearbeitet, dass er den gesamten Funktionscode enthält, aber das liegt weit über meinen Absichten.
FK82
1
Ich bin mir nicht bewusst Systeme Haskell speziell überprüfen entworfen, aber ich mag darauf hinweisen , dass 1) Der Funktionskern von Coq (und Agda) von der Haskell im Wesentlichen nicht zu unterscheiden ist ( mit Ausnahme der Beschränkung auf insgesamt Funktionen) und 2) Programme überprüft in Coq und Agda kann nach Haskell extrahiert werden (obwohl ich glaube, dass die Extraktion nach Haskell in Agda, wo Coq mehr Ocaml-zentriert ist, besser unterstützt wird)
cody
Gut zu wissen! Dies würde jedoch bedeuten, dass ich mein Programm (oder die relevanten Teile) in Coq oder Agda umschreibe. Ich denke nicht, dass das in meinem Fall vernünftig ist.
FK82
Es gibt einige sehr experimentelle "Frontends", die versuchen , Haskell in Isabelle umzuwandeln oder Äquivalenzen mit Isabelle direkt zu beweisen , aber ich würde nicht zu viel Aktien in ihrer Reife halten. Ich denke, das Umschreiben des Codes wäre letztendlich weniger Arbeit.
Cody
4

Ich schlage vor, Programmlogiken zu verwenden. Sie gehen viel besser mit Effekten um als Tippsysteme.

Es gibt zahlreiche Programmlogiken für funktionale Sprachen. Dies wird mit Effekten interessant. Siehe z. B. logisches Denken für Funktionen höherer Ordnung mit lokalem Status .

Die Arbeit von Arthur Charguéraud integriert den Programmlogik-Ansatz mit Proof-Assistenten, siehe z . B. diese Übersichtsseite .

Martin Berger
quelle