Gibt es kommentierte formale Verifizierungssysteme für reine funktionale Programmiersprachen?

25

ACSL (Ansi C Specification Language) ist eine mit speziellen Kommentaren versehene Spezifikation für C-Code, mit der C-Code formal verifiziert werden kann.

Ich habe es nicht untersucht, aber ich stelle mir vor, dass die in ACSL- Verifizierern verwendeten formalen Methoden Hoare Logic ähneln würden. Für reine funktionale Sprachen wie Haskell kann ich mir allerdings nicht vorstellen, welche Art von Formalismus für die formale Verifikation verwendet wird.

Hat jemand etwas Ähnliches wie ACSL gemacht , aber für eine reine Funktionssprache? Wenn nein, wurden Untersuchungen zur formalen Verifizierung mit spezifikationsbezogenen Anmerkungen für funktionale Sprachen durchgeführt?

Ich weiß, dass es abhängiges Tippen gibt, das von vielen Sprachen (Agda, Idris usw.) unterstützt wird, aber in Haskell ist das abhängige Tippen schwierig, ohne einige (unlesbare?) Typenzauberer auszuführen. In diesem Sinne, und da Haskell so viel bessere Bibliotheksunterstützung als Agda und Idris hat, glaube ich, dass ein solches System zur funktionalen formalen Verifizierung nützlich sein könnte, aber ich weiß nicht, ob dies erforscht wurde oder nicht.

Nathan BeDell
quelle

Antworten:

13

Honda und Yoshida

(wahrscheinlich) Pionier der Hoare-Logik für rein funktionale Sprachen. Diese Arbeit basiert auf Hennessy-Milner-Logik und Milners Kodierung von Funktionen in Prozesse, wie hier beschrieben:

Die Arbeit von Régis-Gianas et al., Die in einer anderen Antwort erwähnt wurde, ähnelt der ersten Arbeit von Honda / Yoshida. Dies wurde auf effektive Sprachen im ML-Stil erweitert:

Die genannten Logiken werden als beobachtend vollständig bezeichnet, dh die operationelle und die logische Semantik stimmen überein. Arthur Charguéraud verwendete diese Vervollständigungen für seine Arbeiten zur Überprüfung von Funktionsprogrammen im Hoare-Stil in Coq.

Martin Berger
quelle
15

F

Es scheint eine enge Übereinstimmung zwischen den Verfeinerungstypen und den ACSL-ähnlichen Notationen zu geben.

Schließlich kann ich nur empfehlen, Agda und Idris, die sich nach Haskell kompilieren lassen, genauer zu betrachten und dem Benutzer eine brauchbare Programmiersprache (insbesondere Idris) zur Verfügung zu stellen. Ich vermute, es ist möglich, Haskell-Bibliotheken ohne großen Aufwand in Idris-Code zu integrieren.

Cody
quelle
ohne zu viel Mühe - nicht wirklich. Idris ist standardmäßig streng und Haskell ist faul; das allein stellt ein großes Problem dar. Die Kompatibilität mit Haskell hatte für das Design von Idris ebenfalls nie eine sehr hohe Priorität.
Bartek Banachewicz
Meinetwegen. Agda prüft die Kündigung jedoch standardmäßig, sodass Dinge wie Strenge theoretisch kein Problem darstellen . Natürlich kann die Laufzeit dramatisch abweichen.
Cody
8

Es ist ein Papier , in dem diesjährigen ICFP , Verfeinerung Typen für Haskell . Das Papier befasst sich eher mit der Terminierungsprüfung als mit der vollständigen Hoare-Logik, aber hoffentlich ist dies ein Anfang in dieser Richtung.

Der entsprechende Arbeitsabschnitt in diesem Artikel enthält einige Hinweise, wie Xu, Peyton-Jones und Claessens statische Vertragsprüfung für Haskell sowie Sonnex, Drossopoulou und Eisenbachs Zeno und Vytiniotis, Peyton-Jones, Claessen und Rosens Halo .

Ohad Kammar
quelle
1

Unsere Arbeit an der weichen Überprüfung von Verträgen ist verwandt. Auf der OOPSLA 2012 und der ICFP 2014 können Sie Verträge schreiben, die den ACSL-Spezifikationen sehr ähnlich sind, und diese dann entweder statisch überprüfen oder zur Laufzeit dynamisch überprüfen.

Sam Tobin-Hochstadt
quelle