Warum wenden die Leute keine formalen Methoden an?

Published on January 23, 2019

Warum wenden die Leute keine formalen Methoden an?

Ursprünglicher Autor: Hillel Wayne
  • Übersetzung
Beim Software Engineering Stack Exchange sah ich die folgende Frage : "Was verhindert die weit verbreitete Einführung formaler Methoden?" Die Frage wurde als voreingenommen geschlossen, und die meisten Antworten waren Kommentare wie "Zu teuer !!!" oder "Die Site ist kein Flugzeug !!!". In gewissem Sinne ist das wahr, aber es erklärt sehr wenig. Ich habe diesen Artikel geschrieben, um ein breiteres historisches Bild der formalen Methoden (FM) zu geben, warum sie nicht wirklich verwendet werden und was wir tun, um die Situation zu korrigieren.

Bevor Sie beginnen, müssen Sie einige Bedingungen formulieren. Tatsächlich gibt es nicht viele formale Methoden: nur ein paar winzige Gruppen . Dies bedeutet, dass verschiedene Gruppen die Begriffe unterschiedlich verwenden. Im weiteren Sinne gibt es zwei Gruppen formaler Methoden:In der formalen Spezifikation wird das Verfassen genauer, eindeutiger Spezifikationen untersucht, und in der formalen Überprüfung werden die Nachweismethoden untersucht  . Dies umfasst sowohl Code- als auch abstrakte Systeme. Wir verwenden nicht nur unterschiedliche Begriffe für Code und Systeme, sondern häufig auch unterschiedliche Tools, um diese zu überprüfen. Um alles noch mehr zu verwirren: Wenn jemand sagt, dass er eine formale Spezifikation erstellt, bedeutet dies in der Regel eine Designüberprüfung. Und wenn jemand sagt, dass er eine formale Überprüfung durchführt, bezieht sich dies normalerweise auf die Überprüfung des Codes.

Der Klarheit halber unterteilen wir die Verifikation für die Code-Verifikation (CV) und die Design-Verifikation (DV) und ebenso die Spezifikationen für CS und DS. Solche Begriffe werden in der breiten FM-Community nicht häufig verwendet. Beginnen wir mit CS und CV und fahren dann mit DS und DV fort.

Darüber hinaus ist eine teilweise Überprüfung möglich , bei der nur eine Teilmenge der Spezifikation überprüft wird, oder eine vollständige Überprüfung . Dies kann der Unterschied zwischen den Nachweisen sein, dass "das System niemals ausfällt und das falsche Passwort nicht akzeptiert" oder "das System niemals ausfällt und das Konto blockiert, wenn Sie dreimal das falsche Passwort eingeben". Grundsätzlich gehen wir davon aus, dass wir eine vollständige Überprüfung durchführen.

Sie sollten auch die Art der Software klären, die wir formalisieren. Die meisten Menschen unterscheiden implizit hochzuverlässige Programme wie medizinische Geräte und Flugzeuge. Die Leute gehen davon aus, dass für sie formale Methoden weit verbreitet sind, im Übrigen werden sie nicht benötigt. Dies ist eine zu optimistische Sichtweise: Die meisten hochzuverlässigen Programme verwenden keine formalen Methoden. Stattdessen konzentrieren wir uns auf „gewöhnliche“ Software.

Abschließend ein Haftungsausschluss: Ich bin kein professioneller Historiker, und obwohl ich versucht habe, die Informationen sorgfältig zu überprüfen, kann der Artikel Fehler enthalten. Außerdem spezialisiere ich mich auf formale Spezifikationen (DS und DV), sodass die Wahrscheinlichkeit von Fehlern größer ist, wenn ich über die Codeüberprüfung spreche. Wenn Sie sehen, schreiben Sie mir, ich werde korrigieren (und wieder: Ich verdiene Geld bei Seminaren über TLA + und Alloy, daher bin ich sehr voreingenommen in Bezug auf diese Sprachen; ich versuche, so objektiv wie möglich zu sein, aber Sie wissen: Voreingenommenheit ist Voreingenommenheit).

Formale Programmierung


Stücklistenspezifikation


Bevor Sie die Richtigkeit des Codes nachweisen können, müssen Sie den Wahrheitsstandard ermitteln. Dies bedeutet eine Spezifikation dessen, was der Code tun soll. Wir müssen sicher sein, dass das Ergebnis der Spezifikation entspricht. Es reicht nicht aus zu sagen, dass die Liste „sortiert“ ist: Wir wissen nicht, was wir sortieren, welche Kriterien wir verwenden und was wir mit „sortieren“ meinen. Stattdessen können Sie sagen: "Die Liste der ganzen Zahlen wird l in aufsteigender Reihenfolge für zwei beliebige Indizes i und j sortiert , wenn ja i < j, dann l[i] <= l[j]."

Die Code-Spezifikationen sind in drei Haupttypen unterteilt:

  1. Der erste ist das Schreiben von Code-unabhängigen Operatoren. Wir schreiben unsere Sortierfunktion und schreiben in eine separate Datei das Theorem „das gibt sortierte Listen zurück“. Dies ist die älteste Form der Spezifikation, aber Isabelle und ACL2 funktionieren immer noch (ML wurde speziell erfunden, um das Schreiben solcher Spezifikationen zu unterstützen).
  2. Die zweite implementiert die Spezifikation im Code in Form von Vor- und Nachbedingungen, Anweisungen und Invarianten. Der Funktion „Der Rückgabewert ist eine sortierte Liste“ kann eine Nachbedingung hinzugefügt werden. Assertion-basierte Spezifikationen wurden ursprünglich als Hoare-Logik formalisiert . Sie erschienen zum ersten Mal in der Programmiersprache Euclid in den frühen 1970er Jahren (es ist unklar, wer sie zum ersten Mal einsetzte: Euclid oder SPV , aber soweit ich weiß, wurde Euclid zuvor der Öffentlichkeit vorgestellt). Dieser Stil wird auch als Vertragsprogrammierung bezeichnet - die beliebteste Form der Verifizierung in der modernen Industrie (hier werden Verträge als Codespezifikationen verwendet).
  3. Schließlich gibt es ein Typensystem. Gemäß der Curry-Howard-Korrespondenz kann jeder mathematische Satz oder Beweis als abhängiger Typ codiert werden. Wir definieren den Typ "sortierte Listen" und deklarieren einen Typ für die Funktion [Int] -> Sorted [Int].

Auf Let's Prove Leftpad können Sie sehen, wie es aussieht. HOL4 und Isabelle sind gute Beispiele für die Spezifikationen des "unabhängigen Theorems", SPARK und Dafny - für die Spezifikationen der "verschachtelten Anweisung", und Coq und Agda sind vom "abhängigen Typ".

Bei näherer Betrachtung werden diese drei Arten der Codespezifikation mit den drei Hauptbereichen der automatischen Validierung verglichen: Tests, Verträgeund Typen. Das ist kein Zufall. Korrektheit ist ein weites Feld, und die formale Überprüfung ist eines ihrer Extreme. Wenn der Schweregrad (und der Aufwand) der Überprüfung abnimmt, erhalten wir einfachere und engere Überprüfungen, sei es eine Einschränkung des untersuchten Zustandsraums, die Verwendung schwächerer Typen oder eine erzwungene Überprüfung zur Laufzeit. Dann wird jedes Mittel zur vollständigen Spezifikation zu einem Mittel zur teilweisen Spezifikation und umgekehrt: Viele betrachten Cleanroom als eine formale Verifikationstechnik, bei der die Codeüberprüfung weit über die menschlichen Fähigkeiten hinausgeht.

Welche Angaben stimmen?


Durch die Überprüfung wird überprüft, ob der Code der Spezifikation entspricht. Es stellt sich die Frage: Woher wissen wir, dass wir die richtige Spezifikation haben? Das Finden der richtigen Spezifikation ist eines der größten Probleme bei formalen Methoden. Dies ist auch einer der Hauptgründe gegen sie. Aber Skeptiker meinen hier nicht genau das , was die Experten für formale Methoden meinen.

Wenn Außenstehende fragen: "Wie bekommen Sie die richtigen Spezifikationen?", Denken sie normalerweise über eine Validierung nachDas heißt, Spezifikationen, die nicht den Kundenanforderungen entsprechen. Wenn Sie formal nachweisen, dass Ihr Code die Liste sortiert, und der Client tatsächlich Uber für Suppen (tm) möchte, haben Sie einfach viel Zeit aufgewendet. Sie sagen, dass nur schnelle Iterationen und kurze Feedback-Zyklen Ihre Anforderungen bestätigen können.

Es ist richtig, dass die Codeüberprüfung dies nicht überprüft. Es gibt jedoch zwei Probleme mit diesem Argument. Das erste ist, dass die Phase der Anwendung formaler Methoden einfach übertragen wird, aber nicht vollständig verschwindet. Nach all diesen schnellen Iterationen haben Sie wahrscheinlich bereits eine Vorstellung davon, was der Kunde möchte. Und dann starten Sie den Bestätigungscode. Zweitens wissen wir zwar nicht genau, was der Kunde will, aber wir können davon ausgehen, dass er es definitiv nicht tutwill. Zum Beispiel auf Software, die versehentlich herunterfiel. Sie brauchen keine Sicherheitslücken. Alle sind sich einig: Schließlich sagt niemand, dass Sie die Unit-Tests während der Iterationen überspringen müssen. Stellen Sie also zumindest sicher, dass Ihr Versionskontrollsystem keine zufälligen Benutzerdaten löscht (Hinweis: Denken Sie nicht, dass ich verbittert bin oder ähnliches).

Das Problem, die richtige Spezifikation zu finden, ist grundlegender: Wir wissen oft nicht, was wir dort schreiben sollen . Wir denken an unsere Anforderungen in menschlichen, nicht in mathematischen Begriffen. Wenn ich sage: "Das Programm sollte Bäume von Vögeln unterscheiden", worum geht es dann? Ich kann es einer Person erklären, indem ich ein paar Fotos von Bäumen und Vögeln zeige, aber dies sind nur konkrete Beispiele, keine Beschreibung der Idee.. Um dies in eine formale Spezifikation zu übersetzen, müssen Sie menschliche Konzepte formalisieren, und dies ist ein ernstes Problem.

Versteh mich nicht falsch. Hier können Sie die relevanten Spezifikationen festlegen, und Experten tun dies die ganze Zeit. Das Schreiben der relevanten Spezifikationen ist jedoch eine Fähigkeit, die entwickelt und programmiert werden muss. Aus diesem Grund erklären sich viele der jüngsten Erfolge bei der Codeüberprüfung durch eine klare Zuordnung unserer Wünsche zu dem, was wir ausdrücken können. Zum Beispiel ist CompCert  ein formal verifizierter C-Compiler , dessen Spezifikation lautet: "Vermeiden Sie Kompilierungsfehler".

Das alles hat aber nichts mit Verifikation zu tun. Wenn Sie eine Spezifikation haben, müssen Sie immer noch nachweisen, dass der Code dieser entspricht.

Nachweis der Spezifikation


Das erste Tool zur Codeüberprüfung ist eine Dijkstra-ähnliche Methode, die hauptsächlich für ALGOL gedacht ist. Zum Beispiel kann ich die Richtigkeit der Sortierung anhand der folgenden Einfügemethode "beweisen":

  1. Grundlegende Option : Wenn ein Element zur leeren Liste hinzugefügt wird, ist es das einzige Element, sodass es sortiert wird.
  2. Wenn wir eine sortierte Liste mit k Elementen haben und ein Element hinzufügen, fügen wir das Element so ein, dass es nach allen kleineren Zahlen und vor allen großen Zahlen steht. Dies bedeutet, dass die Liste noch sortiert ist.
  3. Induziert man die Sortierung nach Einfügemethode, wird die gesamte Liste sortiert.

In Wirklichkeit werden die Beweise natürlich strenger aussehen, aber dies ist eine allgemeine Idee. Dijkstra und andere benutzten diesen Stil, um die Korrektheit vieler Algorithmen zu beweisen, einschließlich vieler Grundlagen der Parallelität. Dies ist auch der Stil, mit dem Knuts Worte verwandt sind : „Hüten Sie sich vor Fehlern in diesem Code; Ich habe nur bewiesen, dass es richtig ist, habe es aber nicht ausgeführt. “ Sie können den mathematischen Beweis leicht verderben, so dass niemand etwas merkt. Nach einigen Schätzungen enthalten etwa 20% der veröffentlichten mathematischen Nachweise Fehler. Bei Peter Guttmann hat einen ausgezeichneten Essay über Beweise für die Effizienz lächerlich Programm, wo Tonnen von „trusted“ Code sofort fallen , wenn sie laufen sollen.

Gleichzeitig haben wir die Methoden des automatischen Beweises mathematischer Theoreme untersucht. Das erste Programm, das den Satz beweist, wurde 1967 veröffentlicht . In den frühen 1970er Jahren begannen solche Programme, Pascal-Code zu überprüfen, und Mitte des Jahrzehnts tauchten spezielle formale Sprachen auf. Der Programmierer formuliert bestimmte Eigenschaften des Codes und erstellt dann einen prüfbaren Beweis dafür, dass der Code diese Eigenschaften aufweist. Die ersten Programme zum Beweisen von Theoremen halfen einfach, Beweise zu verifizieren, und komplexere Werkzeuge konnten Teile des Theorems unabhängig voneinander beweisen.

Was zum nächsten Problem führt.

Beweise sind schwer zu bekommen


Die Beweise sind hart und dies ist eine sehr unangenehme Arbeit. Es ist schwer, "das Programmieren zu beenden und in den Zirkus zu gehen". Überraschenderweise sind formale Beweise für Code oft strenger als Beweise, die die meisten Mathematiker schreiben! Mathematik ist eine sehr kreative Aktivität, bei der die Antwort auf den Satz nur gültig ist, wenn Sie sie zeigen. Kreativität passt nicht gut zu Formalismus und Computern.

Nehmen Sie das gleiche Beispiel mit der Sortiermethode der Beilage, bei der wir Induktion angewendet haben. Jeder Mathematiker wird sofort verstehen, was Induktion ist, wie sie im Allgemeinen funktioniert und wie sie in diesem Fall funktioniert. Aber in dem Programm, um den Satz zu beweisen, muss alles streng formalisiert werden. Das Gleiche gilt für Beweise durch Widersprüche, Beweise durch Widersprüche usw. Darüber hinaus müssen alle Annahmen formalisiert werden, auch wenn sich die meisten Mathematiker nicht mit Beweisen beschäftigen. Zum Beispiel, wasa + (b + c) = (a + b) + c. Das Programm zum Testen von Theoremen weiß a priori nicht, dass dies wahr ist. Entweder müssen Sie es beweisen (schwierig) oder es gemäß dem assoziativen Gesetz der Addition für wahr erklären (gefährlich) oder Sie müssen eine Bibliothek mit Theoremen von jemandem kaufen, der es bereits beweisen konnte (teuer). Frühe Programme zum Beweisen von Theoremen konkurrierten hinsichtlich der Anzahl der eingebetteten Beweistaktiken und der zugehörigen Theorembibliotheken. Eines der ersten weitverbreiteten SPADE-Programme präsentierte die vollständige Arithmetikbibliothek als Hauptvorteil.

Als nächstes müssen Sie den Beweis selbst erhalten. Sie können es dem Programm zuweisen oder selbst schreiben. In der Regel ist die automatische Beweisfeststellung nicht lösbar. Für extrem enge Fälle wie Aussagenlogik oder HM-Typprüfung ist es „nur“ NP-vollständig. Tatsächlich schreiben wir selbst die meisten Beweise und der Computer überprüft ihre Richtigkeit. Dies bedeutet, dass Sie gut wissen müssen:

  • Mathematik;
  • Informatik;
  • der Bereich, in dem Sie arbeiten: Compiler, Hardware usw .;
  • Nuancen Ihres Programms und Ihrer Spezialisierung;
  • Nuancen des Programms zum Beweisen von Theoremen, die Sie verwenden, was an sich eine ganze Spezialität ist.

Zu allem Überfluss stecken rechnerspezifische Inserts Sticks in die Räder. Erinnern Sie sich, ich sagte, dass es gefährlich ist, das assoziative Gesetz der Hinzufügung anzunehmen? Einige Sprachen stimmen damit nicht überein. Zum Beispiel ++ in der C INT_MAX. ((-1) + INT_MAX) + 1 - ist INT_MAX. -1 + (INT_MAX + 1)das nicht nachweisbar. Unter der Annahme einer assoziativen Addition in C ++ ist Ihr Beweis falsch und der Code wird beschädigt. Sie müssen diese Anweisung entweder vermeiden oder nachweisen, dass für Ihr bestimmtes Fragment niemals ein Überlauf vorliegt.

Sie können sagen, dass eine unbestimmte Addition ein Fehler ist, aber Sie müssen eine Sprache mit nicht zusammenhängenden ganzen Zahlen verwenden. Die meisten Sprachen haben jedoch spezifische Funktionen, die den Beweis stören. Nimm den folgenden Code:

a = true;
b = false;
f(a);
assert a;

Ist das immer so? Keine Tatsache. Vielleicht fändern a. Vielleicht ändert es den parallelen Fluss. Möglicherweise wurde ein bAlias ​​zugewiesen a, daher ändert sich auch die Änderung a(Hinweis: Aliase behindern das Schreiben von Proofs so sehr, dass John C. Reynolds eine völlig neue Trennungslogik erstellen musste, um dieses Problem zu lösen). Wenn in Ihrer Sprache etwas möglich ist, sollten Sie ausdrücklich nachweisen, dass dies hier nicht der Fall ist. Dies hilft dabei, den Code zu bereinigen. In einem anderen Fall können die Beweise zerstört werden, da die Verwendung von Rekursionen und Funktionen höherer Ordnung erzwungen wird. Das eine und das andere ist übrigens die Basis für das Schreiben guter Funktionsprogramme. Was für die Programmierung gut ist, ist schlecht für den Beweis! (Hinweis: inIn dieser Vorlesung listete Edmund Clark einige schwer zu testende Eigenschaften auf: "Gleitkommas, Zeichenfolgen, benutzerdefinierte Typen, Prozeduren, Parallelität, generische Vorlagen, Speicher, Bibliotheken ...").

Formale Verifizierer haben ein Dilemma: Je ausdrucksvoller die Sprache, desto schwieriger ist es, etwas darauf zu beweisen. Aber je weniger ausdrucksstark die Sprache ist, desto schwieriger ist es, darauf zu schreiben. Die ersten formalen Arbeitssprachen waren sehr begrenzte Untergruppen ausdrucksstärkerer Sprachen: ACL2 war eine Untergruppe von Lisp, Euklid war eine Untergruppe von Pascal usw. Und nichts, was wir bisher besprochen haben, beweist wirklich, dass es sich um echte Programme handelt Beweise zu schreiben.

Die Beweise sind schwer. Aber sie werden einfacher. Forscher auf diesem Gebiet fügen neue Heuristiken, Theorembibliotheken, vorgeprüfte Komponenten usw. hinzu. Der technische Fortschritt hilft auch: Je schneller die Computer, desto schneller die Suche.

SMT-Revolution


Eine der Neuerungen Mitte der 2000er Jahre war die Aufnahme von SMT-Lösern in Programme zur Beweisführung von Theoremen. Im weiteren Sinne kann ein SMT-Löser (einige) mathematische Theoreme in Probleme mit der Einhaltung von Beschränkungen verwandeln. Dies macht eine kreative Aufgabe zu einer rechnerischen. Möglicherweise müssen Sie noch Zwischenprobleme (Lemmas) als Schritte in einem Theorem angeben, dies ist jedoch besser, als alles selbst zu beweisen. Die ersten SMT-Löser erschienen um 2004, zunächst als akademische Projekte. Einige Jahre später veröffentlichte Microsoft Research Z3, einen gebrauchsfertigen SMT-Löser. Der große Vorteil des Z3 bestand darin, dass es viel komfortabler zu bedienen war als andere SMTs, die offen gesagt fast nichts sagten. Microsoft Research hat es intern verwendet, um die Eigenschaften des Windows-Kernels zu überprüfen

Das SMT traf die FM-Community, weil es plötzlich viele einfache Beweise trivial machte und es ermöglichte, sehr schwierige Probleme anzugehen. Auf diese Weise konnten die Menschen in ausdrucksstärkeren Sprachen arbeiten, da nun die Probleme der Ausdrucksäußerungen gelöst wurden. Unglaubliche Fortschritte sind im IronFleet- Projekt zu verzeichnen : Mit den besten SMT-Lösern und der erweiterten Verifizierungssprache konnte Microsoft in nur 3,7 Personenjahren 5000 Zeilen verifizierten Dafny-Code schreiben! Dies ist ein unglaublich hohes Tempo: so viele wie vier Punkt - Linie in den Tag (Hinweis: Der bisherige Rekord gehörte SEL4 , Entwickler , die auf geschrieben haben zwei Linien in den Tag zu C .

Der Beweis ist schwierig.

Warum brauchst du das?


Es ist Zeit, einen Schritt zurückzutreten und zu fragen: "Was ist der Sinn?" Wir versuchen zu beweisen, dass ein Programm eine bestimmte Spezifikation erfüllt. Richtigkeit ist ein Bereich. Es gibt zwei Teile der Überprüfung: Wie objektiv Ihr Programm "korrekt" ist und wie gründlich Sie die Richtigkeit überprüft haben. Je mehr verifiziert, desto besser, aber das Überprüfen kostet Zeit und Geld. Wenn wir mehrere Einschränkungen haben (Leistung, Time-to-Market, Kosten usw.), ist eine vollständige Validierungsprüfung nicht unbedingt die beste Option. Dann stellt sich die Frage, was ist der minimale Scheck, den wir brauchen und was er kostet. In den meisten Fällen benötigen Sie beispielsweise eine Richtigkeit von 90% oder 95% oder 99%. Vielleicht sollten Sie Zeit damit verbringen, die Benutzeroberfläche zu verbessern, anstatt die verbleibenden 1% zu überprüfen?

Dann die Frage: "Ist die Verifizierung 90/95/99% deutlich billiger als 100%?" Die Antwort lautet "Ja". Es ist recht angenehm zu sagen, dass die Codebasis, die wir gut getestet und getippt haben, bis auf einige Korrekturen in der Produktion im Grunde genommen korrekt ist und wir sogar mehr als vier Codezeilen pro Tag schreiben. Tatsächlich hätte die überwiegende Mehrheit der Fehler beim Betrieb verteilter Systeme durch ein etwas vollständigeres Testen verhindert werden können. Und dies ist nur eine Erweiterung der Tests, ganz zu schweigen von Fuzzing-, Eigenschafts- oder Modelltests. Mit diesen einfachen Tricks können Sie ein wirklich hervorragendes Ergebnis erzielen, ohne dass Sie einen vollständigen Beweis benötigen.

Was ist, wenn die Eingabe und die Tests keine ausreichende Bestätigung liefern? Es ist immer noch viel einfacher, von 90% auf 99% zu wechseln als von 99% auf 100%. Wie bereits erwähnt, handelt es sich bei Cleanroom um eine Entwicklerpraxis, die eine umfassende Dokumentation, eine gründliche Ablaufanalyse und eine umfassende Codeüberprüfung umfasst. Keine Beweise, keine formelle Überprüfung, nicht einmal Unit-Tests. Ein ordnungsgemäß organisierter Reinraum reduziert die Fehlerdichte jedoch auf weniger als 1 Fehler pro 1000 Codezeilen in der Produktion (Anmerkung: Zahlen aus Stevelys Forschungen zur Null- Fehler -Programmierung). Seien Sie jedoch immer skeptisch und überprüfen Sie die Originalquellen). Die Programmierung von Cleanroom verlangsamt die Entwicklung nicht und geht mit Sicherheit schneller als 4 Zeilen pro Tag. Und Cleanroom selbst ist nur eine von vielen Methoden zur Entwicklung hochzuverlässiger Software, die zwischen normaler Entwicklung und Codeüberprüfung liegt. Sie brauchen keine vollständige Überprüfung, um eine gute oder sogar nahezu perfekte Software zu schreiben. Es gibt Fälle, in denen dies erforderlich ist, aber für die meisten Branchen ist dies eine Verschwendung von Geld.

Dies bedeutet jedoch nicht, dass formale Methoden in der Regel unwirtschaftlich sind. Viele der oben genannten hochzuverlässigen Methoden basieren auf dem Schreiben von Codespezifikationen, die Sie nicht offiziell nachweisen. In Bezug auf die Verifizierung gibt es in der Branche zwei allgemeine Möglichkeiten, um davon zu profitieren. Zuerst die Designüberprüfung anstelle von Code, auf die wir später noch eingehen werden. Zweitens eine teilweise Überprüfung des Codes, die wir jetzt betrachten werden.

Teilweise Codeüberprüfung


Für alltägliche Aufgaben ist es zu teuer, einen vollständigen Scan durchzuführen. Wie wäre es teilweise? Schließlich können Sie vom Nachweis einiger Eigenschaften einzelner Codefragmente profitieren. Anstatt zu beweisen, dass meine Funktion Zahlen immer richtig sortiert, kann ich zumindest beweisen, dass sie nicht für immer wiederholt und niemals außerhalb des Bereichs liegt. Dies ist auch eine sehr nützliche Information. Selbst der einfachste Beweis für C-Programme ist eine großartige Möglichkeit , einen großen Teil des unbestimmten Verhaltens zu eliminieren .

In dem Problem der Verfügbarkeit. Die meisten Sprachen dienen entweder der vollständigen Überprüfung oder werden überhaupt nicht unterstützt. Im ersten Fall fehlen Ihnen viele gute Funktionen für ausdrucksstärkere Sprachen, und im zweiten Fall müssen Sie die Dinge in einer Sprache beweisen, die dem Konzept selbst feindlich gegenübersteht. Aus diesem Grund konzentrieren sich die meisten Teilprüfungsstudien auf mehrere Sprachen mit hoher Priorität wie C und Java. Viele arbeiten mit begrenzten Teilmengen von Sprachen. Beispielsweise ist SPARK eine begrenzte Teilmenge von Ada, sodass Sie kritischen SPARK-Code schreiben und mit weniger kritischem Ada-Code interagieren können. Aber die meisten dieser Sprachen sind ziemlich Nischen.

Häufiger sind bestimmte Arten der Verifikation in die Grundstruktur von Sprachen eingebettet. Typisierungssysteme, die in der Produktion verwendet werden, sind weit verbreitet: Sie wissen möglicherweise nicht, dass der Schwanz immer den Schwanz zurückgibt, aber Sie wissen genau, um welchen Typ es sich handelt [a] -> [a]. Es gibt auch Beispiele wie Rust mit nachgewiesener Speichersicherheit und Pony mit Sicherheitsnachweis für Ausnahmen. Sie unterscheiden sich geringfügig von SPARK und Frama-C darin, dass sie nur Teilprüfungen durchführen können. Und sie werden in der Regel von Experten für Programmiersprachen und nicht von Experten für formale Methoden entwickelt: Beide Disziplinen haben vieles gemeinsam, sind jedoch nicht identisch. Vielleicht sind Sprachen wie Rust und Haskell deshalb wirklich praxisgerecht.

Design-Spezifikation


Bisher haben wir nur über die Codeüberprüfung gesprochen. Formale Methoden haben jedoch eine andere Seite, die abstrakter ist und das Design selbst verifiziert, die Projektarchitektur. Dies ist eine so gründliche Analyse, dass sie gleichbedeutend mit einer formalen Spezifikation ist : Wenn jemand sagt, dass er eine formale Spezifikation erfüllt, bedeutet dies höchstwahrscheinlich, dass er das Design definiert und überprüft.

Wie wir gesagt haben, ist es sehr, sehr schwierig, alle Zeilen des Codes zu beweisen. Viele Probleme in der Produktion entstehen aber nicht durch den Code, sondern durch das Zusammenspiel der Systemkomponenten. Wenn wir beispielsweise Implementierungsdetails verwerfen, bei denen vorausgesetzt wird, dass das System Vögel erkennen kann, können wir leichter analysieren, wie Bäume und Vögel als übergeordnete Module in das Gesamtdesign passen. In einem solchen Maßstab wird es viel einfacher, Dinge zu beschreiben, die Sie nicht implementieren können, beispielsweise eine Laufzeitumgebung, menschliche Interaktionen oder einen unbarmherzigen Zeitfluss . Auf dieser Skala formalisieren wir unsere Absichten mit einem gemeinsamen System, nicht mit Codezeilen. Dies ist viel näher an der menschlichen Ebene, wo Projekte und Anforderungen viel mehrdeutiger sein können als auf Codeebene.

Nehmen wir zum Beispiel eine Prozedur mit einer groben Spezifikation: "Wenn sie aufgerufen wird, wird ein Systemaufruf ausgeführt, um Daten im Repository zu speichern und Systemfehler zu behandeln." Die Eigenschaften sind schwer zu überprüfen, aber es ist ziemlich klar, wie dies zu tun ist. Sind die Daten korrekt serialisiert? Werden unsere Garantien aufgrund falscher Eingaben verletzt? Behandeln wir alle möglichen Möglichkeiten, um den Systemaufruf fehlzuschlagen? Vergleichen Sie nun das Protokollierungssystem auf hoher Ebene mit der Spezifikation "Alle Nachrichten werden protokolliert" und beantworten Sie die folgenden Fragen:

  • Werden alle Nachrichten oder alle Nachrichten , die in das System eingehen, aufgezeichnet ? Nachrichten werden einmal aufgezeichnet oder einmal garantiert ?
  • Wie werden die Nachrichten gesendet? Ist es eine Wende? Liefert der Kanal sie nur einmal? Ist alles in Ordnung mit der Lieferung?
  • Meinen wir mit Protokollierung für immer schreiben? Kann ich eine Nachricht in das Protokoll aufnehmen und von dort aus löschen? Kann es zwischen dem aufgenommenen und dem nicht aufgenommenen Zustand „rumhängen“, bevor es dauerhaft aufgenommen wird?
  • Was kann ich tun, wenn der Server während der Aufzeichnung einer Nachricht explodiert? Ist ein Journal notwendig?
  • Gibt es wichtige Medieneigenschaften? Übersteigt die Tatsache, dass der Spediteur Daten verloren hat, unsere Anforderungen oder nicht?
  • Was ist mit der DSGVO?
  • und so weiter und so fort.

Ohne formale Gestaltung ist es schwieriger, die wirklich notwendigen Anforderungen an das System auszudrücken. Wenn Sie sie nicht ausdrücken können, haben Sie keine Ahnung, ob das Design den Anforderungen wirklich entspricht oder nur so aussieht, aber zu unvorhersehbaren Konsequenzen führen kann. Indem wir unsere Absichten und unser Design formeller ausdrücken, können wir leicht überprüfen, ob wir tatsächlich das entwickeln, was wir brauchen.

So wie wir Programmiersprachen zur Darstellung von Code verwenden, verwenden wir auch Spezifikationssprachen zur Darstellung von Projekten. Spezifikationssprachen konzentrieren sich normalerweise auf Designspezifikationen und nicht auf Codespezifikationen, obwohl einige Sprachen in beiden Fällen verwendet werden können (Anmerkung: Der Prozess des Abgleichs von Designspezifikationen mit Codespezifikationen wird als Verfeinerung bezeichnetIn Zukunft werde ich die Spezifikationssprachen als Designsprachen (DL) bezeichnen, um Verwirrung zu vermeiden (auch dies ist keine gebräuchliche Terminologie; die meisten Leute verwenden die "Spezifikationssprache", aber ich möchte klar zwischen Codespezifikationen und Designspezifikationen unterscheiden).

Der wahrscheinlich erste komplette DL war der VDM um 1972. Seitdem haben wir eine Vielzahl unterschiedlicher Sprachspezifikationen gesehen. Der DL-Bereich ist viel vielfältiger und fragmentierter als bei Code Verification Languages ​​(CVL). Grob gesagt haben die Leute DL als Mittel zum Erreichen eines Ziels und CVL als Ziel selbst erfunden. Da sie stark von spezifischen Problembereichen beeinflusst werden, werden alle möglichen Ideen und Semantiken in DL implementiert. Hier ist ein sehr kurzer Überblick über einige der ersten DLs:

Sprache Modellierungsbereich Abhilfe schaffen
Z Geschäftsanforderungen relationale Algebra
Promela nachrichten CSP
SDL Telekommunikation Flussdiagramme
Harel-Zustandsdiagramme Steuerungen Automaten
Entscheidungstabellen lösungen Tabellen

Da DLs in der Regel zur Lösung spezifischer Probleme erstellt werden, verfügen die meisten von ihnen über mindestens zwei oder drei echte Anwendungen. Die Ergebnisse sind in der Regel sehr positiv. Praktizierende sagen, dass DL Einblick in die Probleme gibt und das Finden von Lösungen erleichtert. Der Hauptchampion war lange Zeit Praxis (jetzt Altran), die "Fixes-by-Design" - eine  Kombination aus Z-Designs und SPARK-Code - verwendete, um kritische Sicherheitssysteme zu erstellen. Spezifikationen sparen Zeit und Geld, da Sie zu einem späteren Zeitpunkt des Projekts keine Konstruktionsfehler finden.

Pamela Zave experimentierte mit Alloy und entdeckte einen grundlegenden Fehler in Chord, einer der wichtigsten verteilten Hash-Tabellen. AWS fing an, 35-Schritte-Fehler zu findendurch Schreiben einer TLA + -Spezifikation. Wenn Leute versuchen, Spezifikationen zu schreiben, werden sie meiner Erfahrung nach sehr bald große Fans dieses Geschäfts.

Aber Fans formaler Methoden und Außenstehende beurteilen den Wert des Schreibens von Spezifikationen ganz anders. Für Fans ist der größte Vorteil, dass Sie durch den Designprozess selbst verstehen, was Sie schreiben. Wenn Sie formell ausdrücken müssen, was Ihr System tut, werden eine Vielzahl von impliziten Fehlern plötzlich schmerzhaft offensichtlich. Außenstehende können das überhaupt nicht verstehen. Wenn Sie jemanden mit dem DL versuchen möchten, muss die Person eine Möglichkeit haben, zu überprüfen, ob der Entwurf wirklich die gewünschten Eigenschaften aufweist.

Glücklicherweise ist dies auch für viele Qualifikanten äußerst wichtig, sodass die Designüberprüfung ein großes Forschungsgebiet darstellt.

Modellprüfung


Wie beim Code können wir das Design überprüfen, indem wir Sätze schreiben. Zum Glück haben wir einen weiteren Trick: Sie können den Model Checker (Model Checker) verwenden. Anstatt zu beweisen, dass das Design korrekt ist, erzwingen wir einfach den Raum möglicher Zustände und prüfen, ob ein falscher Zustand darin enthalten ist. Wenn wir nichts finden, ist alles in Ordnung (Hinweis: Modellüberprüfungsprogramme werden auch zum Überprüfen von Code verwendet, wie JMBC, aber die Modellüberprüfung wird bei der Entwurfsüberprüfung viel häufiger verwendet als die Modellüberprüfung).

Die Überprüfung von Modellen bietet viele Vorteile. Erstens müssen Sie keine Beweise schreiben, die viel Zeit und Mühe sparen. Zweitens müssen Sie nicht lernenschreiben Beweise, so dass die Eintrittsbarriere viel niedriger ist. Drittens liefert die Überprüfung des Modells ein explizites Gegenbeispiel, wenn das Design beschädigt ist. Es ist sehr viel einfacher, den Fehler zu korrigieren, insbesondere wenn Sie 35 Schritte benötigen, um ihn abzuspielen. Versuchen Sie es selbst zu finden.

Es gibt ein paar Nachteile. Erstens sind diese Tools nicht so leistungsfähig. Insbesondere können Sie auf eine Unendlichkeit stoßen(unbegrenztes) Modell, das unendlich viele verschiedene Zustände hat. Beispielsweise definieren Sie einen Nachrichtenwarteschlangen-Handler: Er funktioniert normalerweise mit einer Liste von zehn Nachrichten. Aber wenn Sie es auf einer Liste glauben müssen ... nun, es gibt eine unendliche Anzahl von ihnen, also gibt es eine unendliche Anzahl von Zuständen im Modell. Die meisten Modellvalidierungswerkzeuge haben unterschiedliche Techniken für solche Situationen, z. B. das Bestimmen von Äquivalenzklassen oder Symmetrien, aber jeder Fall ist anders.

Ein weiterer großer Nachteil - die Explosion im Raum der Zustände (Zustandsraumexplosion). Stellen Sie sich vor, Sie haben drei Prozesse, von denen jeder aus vier aufeinanderfolgenden Schritten besteht und die sich in beliebiger Weise abwechseln können. Wenn sie sich nicht gegenseitig beeinflussen, stellt sich heraus(4*3)! / (4!)^3 = 34 650mögliche Leistungen (Verhaltensweisen). Wenn jeder Prozess einen der fünf Anfangszustände aufweist, erhöht sich die Gesamtzahl der Verhalten auf 4.300.000. Bei der Überprüfung der Modelle muss sichergestellt werden, dass sich alle gut verhalten. Und vorausgesetzt, dass sie nicht miteinander interagieren! Wenn sie dies tun, wächst der Zustandsraum noch schneller. Die kombinatorische Explosion wird als das Hauptproblem bei der Modellprüfung angesehen, und es muss viel Arbeit geleistet werden, um dieses Problem zu lösen.

Gleichzeitig gibt es aber auch eine andere Möglichkeit, mit der Explosion des Staatenraums umzugehen: Wirf mehr Ausrüstung darauf. Das größte Problem bei der Überprüfung des Modells ist „nur“ das Leistungsproblem, und wir lösen die Leistungsprobleme sehr gut. Die meisten (aber nicht alle) Modellprüfungen lassen sich problemlos parallelisieren. Nachdem Sie das Modell optimiert und mit kleinen Parametern getestet haben, können Sie einen AWS-Cluster bereitstellen und mit großen Parametern ausführen.

In der Praxis verwenden viele Qualifizierer die Modellprüfung und gehen dann bei Bedarf zu Programmen, um Theoreme zu beweisen (Hinweis: Beachten Sie, dass „viele Spezifizierer“ etwa zehn Personen umfassen). Noch mehr Spezialisten für die Erstellung von Spezifikationen beginnen, Modelle zu überprüfen, und wenn sie an ihre Grenzen stoßen, wechseln sie zu weniger intensiven Überprüfungsformen.

Problem mit den Designspezifikationen


Daher ist die Designüberprüfung einfacher und schneller als die Codeüberprüfung und hat viele beeindruckende Erfolge gezeigt. Warum benutzen die Leute es nicht? Das Problem mit DV ist viel heimtückischer. Die Codeüberprüfung ist ein technisches Problem, und die Designüberprüfung ist ein soziales Problem: Die Leute verstehen den Punkt einfach nicht.

Dies liegt hauptsächlich an der Tatsache, dass Design kein Code ist . In den meisten DLs gibt es keine automatische Möglichkeit, Code zu generieren, und es gibt keine Möglichkeit, vorhandenen Code zu übernehmen und auf Design zu überprüfen (Hinweis: Die Codegenerierung aus Spezifikationen wird als Synthese bezeichnet ; zur Orientierung siehe die Arbeit von Nadya Polykarpova ; Nachweis, dass der Code der Spezifikation entspricht (oder eine andere Spezifikation) heißtKlarstellung : In beiden Richtungen wird aktiv geforscht).

Programmierer neigen dazu, Software-Artefakten nicht zu vertrauen, die keinen Code enthalten oder nicht zwangsweise mit dem Code synchronisiert sind. Aus dem gleichen Grund werden häufig Dokumentationen, Kommentare, Diagramme, Wikis und Commits ignoriert.

Es scheint, dass Programmierer einfach nicht glauben, dass die Spezifikationen irgendeinen Nutzen bringen. Nach meiner Erfahrung gehen sie davon aus, dass aktuelle Tools (Pseudocode, Diagramme, TDD) mehr als genug für ein korrektes Design sind. Ich weiß nicht, wie verbreitet diese Meinung ist, und ich kann sie nur mit Ausnahme des allgemeinen Konservatismus erklären.

Aber es gibt genau solche Beschwerden in jeder Community der mir bekannten Methodik: TDD-Unterstützer beschweren sich, dass Programmierer TDD nicht ausprobieren wollen, Haskell-Fans beschweren sich, dass Programmierer nicht an statisches Tippen denken und so weiter.

Ich habe das Argument gehört, dass Agile kein vorgefertigtes Design akzeptiert, sodass niemand eine formale Spezifikation machen möchte. Kann sein. Aber viele von denen, die ich getroffen habe, lehnen sowohl Agile als auch FM ab. Ein weiteres Argument ist, dass historisch formale Methoden ständig neu bewertet werden und das Versprechen nicht erfüllten. Es ist auch möglich, aber die meisten Menschen nicht einmal gehört haben , die formalen Methoden und noch mehr über ihre Geschichte.

Es ist nur sehr schwierig, die Leute dazu zu bringen, sich Sorgen zu machen, was sie nicht tun, selbst wenn sie die Vorteile erkennen.

Zusammenfassung


Die Codeüberprüfung ist eine schwierige Aufgabe. Immer mehr Menschen beteiligen sich daran, obwohl theorembeweisende Programme und SMT-Löser immer komplexer werden. Aber noch in absehbarer Zeit wird es wahrscheinlich eine Menge Spezialisten bleiben.

Die Designüberprüfung ist viel einfacher, erfordert jedoch die Überwindung der kulturellen Barrieren. Ich denke, die Situation kann geändert werden. Vor zwanzig Jahren waren automatisierte Tests und Codeüberprüfungen eher exotische und Nischenthemen, wurden aber schließlich zum Mainstream. Auch hier war und ist die Vertragsprogrammierung eine Nische.

Ich hoffe, dieser Artikel erklärt ein bisschen besser, warum formale Methoden so selten verwendet werden. Zumindest ist dies eine bessere Erklärung als das übliche Argument „Web ist kein Flugzeug“. Schreien Sie, wenn Sie offensichtliche Fehler bemerken.