Beim Software Engineering Stack Exchange sah ich die 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 "Eine Seite ist kein Flugzeug !!!" In gewisser Weise ist dies wahr, aber es erklärt nicht viel. Ich habe diesen Artikel geschrieben, um ein umfassenderes historisches Bild der formalen Methoden (FM) zu vermitteln, warum sie nicht tatsächlich 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. Grundsätzlich gibt es zwei Gruppen formaler Methoden: Die formale Spezifikation untersucht das Schreiben präziser, eindeutiger Spezifikationen und die formale Verifikation untersucht die Beweismethoden. Dies umfasst sowohl Code- als auch abstrakte Systeme. Wir verwenden nicht nur unterschiedliche Begriffe für Code und Systeme, sondern verwenden häufig unterschiedliche Tools, um sie zu überprüfen. Um die Sache noch verwirrender zu machen: Wenn jemand sagt, dass er eine formale Spezifikation erstellt, bedeutet dies normalerweise eine Entwurfsüberprüfung. Und wenn jemand sagt, dass er eine formale Überprüfung durchführt, bezieht sich dies normalerweise auf die Codeüberprüfung.

Aus Gründen der Übersichtlichkeit teilen wir die Codeverifizierungsüberprüfung (CV) und die Entwurfsüberprüfung (DV) auf und unterteilen die Spezifikationen auf ähnliche Weise in 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 Beweisen der Behauptungen sein, dass das System niemals abstürzt und das falsche Passwort nicht akzeptiert, oder dass das System niemals abstürzt und das Konto sperrt, 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 identifizieren implizit hochzuverlässige Programme wie medizinische Geräte und Flugzeuge. Die Menschen gehen davon aus, dass formale Methoden für sie weit verbreitet sind, für den Rest jedoch nicht. Dies ist zu optimistisch : Die meisten hochzuverlässigen Programme verwenden keine formalen Methoden. Stattdessen konzentrieren wir uns auf „normale“ Software.

Zum Schluss der Haftungsausschluss: Ich bin kein professioneller Historiker, und obwohl ich versucht habe, die Informationen sorgfältig zu überprüfen, kann der Artikel Fehler enthalten. Darüber hinaus bin ich auf formale Spezifikationen (DS und DV) spezialisiert, sodass bei Fehlern über die Codeüberprüfung mehr Fehler auftreten können. Wenn Sie sehen, schreiben Sie mir, ich werde das Problem beheben (und noch etwas: Ich verdiene Geld mit Seminaren zu TLA + und Alloy, daher bin ich sehr voreingenommen gegenüber diesen Sprachen; ich versuche so objektiv wie möglich zu sein, aber Sie verstehen: Voreingenommenheit ist Voreingenommenheit).

Formale Programmierung

Spezifikation erhalten

Bevor Sie die Richtigkeit des Codes nachweisen können, müssen Sie den Standard der Wahrheit 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 unter "Sortieren" verstehen. Stattdessen können wir sagen: "Die Liste der ganzen Zahlen l in aufsteigender Reihenfolge für zwei beliebige Indizes i und j sortiert. Wenn i < j , dann ist l[i] <= l[j] ."

Die Codespezifikationen sind in drei Haupttypen unterteilt:

Die erste besteht darin, codeunabhängige Anweisungen zu schreiben. Wir schreiben unsere Sortierfunktion und schreiben in eine separate Datei den Satz „Dies gibt sortierte Listen zurück“. Dies ist die älteste Form der Spezifikation, aber Isabelle und ACL2 funktionieren immer noch auf diese Weise (ML wurde speziell erfunden, um solche Spezifikationen zu schreiben).
Die zweite implementiert Spezifikationen im Code in Form von Vor- und Nachbedingungen, Anweisungen und Invarianten. Sie können der Funktion "Der Rückgabewert ist eine sortierte Liste" eine Nachbedingung hinzufügen. Anspruchsbasierte Spezifikationen wurden ursprünglich als Hoars Logik formalisiert. Sie erschienen zum ersten Mal in der Programmiersprache Euclid in den frühen 1970er Jahren (es ist nicht klar, wer sie zuerst verwendet hat: Euclid oder SPV , aber soweit ich weiß, wurde Euclid zuvor der Öffentlichkeit vorgestellt). Dieser Stil wird auch als Vertragsprogrammierung bezeichnet - die beliebteste Form der Überprüfung in der modernen Industrie (hier werden Verträge als Code-Spezifikationen verwendet).
Schließlich gibt es Typsysteme. Durch Curry-Howard-Korrespondenz kann jeder mathematische Satz oder Beweis als abhängiger Typ codiert werden. Wir definieren den Typ der sortierten Listen und deklarieren den Typ [Int] -> Sorted [Int] für die Funktion.

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 sind die Spezifikationen der „verschachtelten Anweisung“ und Coq und Agda sind der „abhängige Typ“.

Wenn Sie genau hinschauen, werden diese drei Formen der Codespezifikation mit den drei Hauptbereichen der automatischen Validierung verglichen: Tests, Verträge und Typen. Dies ist kein Zufall. Korrektheit ist ein weites Feld, und die formale Überprüfung ist eines ihrer Extreme. Wenn die Genauigkeit (und der Aufwand) der Überprüfung abnimmt, erhalten wir einfachere und engere Überprüfungen, unabhängig davon, ob der zu untersuchende Zustandsraum begrenzt, schwächere Typen verwendet oder zur Laufzeit erzwungen werden. Dann wird jedes Mittel zur vollständigen Spezifikation zu einem Mittel zur teilweisen Spezifikation und umgekehrt: Viele betrachten Cleanroom als eine Technik der formalen Verifikation, bei der eine Codeüberprüfung weit über die menschlichen Fähigkeiten hinausgeht.

Welche Angaben sind richtig?

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 eine der wichtigsten Einwände gegen sie. Aber Skeptiker meinen hier nicht genau das , was formale Spezialisten im Sinn haben.

Wenn Außenstehende fragen: "Wie erhalten Sie die richtigen Spezifikationen?", Denken sie normalerweise an die Validierung , dh an Spezifikationen, die nicht den Anforderungen des Kunden entsprechen. Wenn Sie offiziell beweisen, dass Ihr Code die Liste sortiert und der Kunde Uber tatsächlich für Suppen (tm) möchte, haben Sie nur eine Menge Zeit aufgewendet. Nur schnelle Iterationen und kurze Rückkopplungsschleifen können Ihre Anforderungen bestätigen.

Es ist wahr, dass die Codeüberprüfung sie nicht validiert. Bei diesem Argument gibt es jedoch zwei Probleme. Das erste ist, dass die Phase der Anwendung formaler Methoden einfach verschoben wird, aber nicht vollständig verschwindet. Nach all diesen schnellen Iterationen haben Sie wahrscheinlich bereits eine Vorstellung davon, was der Client will. Und dann beginnen Sie mit der Codeüberprüfung. Zweitens können wir, obwohl wir nicht genau wissen, was der Kunde will, davon ausgehen, was er definitiv nicht will. Zum Beispiel, um versehentlich Software zum Absturz zu bringen. Sie brauchen keine Sicherheitslücken. Alle sind damit einverstanden: Am Ende sagt niemand, dass Sie 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 so etwas).

Das Problem beim Finden der richtigen Spezifikation ist grundlegender: Wir wissen oft nicht, was wir dort schreiben sollen . Wir denken über unsere Anforderungen in menschlichen, nicht mathematischen Begriffen nach. 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 Bilder von Bäumen und Vögeln zeige, aber dies sind nur konkrete Beispiele, keine Beschreibung der Idee . In der Tat ist es notwendig, menschliche Konzepte zu formalisieren, um dies in eine formale Spezifikation umzusetzen, und dies ist ein ernstes Problem.

Versteh mich nicht falsch. Hier können die relevanten Spezifikationen definiert werden, und Experten tun dies ständig. Das Schreiben der entsprechenden Spezifikationen ist jedoch eine Fähigkeit, die entwickelt werden muss, sowie Programmierkenntnisse. Aus diesem Grund erklären sich viele der jüngsten Erfolge der Codeüberprüfung durch eine klare Zuordnung dessen, was wir wollen, zu dem, was wir ausdrücken können. Beispielsweise ist CompCert ein formal verifizierter C-Compiler. Die Spezifikation dafür lautet: „Kompilierungsfehler vermeiden“.

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

Spezifikationsnachweis

Das erste Tool zur Codeüberprüfung ist die Dijkstra-Methode „Überlegen Sie, warum dies wahr ist“, die hauptsächlich für ALGOL gilt. Zum Beispiel kann ich die Richtigkeit der Sortierung mit der Einfügemethode wie folgt „beweisen“:

Die grundlegende Option : Wenn Sie der leeren Liste ein Element hinzufügen, ist dies das einzige Element, sodass es sortiert wird.
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 größeren Zahlen steht. Dies bedeutet, dass die Liste noch sortiert ist.
Durch Induktion sortiert die Einfügesortierung die gesamte Liste.

In Wirklichkeit wird der Beweis natürlich strenger aussehen, aber dies ist eine allgemeine Idee. Dijkstra und andere verwendeten diesen Stil, um die Richtigkeit vieler Algorithmen zu beweisen, einschließlich vieler Grundlagen der Parallelität. Dies ist auch der Stil, mit dem Knuths Worte verbunden sind: „Vorsicht vor Fehlern in diesem Code; Ich habe nur bewiesen, dass es richtig ist, aber ich habe es nicht gestartet. " Sie können einen mathematischen Beweis leicht ruinieren, so dass niemand es bemerkt. Nach einigen Schätzungen enthalten ungefähr 20% der veröffentlichten mathematischen Beweise Fehler. Peter Guttmann hat einen ausgezeichneten Aufsatz über die Gesundheit eines lächerlichen Programms, in dem Tonnen von "getestetem" Code sofort fallen, wenn Sie sie ausführen.

Gleichzeitig untersuchten wir Möglichkeiten, um mathematische Theoreme automatisch zu beweisen. Das erste Programm, das die Theoreme beweist, wurde 1967 veröffentlicht . In den frühen 1970er Jahren wurden solche Programme zum Testen von Pascal-Code verwendet, und Mitte des Jahrzehnts erschienen spezielle formale Sprachen. Der Programmierer formuliert einige Eigenschaften des Codes und erstellt dann einen überprüfbaren Beweis dafür, dass der Code diese Eigenschaften aufweist. Die ersten Programme zum Beweisen von Theoremen halfen den Menschen lediglich, die Beweise zu verifizieren, während ausgefeiltere Werkzeuge Teile des Theorems unabhängig voneinander beweisen konnten.

Was zu folgendem Problem führt.

Beweise sind schwer zu bekommen

Beweise sind schwierig und es ist ein sehr böser Job. Es ist schwer, die Programmierung zu beenden und in den Zirkus zu gehen. Überraschenderweise sind formale Code-Beweise oft strenger als die von den meisten Mathematikern geschriebenen Beweise! 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 schlecht zu Formalismus und Computern.

Nehmen Sie das gleiche Beispiel für die Sortierung von Einfügungen, bei dem wir die Induktion angewendet haben. Jeder Mathematiker wird sofort verstehen, was Induktion ist, wie sie im Allgemeinen funktioniert und wie sie in diesem Fall funktioniert. Aber im Programm zum Beweis der Theoreme muss alles streng formalisiert werden. Gleiches gilt für Beweise durch Widerspruch, Beweise durch Gegenposition usw. Darüber hinaus müssen alle Annahmen formalisiert werden, auch diejenigen, bei denen sich die meisten Mathematiker nicht um Beweise kümmern. Zum Beispiel ist a + (b + c) = (a + b) + c . Das Programm zur Überprüfung von Theoremen a priori weiß nicht, dass dies wahr ist. Sie müssen es entweder beweisen (schwer) oder es gemäß dem assoziativen Additionsgesetz (gefährlich) als wahr erklären oder eine Bibliothek von Theoremen von jemandem kaufen, der es bereits beweisen konnte (teuer). Frühe Theoremprüfprogramme konkurrierten um die Anzahl der eingebauten Proof-Taktiken und der zugehörigen Theorembibliotheken. Eines der ersten weit verbreiteten SPADE-Programme präsentierte die komplette Arithmetikbibliothek als Hauptvorteil.

Als nächstes müssen Sie den Beweis selbst erhalten. Sie können dies dem Programm anvertrauen oder selbst schreiben. Normalerweise ist die automatische Definition von Beweismitteln nicht entscheidbar. Für extrem enge Fälle wie Aussagenlogik oder Typprüfung HM 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:

Mathe
Informatik;
der Bereich, in dem Sie arbeiten: Compiler, Hardware usw.;
die Nuancen Ihres Programms und Ihrer Spezialisierung;
die Nuancen des Programms, um die von Ihnen verwendeten Theoreme zu beweisen, was an sich eine ganze Spezialität ist.

Schlimmer noch, computer-spezifische Sticks in Rädern. Erinnern Sie sich, ich sagte, es sei gefährlich, ein assoziatives Additionsgesetz anzunehmen? Einige Sprachen erfüllen diese nicht. Zum Beispiel in C ++ INT_MAX. ((-1) + INT_MAX) + 1 INT_MAX. ((-1) + INT_MAX) + 1 ist INT_MAX. -1 + (INT_MAX + 1) INT_MAX. -1 + (INT_MAX + 1) , was nicht nachweisbar ist. Unter der Annahme einer assoziativen Hinzufügung in C ++ ist Ihr Beweis falsch und der Code wird beschädigt. Sie müssen diese Aussage entweder vermeiden oder nachweisen, dass für Ihr bestimmtes Fragment niemals ein Überlauf auftritt.

Sie können sagen, dass eine unbestimmte Addition ein Fehler ist, aber Sie müssen eine Sprache mit nicht verwandten Ganzzahlen verwenden. Die meisten Sprachen haben jedoch spezifische Merkmale, die die Evidenz beeinträchtigen. Nehmen Sie den folgenden Code:

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

Ist das immer so? Keine Tatsache. Vielleicht ändert f a . Vielleicht ändert es den parallelen Fluss. Vielleicht wurde b ein Alias a zugewiesen, so dass a Änderung auch a ändert (Hinweis: Aliase behindern das Schreiben von Beweisen so sehr, dass John C. Reynolds eine völlig neue Trennungslogik erstellen musste, um dieses Problem zu lösen). Wenn so etwas in Ihrer Sprache möglich ist, sollten Sie klar beweisen, dass dies hier nicht der Fall ist. Sauberer Code hilft hier, in einem anderen Fall kann er den Beweis zerstören, da Sie gezwungen sind, Rekursionen und Funktionen höherer Ordnung zu verwenden. Beide sind übrigens die Basis für das Schreiben guter Funktionsprogramme. Was für die Programmierung gut ist, ist für den Beweis schlecht! (Hinweis: In dieser Vorlesung listete Edmund Clark einige Eigenschaften auf, die schwer zu überprüfen sind: „Gleitkommawerte, Zeichenfolgen, benutzerdefinierte Typen, Prozeduren, Parallelität, universelle Vorlagen, Speicher, Bibliotheken ...“).

Formale Verifizierer haben ein Dilemma: Je ausdrucksvoller die Sprache ist, desto schwieriger ist es, etwas zu beweisen. Aber je weniger ausdrucksstark die Sprache ist, desto schwieriger ist es, darauf zu schreiben. Die ersten formalen Arbeitssprachen waren sehr begrenzte Teilmengen ausdrucksstärkerer Sprachen: ACL2 war eine Teilmenge von Lisp, Euklid war eine Teilmenge von Pascal usw. Und nichts von dem, was wir bisher besprochen haben, beweist tatsächlich echte Programme, dies sind nur Versuche, sich zu nähern Beweise zu schreiben.

Die Beweise sind schwierig. Aber es wird einfacher. Forscher auf diesem Gebiet fügen neue Heuristiken, Theorembibliotheken, vorab getestete Komponenten usw. hinzu. Der technische Fortschritt hilft auch: Je schneller Computer, desto schneller die Suche.

SMT Revolution

Eine der Neuerungen Mitte der 2000er Jahre war die Einbeziehung von SMT-Lösern in Programme zum Nachweis von Theoremen. Im Allgemeinen kann ein SMT-Löser (einige) mathematische Theoreme in Probleme bei der Einhaltung von Beschränkungen umwandeln. Dies verwandelt eine kreative Aufgabe in eine rechnerische. Möglicherweise müssen Sie noch Zwischenprobleme (Lemmas) als Schritte im Theorem bereitstellen, aber dies ist 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 den Z3, einen handelsüblichen SMT-Solver. Der große Vorteil des Z3 war, dass es viel bequemer 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 beweisen, sodass sie nicht auf minimale UX beschränkt waren.

SMT traf die FM-Community unter dem Atem, weil es plötzlich viele einfache Beweise trivial machte und es ihr ermöglichte, sich sehr komplexen Problemen zu nähern. So konnten die Menschen in ausdrucksstärkeren Sprachen arbeiten, da nun die Probleme der Ausdrucksaussagen gelöst wurden. Im IronFleet- Projekt sind unglaubliche Fortschritte zu verzeichnen : Mit den besten SMT-Lösern und einer erweiterten Verifizierungssprache konnte Microsoft in nur 3,7 Mannjahren 5.000 Zeilen bewährten Dafny-Codes schreiben! Dies ist ein unglaublich schnelles Tempo: Bis zu vier ganze Zeilen pro Tag (Hinweis: Der vorherige Datensatz gehörte seL4 , dessen Entwickler zwei Zeilen pro Tag in C geschrieben haben.

Die Beweise sind schwierig.

Warum wird das benötigt?

Es ist Zeit, zurückzutreten und zu fragen: "Was ist der Sinn?" Wir versuchen zu beweisen, dass ein Programm einer bestimmten Spezifikation entspricht. Korrektheit ist ein Bereich. Die Überprüfung besteht aus zwei Teilen: Wie objektiv „korrekt“ Ihr Programm ist und wie sorgfältig Sie die Richtigkeit überprüft haben. Je mehr überprüft wird, desto besser, aber die Überprüfung ist die Zeit und das Geld wert. Wenn wir verschiedene Einschränkungen haben (Leistung, Time-to-Market, Kosten usw.), ist eine vollständige Validierung nicht unbedingt die beste Option. Dann stellt sich die Frage, was der Mindestscheck ist, den wir brauchen und was er kostet. In den meisten Fällen reichen beispielsweise 90% oder 95% oder 99% Korrektheit für Sie aus. Vielleicht sollten Sie Zeit damit verbringen, die Benutzeroberfläche zu verbessern, anstatt die verbleibenden 1% zu überprüfen?

Dann die Frage: "Ist ein Scheck von 90/95/99% viel billiger als 100%?" Die Antwort lautet ja. Es ist sehr angenehm zu sagen, dass die Codebasis, die wir gut getestet und getippt haben, bis auf einige Korrekturen in der Produktion grundsätzlich korrekt ist und wir sogar mehr als vier Codezeilen pro Tag schreiben. Tatsächlich hätte die überwiegende Mehrheit der Fehlfunktionen in verteilten Systemen durch etwas umfassendere Tests verhindert werden können. Und es ist nur eine Erweiterung der Tests, ganz zu schweigen von Fuzzing, eigenschaftsbasierten Tests oder Modelltests. Mit diesen einfachen Tricks können Sie ein wirklich herausragendes Ergebnis erzielen, ohne einen vollständigen Beweis erhalten zu müssen.

Was ist, wenn das Tippen und Testen keine ausreichende Überprüfung bietet? Es ist immer noch viel einfacher, von 90% auf 99% zu wechseln als von 99% auf 100%. Wie bereits erwähnt, ist Cleanroom eine Entwicklerpraxis, die umfassende Dokumentation, gründliche Flussanalyse und umfassende Codeüberprüfungen 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 (Hinweis: Zahlen aus der Stavley-Studie in Richtung Null- Fehler -Programmierung >, aber seien Sie immer skeptisch und überprüfen Sie die Quelle ). Das Programmieren von Cleanroom verlangsamt das Entwicklungstempo nicht und geht mit Sicherheit schneller als 4 Zeilen pro Tag. Und Cleanroom selbst ist nur eine von vielen hochzuverlässigen Softwareentwicklungsmethoden, die zwischen der üblichen Entwicklung und der Codeüberprüfung liegen. Sie benötigen keine vollständige Überprüfung, um eine gute oder fast perfekte Software zu schreiben. Es gibt Zeiten, in denen es gebraucht wird, aber für die meisten Branchen ist es eine Geldverschwendung.

Dies bedeutet jedoch nicht, dass formale Methoden im Allgemeinen unwirtschaftlich sind. Viele der oben genannten hochzuverlässigen Methoden basieren auf dem Schreiben von Codespezifikationen, die Sie formal nicht nachweisen. In Bezug auf die Überprüfung gibt es zwei gängige Möglichkeiten, von denen die Branche profitiert. Zuerst die Entwurfsüberprüfung anstelle des Codes, 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, eine vollständige Überprüfung 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 wird und niemals außerhalb des Bereichs liegt. Dies sind auch sehr nützliche Informationen. Selbst der einfachste Beweis für C-Programme ist eine großartige Möglichkeit , einen großen Teil des undefinierten Verhaltens zu eliminieren .

Das Problem ist die Zugänglichkeit . , . , , . , C Java. . , SPARK Ada, SPARK Ada. .

. — : , tail tail, , [a] -> [a] . Rust Pony . SPARK Frama-C , . , : , . , , Rust Haskell, .

. , , . , : - , , , , .

, , . - , - . , , , , , . , , , , . , . , , .

, « , ». , , . ? - ? ? « » :

, ? ?
? ? ? ?
? , ? «» , ?
, ? ?
? « » ?
GDPR?
.

. , , , . , , , .

, , . , , (: ). (DL), ( , ; « », ).

, DL VDM 1972 . . DL , (CVL). , DL , CVL — . , DL . , DL:

Sprache
Z.	-
Promela	Beiträge	CSP
SDL		-

DL , . , . , DL . Praxis ( Altran), «--» — Z- SPARK — . , .

Alloy Chord, -. AWS 35- , TLA+. , , .

- . , , . , , . . - DL, , , .

, , — .

, , . , : (model checker). , , , . , (: , JMBC, , ).

. -, , . -, , . -, , . , , 35 . .

. -, . , (unbounded) , . , : . … , , . , , .

— (state-space explosion). , , , . , (4*3)! / (4!)^3 = 34 650 (). , 4 300 000. , . , ! , . , , .

: . — « » , . ( ) . AWS .

, (: , « » — ). , , .

, , , . ? DV . — , — : .

, — . DL , (: ; . ; , ( ) : ).

, . , , , .

, , - . , , (, , TDD) . , , .

, : TDD , TDD, Haskell , .

, Agile , . Kann sein. , , Agile, FM. , . , , .

, , .

Zusammenfassung

— . , SMT- . - , , .

, . , . - , . , .

, , . , , « — ». , - .

Warum wenden die Menschen keine formalen Methoden an?