Gibt es beweisbar real-world Sprachen? (Scala?)

https://stackoverflow.com/questions/4065001

27-09-2019
|

Frage

Ich habe gelernt, über formalen Systeme an der Universität, aber ich war enttäuscht, wie sie es nicht taten scheint in der realen Welt verwendet werden.

Ich mag die Idee, in der Lage, zu wissen, dass einige Code (Objekt, eine Funktion, was auch immer) arbeitet, nicht durch Tests, sondern von Beweis .

Ich bin sicher, wir sind alle vertraut mit den Parallelen, die zwischen physikalischen Engineering und Software-Engineering nicht vorhanden sind (Stahl verhält sich vorhersagbar, Software kann alles tun - wer weiß), und ich würde gerne wissen, ob es alle Sprachen, die der Einsatz in der realen Welt sein können (für einen Web-Framework fragen zu viel verlangt?)

Ich habe wie scala interessante Dinge über die Testbarkeit von funktionalen Sprachen zu hören.

Als Software Ingenieure , welche Möglichkeiten haben wir?

Lösung

Ja, es gibt Sprachen konzipiert für beweisbar korrekte Software zu schreiben. Einige sind sogar in der Industrie verwendet. Spark-Ada wahrscheinlich das bekannteste Beispiel ist. Ich habe bei Praxis Critical Systems Limited ein paar Leuten gesprochen, die es für den Code verwendet, auf Boings läuft (für Motorüberwachung) und es scheint ganz nett. (Hier ist ein großer Zusammenfassung / Beschreibung der Sprache Diese Sprache und flankierende Nachweis-System verwendet.) die zweite Technik nachstehend beschrieben. Es ist nicht einmal die dynamische Speicherzuordnung unterstützen!

Mein Eindruck und Erfahrung ist, dass es zwei Techniken für die richtige Software zu schreiben:

Technik 1: Schreiben Sie die Software in einer Sprache, die Sie bequem sind mit (C, C ++ oder Java zum Beispiel). Nehmen Sie eine formale Spezifikation solchen Sprache, und beweisen Sie Ihr Programm korrekt ist.

Wenn Ihr Ziel ist es 100% korrekt zu sein (was meistens eine Anforderung in der Automobil- / Luft- und Raumfahrtindustrie) Sie wenig Zeit Programmierung verbringen würden, und mehr Zeit Proving.
Technik 2: Schreiben Sie die Software in einer etwas unbeholfenen Sprache (eine Teilmenge von Ada oder gezwickt Version von OCaml zum Beispiel) und den Korrektheitsbeweis auf dem Weg zu schreiben. Hier Programmierung und Erprobung geht Hand in Hand. Programmierung in Coq entspricht sie sogar komplett! (Siehe Curry-Howard Korrespondenz )

In diesen Szenarien werden Sie immer mit einem korrekten Programm beenden. (Es wird ein Fehler garantiert wird in der Beschreibung verwurzelt sein.) Sie werden wahrscheinlich mehr Zeit damit verbringen, über die Programmierung, aber auf der anderen Seite Sie beweisen es auf dem Weg zu korrigieren.

Beachten Sie, dass beiden Ansätze Scharniere auf der Tatsache, dass Sie eine formale Spezifikation zur Hand haben (wie sonst würden Sie sagen, was richtig / falsch Verhalten ist) und eine formal definierte Semantik der Sprache (wie sonst würden Sie in der Lage zu sagen, was das tatsächliche Verhalten des Programms ist).

Hier sind ein paar Beispiele für formale Ansätze. Wenn es "real-world" ist oder nicht, hängt davon ab, wen man fragt: -)

Das Coq Theorembeweisers: mit Coq Programmierung (Technik 2)
ESC / Java (Technik 1, weder Ton noch vollständig obwohl)
Spec # (Technik 1, weder Ton noch vollständig obwohl)
Warum / Krakatoa (Technik 2, basierend auf Java)

Ich kenne nur eine "beweisbar korrekte" Web-Applikationssprache : UR . Ein Ur-Programm, dass „durch den Compiler geht“ garantiert nicht:

von jeder Art von Code-Injection-Angriffe
Zurück ungültige HTML
enthalten tot intra-Anwendung Links
Haben Sie Diskrepanzen zwischen HTML-Formularen und den von ihren Lenkern erwarteten Felder
Fügen Sie clientseitigen Code, der falsche Annahmen über die „AJAX“ -Stil Dienste macht, dass der Remote-Web-Server bietet
Versuch ungültig SQL-Abfragen
Verwendung unangebrachte Serialisieren oder Deserialisieren in Kommunikation mit SQL-Datenbanken oder zwischen Browser und Web-Server

Andere Tipps

Um diese Frage zu beantworten, müssen Sie wirklich definieren, was Sie unter „beweisbar“ bedeuten. Als Ricky wies darauf hin, jede Sprache mit einem Typ-System ist eine Sprache, mit einem eingebauten in Proof-System, das jedes Mal läuft Sie Ihr Programm kompilieren. Diese Beweissysteme sind fast immer traurig impotent - Beantwortung von Fragen wie String vs Int und die Vermeidung von Fragen wie „ist die Liste sortiert?“ - aber sie sind Beweis Systeme none-the-less

Leider ist die anspruchsvollere Ihres Beweis Ziele, desto schwieriger ist es mit einem System zu arbeiten, die Ihre Beweise prüfen. Diese eskaliert ziemlich schnell in Unentscheidbarkeit, wenn Sie die schiere Größe der Klasse von Problemen berücksichtigen, die auf Turingmaschinen unentscheidbar sind. Sicher, man kann theoretisch tun grundlegenden Dinge wie die Richtigkeit Ihrer Sortieralgorithmus zu beweisen, aber etwas mehr als das wird sehr dünnes Eis betreten werden.

Auch etwas Einfaches wie die Richtigkeit eines Sortieralgorithmus zu beweisen, erfordert ein vergleichsweise hoch entwickelte Proof-System. (Anmerkung: Da wir bereits festgestellt haben, dass Typ-Systeme sind ein Beweis System in die Sprache gebaut, werde ich über die Dinge in Bezug auf die Typentheorie zu reden, anstatt meine Hände winken noch energischer) ich ziemlich sicher bin, dass ein Vollkorrektheitsbeweis auf Liste Sortierung würde irgendeine Form abhängiger Arten benötigen, sonst haben Sie keine Möglichkeit relative Werte auf der Typebene zu referenzieren. Dies beginnt sofort in Bereiche des Typs Theorie zu brechen, die sein unentscheidbar gezeigt wurden. So, während Sie Korrektheit auf Ihrer Liste Sortieralgorithmus zu beweisen, können in der Lage sein, die einzige Art und Weise zu tun, wäre es, ein System zu verwenden, die auch Sie erlaubt, Beweise zu äußern, die sie nicht überprüfen können. Ich persönlich finde das sehr beunruhigend.

Es gibt auch die Einfachheit der Nutzung Aspekt, den ich früher erwähnt. Je anspruchsvoller Ihre Art System, das weniger angenehm ist, es zu benutzen. Das ist keine feste Regel, aber ich denke, es ist für den größten Teil gilt. Und wie bei jedem formalen System, werden Sie oft feststellen, dass der Beweis auszudrücken, ist mehr Arbeit (und fehleranfällig) als die Umsetzung in erster Linie zu schaffen.

Mit allem, was aus dem Weg, es ist erwähnenswert, dass Scala Typ-System (wie Haskell) ist Turing-Complete, was bedeutet, dass Sie theoretisch verwenden Sie es für alle entscheidbar Eigenschaft über Ihren Code zu beweisen, vorausgesetzt, dass Sie Ihren Code in einer solchen Art und Weise geschrieben, dass es solche Beweise zugänglich ist. Haskell ist mit ziemlicher Sicherheit eine bessere Sprache für diese als Java (seit Typ-Level-Programmierung in Haskell zu Prolog ähnlich ist, während Typ-Level-Programmierung in Scala ähnliche SML ist). Ich rate nicht, dass Sie Scala oder Haskell Typ-Systeme auf diese Weise (formale Beweise der algorithmischen Korrektheit) verwenden, aber die Option ist theoretisch zur Verfügung.

Insgesamt denke ich, dass der Grund, warum Sie nicht formale Systeme in der „realen Welt“ kommt von der Tatsache gesehen, dass formale Beweis Systeme der gnadenlosen Tyrannei des Pragmatismus ergeben haben. Wie ich bereits erwähnt, gibt es so viel Mühe in Crafting Ihre Richtigkeit Abzüge auf, dass es fast nie lohnt,. Die Industrie entschied mich für eine lange Zeit her, dass es leichter war, Ad-hoc-Tests zu erstellen, als es durch jede Art von analytischem formaler Argumentation Prozess zu gehen.

typisierten Sprachen beweisen das Fehlen bestimmter Kategorien von Schuld. Je mehr die Art System vorgeschoben, desto mehr Fehler sie das Fehlen nachweisen können.

Für den Nachweis, dass ein ganzes Programm funktioniert, ja, du bist Stepping außerhalb der Grenzen der gewöhnlichen Sprachen, in denen Mathematik und Programmierung treffen einander die Hände schütteln und dann weiter mit griechischen Symbolen darüber zu reden, wie Programmierer können Griechisch nicht umgehen Symbole. Das entspricht etwa der S davon sowieso.

Sie fragen eine Frage viele von uns im Laufe der Jahre gefragt. Ich weiß nicht, dass ich eine gute Antwort haben, aber hier sind einige Stücke:

Es gibt wohlverstandenen Sprachen mit der Möglichkeit der heute im Einsatz bewährt werden; Lisp über ACL2 eines ist, und natürlich Schema hat eine gut verstanden als auch formale Definition.
eine Reihe von Systemen hat versucht, rein funktionale Sprachen zu verwenden, oder fast Reine, wie Haskell. Es gibt ein gutes Stück von formalen Methoden der Arbeit in Haskell.
Going 20+ Jahre zurück, gab es eine kurzlebige Sache für die Verwendung von hand Nachweis einer formalen Sprache, die wurde dann konsequent in einer kompilierten Sprache übersetzt. Einige Beispiele waren IBMs Software Reinraum-, ACL, Zigeuner, und Rose aus Computational Logic, John McHugh und meiner Arbeit auf vertrauenswürdige Sammlung von C, und meine eigene Arbeit auf der Hand sicher für C-Systeme zu programmieren. Diese alle haben eine gewisse Aufmerksamkeit, aber keiner von ihnen machte es viel in die Praxis umsetzen.

Eine interessante Frage zu stellen, denke ich, ist das, was würden hinreichende Bedingungen formale Ansätze in der Praxis zu bekommen sein? Ich würde gerne ein paar Vorschläge hören.

Sie können untersuchen rein funktionalen Sprachen wie Haskell, die verwendet werden, wenn einer Ihrer Anforderungen ist Beweisbarkeit .

Diese wird ein Spaß zu lesen, wenn Sie daran interessiert sind über funktionale Programmiersprachen und rein funktionalen Programmiersprachen.

reale Welt Verwendung solcher beweisbar Sprachen wäre unglaublich schwierig sein, zu schreiben und zu verstehen afterwoods. die Geschäftswelt braucht funktionierende Software, schnell.

„beweisbar“ Sprachen nur tun sie nicht Maßstab für das Schreiben / ein großes Projekt der Codebasis zu lesen und scheinen nur auf die Arbeit in kleinen und isolierten Anwendungsfälle.

Ich bin in zwei beweisbar Sprachen beteiligt. Die erste ist die Sprache von Perfect Entwickler unterstützt, ein System zur Angabe Sotfware, zu verfeinern und Generieren von Code. Es ist seit einigen großen Systemen, einschließlich PD selbst, und es wird gelehrt, in einer Reihe von Universitäten eingesetzt. Die zweite beweisbar Sprache, die ich beteiligt bin eine beweisbar Teilmenge von MISRA-C ist, finden Sie unter C / C ++ Überprüfung Blog mehr.

Sehen Sie sich Omega .

Die Einführung enthält eine relativ schmerzlos Implementierung von AVL-Bäumen mit Korrektheitsbeweis enthalten.

Scala sollte „reale Welt“ sein, so dass keine Anstrengungen unternommen wurden, um es beweisbar zu machen. Was können Sie in Scala zu tun ist, funktionalen Code zu erzeugen. Functional-Code ist viel einfacher zu testen, was meiner Meinung nach ist ein guter Kompromiss zwischen „realen Welt“ und Beweisbarkeit.

EDIT ===== Entfernt meine falschen Vorstellungen über ML „beweisbar“ zu sein.

My (umstrittene) Definition von "real-world" im Zusammenhang mit beweisbar-korrektem Code ist:

Es muss ein gewisses Maß an beinhalten Automation , sonst wirst du viel zu viel Zeit Proving und den Umgang mit dem unordentlichen kleinen Details verbringen, und es wird völlig unpraktisch sein (außer vielleicht für Satelliten Kontrolle Software und diese Art der Sache, für die Sie tatsächlich Unsummen auf sorgfältige Kontrollen verbringen mögen).
Es muss ein gewisses Maß an der funktionalen Programmierung unterstützen , die Sie Code schreiben, hilft das sehr modular aufgebaut ist, wiederverwendbar und einfacher zu Grund über. Offensichtlich funktionale Programmierung ist nicht erforderlich für das Schreiben oder beweisen Hallo Welt, oder eine Vielzahl von einfachen Programmen, aber an einem bestimmten Punkt, die funktionale Programmierung nicht wurde sehr nützlich.
Während man nicht unbedingt hat, um Ihren Code in einer Mainstream-Programmiersprache zu schreiben, als Alternative, sollten Sie zumindest die Lage sein, maschinell übersetzt Ihren Code in einigermaßen effizient Code geschrieben in einer Mainstream-Programmiersprache, in zuverlässiger Art und Weise.

Die oben genannte sind relativ universelle Anforderungen. Andere, wie die Fähigkeit, zwingend notwendig, Code zu modellieren, oder die Fähigkeit zu beweisen, Funktionen höhere Ordnung zu korrigieren, kann für einige Aufgaben wichtig oder notwendig sein, aber nicht alle.

Im Hinblick auf diese Punkte, viele der Werkzeuge aufgelistet in diese Blog-Post von mir kann nützlich sein - obwohl sie fast alle entweder neu und experimentell oder fremd für die große Mehrheit der Industrie-Programmierer sind. Es gibt einige sehr reifen Tools abgedeckt dort aber.

Wie wäre es Idris und Agda ? Reale Welt genug?

Als gutes richtiges Beispiel, gibt es ein Projekt, das darauf abzielt, eine in Agda geschrieben HTTP REST-Bibliothek überprüft bereitzustellen, die so genannte Lemmachine:

Lizenziert unter: CC-BY-SA mit Zuschreibung

Nicht verbunden mit StackOverflow