Dies ist ein Übersetzungsartikel aus dem Stanford-Workshop . Aber vor ihr ist eine kleine Einführung. Wie entstehen Zombies? Jeder ist in eine Situation geraten, in der Sie einen Freund oder Kollegen auf Ihr Niveau bringen möchten, aber es funktioniert nicht. Außerdem "klappt es nicht" bei Ihnen weniger als bei ihm: Auf der einen Seite der Waage steht ein normales Gehalt, Aufgaben usw. und auf der anderen Seite das Bedürfnis zu denken. Denken ist unangenehm und schmerzhaft. Er gibt schnell auf und schreibt weiterhin Code, ohne das Gehirn einzubeziehen. Sie stellen sich vor, wie viel Aufwand Sie aufwenden müssen, um die Barriere der erlernten Hilflosigkeit zu überwinden, und Sie tun es einfach nicht. Auf diese Weise entstehen Zombies, die scheinbar geheilt werden können, aber es scheint, dass niemand dies tun wird.
Als ich sah, dass Leslie Lampport (ja, derselbe Freund aus den Lehrbüchern) nach Russland kam und keinen Bericht, sondern eine Frage-und-Antwort-Sitzung gab, war ich etwas vorsichtig. Für alle Fälle ist Leslie ein weltberühmter Wissenschaftler, der Autor der grundlegenden Arbeiten im Bereich des verteilten Rechnens, und Sie können ihn auch an den Buchstaben La in LaTeX - „Lamport TeX“ erkennen. Der zweite alarmierende Faktor ist seine Forderung: Jeder, der kommt, sollte (völlig kostenlos) im Voraus ein paar seiner Berichte anhören, mindestens eine Frage zu ihnen stellen und erst dann kommen. Ich beschloss zu sehen, was Lampport dort sendete - und es war großartig! Dies ist genau das, eine magische Verbindungspille zur Behandlung eines Zombies. Ich warne Sie: Aus dem Text kann es insbesondere für Fans superflexibler Methoden und Nicht-Enthusiasten herausbrennen, zu testen, was geschrieben steht.
Tatsächlich beginnt nach Habrokat die Übersetzung des Seminars. Viel Spaß beim Lesen!
Unabhängig davon, welche Aufgabe Sie übernehmen, müssen Sie immer drei Schritte ausführen:
- Entscheiden Sie, welches Ziel Sie erreichen möchten.
- Entscheiden Sie, wie Sie Ihr Ziel erreichen.
- Komm zu deinem Ziel.
Dies gilt auch für die Programmierung. Wenn wir den Code schreiben, brauchen wir:
- entscheiden, was das Programm tun soll;
- genau bestimmen, wie es seine Aufgabe erfüllen soll;
- Schreiben Sie den entsprechenden Code.
Der letzte Schritt ist natürlich sehr wichtig, aber ich werde heute nicht darüber sprechen. Stattdessen diskutieren wir die ersten beiden. Jeder Programmierer führt sie aus, bevor er mit der Arbeit beginnt. Sie setzen sich nicht zum Schreiben hin, wenn Sie nicht entschieden haben, was Sie schreiben: einen Browser oder eine Datenbank. Eine genaue Vorstellung vom Ziel muss vorhanden sein. Und Sie werden sicher darüber nachdenken, was genau das Programm tun wird, und es nicht irgendwie schreiben, in der Hoffnung, dass der Code selbst irgendwie zu einem Browser wird.
Wie genau findet diese vorläufige Überlegung des Codes statt? Wie viel Aufwand sollten wir dafür aufwenden? Es hängt alles davon ab, wie schwierig das Problem ist, das wir lösen. Angenommen, wir möchten ein fehlertolerantes verteiltes System schreiben. In diesem Fall sollten wir alles richtig betrachten, bevor wir uns für den Code setzen. Und wenn wir nur die Ganzzahlvariable um 1 erhöhen müssen? Auf den ersten Blick ist hier alles trivial und es sind keine Gedanken erforderlich, aber dann erinnern wir uns, dass ein Überlauf auftreten kann. Selbst um zu verstehen, ob ein Problem einfach oder komplex ist, müssen Sie daher zunächst überlegen.
Wenn Sie über mögliche Lösungen für das Problem nachdenken, können Sie Fehler vermeiden. Dies setzt jedoch voraus, dass Sie klar denken. Um dies zu erreichen, müssen Sie Ihre Gedanken aufschreiben. Ich mag Dick Gindons Zitat sehr: "Wenn Sie schreiben, zeigt Ihnen die Natur, wie schlampig Ihr Denken ist." Wenn Sie nicht schreiben, scheint es Ihnen nur, dass Sie denken. Und Sie müssen Ihre Gedanken in Form von Spezifikationen aufschreiben.
Spezifikationen erfüllen viele Funktionen, insbesondere bei großen Projekten. Aber ich werde nur über einen von ihnen sprechen: Sie helfen uns, klar zu denken. Klar zu denken ist sehr wichtig und ziemlich schwierig, deshalb brauchen wir hier jede Hilfe. In welcher Sprache sollen wir die Spezifikationen schreiben? Dies ist immer die erste Frage für Programmierer: In welcher Sprache werden wir schreiben? Es gibt keine richtige Antwort darauf: Die Probleme, die wir lösen, sind zu vielfältig. TLA + ist für einige nützlich - dies ist die Spezifikationssprache, die ich entwickelt habe. Für andere ist es bequemer, Chinesisch zu verwenden. Es hängt alles von der Situation ab.
Eine andere Frage ist wichtiger: Wie kann man klarer denken? Antwort: Wir müssen wie Wissenschaftler denken. Diese Denkweise hat sich in den letzten 500 Jahren bewährt. In der Wissenschaft bauen wir mathematische Modelle der Realität. Die Astronomie war vielleicht die erste Wissenschaft im engeren Sinne des Wortes. In dem in der Astronomie verwendeten mathematischen Modell erscheinen Himmelskörper als Punkte mit Masse, Position und Impuls, obwohl sie in Wirklichkeit äußerst komplexe Objekte mit Bergen und Ozeanen und Gezeiten sind. Dieses Modell wurde wie jedes andere entwickelt, um bestimmte Probleme zu lösen. Es ist ideal, um festzustellen, wohin das Teleskop gerichtet werden soll, wenn Sie einen Planeten finden müssen. Wenn Sie jedoch das Wetter auf diesem Planeten vorhersagen möchten, funktioniert dieses Modell nicht.
Mithilfe der Mathematik können wir die Eigenschaften eines Modells bestimmen. Und die Wissenschaft zeigt, wie diese Eigenschaften mit der Realität zusammenhängen. Sprechen wir über unsere Wissenschaft, die Informatik. Die Realität, mit der wir arbeiten, sind Computersysteme verschiedener Typen: Prozessoren, Spielekonsolen, Computer, Ausführen von Programmen und so weiter. Ich werde über das Ausführen eines Programms auf einem Computer sprechen, aber im Großen und Ganzen gelten all diese Schlussfolgerungen für jedes Computersystem. In unserer Wissenschaft verwenden wir viele verschiedene Modelle: eine Turing-Maschine, teilweise geordnete Ereignissätze und viele andere.
Was ist ein Programm? Dies ist jeder Code, der unabhängig betrachtet werden kann. Angenommen, wir müssen einen Browser schreiben. Wir führen drei Aufgaben aus: Wir entwerfen die Präsentation des Programms für den Benutzer, schreiben dann ein allgemeines Schema des Programms und schließlich schreiben wir den Code. Während wir den Code schreiben, verstehen wir, dass wir ein Werkzeug zum Formatieren des Textes schreiben müssen. Hier müssen wir noch einmal drei Probleme lösen: Bestimmen Sie, welchen Text dieses Tool zurückgeben wird; Wählen Sie einen Algorithmus für die Formatierung. Code schreiben. Diese Aufgabe hat eine eigene Unteraufgabe: Fügen Sie Bindestriche korrekt in Wörter ein. Wir lösen diese Unteraufgabe auch in drei Schritten - wie wir sehen, werden sie auf vielen Ebenen wiederholt.
Betrachten wir den ersten Schritt genauer: Welches Problem löst das Programm? Hier modellieren wir meistens ein Programm als eine Funktion, die eine Eingabe empfängt und eine Ausgabe gibt. In der Mathematik wird eine Funktion normalerweise als geordnete Menge von Paaren beschrieben. Beispielsweise wird die Quadrierungsfunktion für natürliche Zahlen als die Menge {<0,0>, <1,1>, <2,4>, <3,9>, ...} beschrieben. Der Umfang einer solchen Funktion ist die Menge der ersten Elemente jedes Paares, dh natürlicher Zahlen. Um eine Funktion zu definieren, müssen wir ihren Umfang und ihre Formel angeben.
Funktionen in der Mathematik sind jedoch nicht dasselbe wie Funktionen in Programmiersprachen. Mathematik ist viel einfacher. Da ich keine Zeit für komplexe Beispiele habe, betrachten Sie eine einfache: eine Funktion in C oder eine statische Methode in Java, die den größten gemeinsamen Teiler von zwei Ganzzahlen zurückgibt. In der Spezifikation dieser Methode schreiben wir: Berechnet GCD(M,N) für die Argumente M und N , wobei GCD(M,N) eine Funktion ist, deren Domäne die Menge von Ganzzahlpaaren ist und der Rückgabewert die größte Ganzzahl ist, die durch teilbar ist M und N Wie hängt die Realität mit diesem Modell zusammen? Das Modell arbeitet mit ganzen Zahlen, und in C oder Java haben wir ein 32-Bit- int . Mit diesem Modell können wir entscheiden, ob der GCD Algorithmus korrekt ist, aber Überlauffehler werden nicht verhindert. Dies würde ein komplexeres Modell erfordern, für das keine Zeit bleibt.
Lassen Sie uns über die Einschränkungen der Funktion als Modell sprechen. Die Arbeit einiger Programme (z. B. Betriebssysteme) besteht nicht darin, einen bestimmten Wert für bestimmte Argumente zurückzugeben, sondern kann kontinuierlich ausgeführt werden. Darüber hinaus ist die Funktion als Modell für den zweiten Schritt schlecht geeignet: die Planung einer Methode zur Lösung des Problems. Schnelles Sortieren und Blasensortieren berechnen dieselbe Funktion, dies sind jedoch völlig unterschiedliche Algorithmen. Um zu beschreiben, wie das Ziel des Programms erreicht werden kann, verwende ich ein anderes Modell. Nennen wir es das Standard-Verhaltensmodell. Das darin enthaltene Programm wird als die Menge aller zulässigen Verhaltensweisen dargestellt, von denen jedes wiederum eine Folge von Zuständen ist und ein Zustand eine Zuweisung von Werten zu Variablen ist.
Mal sehen, wie der zweite Schritt für den euklidischen Algorithmus aussehen wird. Wir müssen GCD(M, N) berechnen. Wir initialisieren M als x und N als y und subtrahieren dann die kleinere dieser Variablen von der größeren, bis sie gleich sind. Wenn beispielsweise M = 12 und N = 18 , können wir das folgende Verhalten beschreiben:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Und wenn M = 0 und N = 0 ? Null ist durch alle Zahlen teilbar, daher gibt es in diesem Fall keinen größten Teiler. In dieser Situation müssen wir zum ersten Schritt zurückkehren und fragen: Müssen wir die GCD wirklich für nicht positive Zahlen berechnen? Wenn dies nicht erforderlich ist, müssen Sie nur die Spezifikation ändern.
Hier sollte ein kleiner Exkurs über die Produktivität gemacht werden. Sie wird häufig anhand der Anzahl der pro Tag geschriebenen Codezeilen gemessen. Ihre Arbeit ist jedoch viel nützlicher, wenn Sie eine bestimmte Anzahl von Zeilen entfernen, da Sie weniger Platz für Fehler haben. Der einfachste Weg, den Code loszuwerden, ist der erste Schritt. Es ist möglich, dass Sie einfach nicht alle Schnickschnack benötigen, die Sie implementieren möchten. Der schnellste Weg, ein Programm zu vereinfachen und Zeit zu sparen, besteht darin, keine Dinge zu tun, die es nicht wert sind, getan zu werden. Der zweite Schritt steht hinsichtlich des Zeitsparpotenzials an zweiter Stelle. Wenn Sie die Produktivität an der Anzahl der geschriebenen Zeilen messen, werden Sie weniger produktiv , wenn Sie darüber nachdenken, wie die Aufgabe ausgeführt werden soll, da Sie dasselbe Problem mit weniger Code lösen können. Ich kann hier keine genauen Statistiken angeben, da ich die Anzahl der Zeilen, die ich nicht geschrieben habe, nicht berechnen kann, weil ich Zeit mit der Spezifikation verbracht habe, dh mit dem ersten und zweiten Schritt. Und das Experiment kann auch hier nicht platziert werden, da wir im Experiment kein Recht haben, den ersten Schritt abzuschließen, die Aufgabe ist vorbestimmt.
In informellen Spezifikationen werden viele Schwierigkeiten leicht übersehen. Es ist nicht kompliziert, strenge Spezifikationen für Funktionen zu schreiben, ich werde dies nicht diskutieren. Stattdessen werden wir über das Schreiben strenger Spezifikationen für Standardverhaltensmodelle sprechen. Es gibt einen Satz, der besagt, dass jeder Satz von Verhaltensweisen unter Verwendung der Sicherheitseigenschaft und der Lebendigkeitseigenschaft beschrieben werden kann. Sicherheit bedeutet, dass nichts Schlimmes passiert, das Programm gibt nicht die falsche Antwort. Vitalität bedeutet, dass früher oder später etwas Gutes passieren wird, dh das Programm wird früher oder später die richtige Antwort geben. Sicherheit ist in der Regel ein wichtigerer Indikator, hier treten am häufigsten Fehler auf. Um Zeit zu sparen, werde ich daher nicht über die Überlebensfähigkeit sprechen, obwohl dies natürlich auch wichtig ist.
Wir erreichen Sicherheit, indem wir zum einen die vielen möglichen Ausgangszustände vorschreiben. Und zweitens Beziehungen zu allen möglichen nächsten Zuständen für jeden Zustand. Wir werden uns als Wissenschaftler verhalten und die Zustände mathematisch definieren. Die Menge der Anfangszustände wird beispielsweise im Fall des euklidischen Algorithmus durch die Formel beschrieben: (x = M) ∧ (y = N) . Für bestimmte Werte von M und N gibt es nur einen Anfangszustand. Die Beziehung zum nächsten Zustand wird durch eine Formel beschrieben, in der die Variablen des nächsten Zustands mit einem Bindestrich und der aktuelle Zustand ohne Bindestrich geschrieben werden. Im Fall des euklidischen Algorithmus werden wir uns mit der Disjunktion zweier Formeln befassen, von denen eine der größte Wert ist und in der zweiten - y :
Im ersten Fall ist der neue Wert von y gleich dem vorherigen Wert von y, und wir erhalten den neuen Wert von x, indem wir den kleineren von der größeren Variablen subtrahieren. Im zweiten Fall machen wir das Gegenteil.
Kehren wir zum euklidischen Algorithmus zurück. Angenommen, M = 12 , N = 18 . Dies bestimmt den einzigen Anfangszustand (x = 12) ∧ (y = 18) . Dann ersetzen wir diese Werte in der obigen Formel und erhalten:
Hier die einzig mögliche Lösung: x' = 18 - 12 ∧ y' = 12 , und wir erhalten das Verhalten: [x = 12, y = 18] . Auf die gleiche Weise können wir alle Zustände in unserem Verhalten beschreiben: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6] .
Im letzten Zustand [x = 6, y = 6] beide Teile des Ausdrucks falsch, daher hat er keinen nächsten Zustand. Wir haben also die vollständige Spezifikation des zweiten Schritts - wie wir sehen, ist dies eine ganz normale Mathematik, wie die von Ingenieuren und Wissenschaftlern, und nicht seltsam, wie in der Informatik.
Diese beiden Formeln können zu einer zeitlichen Logikformel kombiniert werden. Sie ist elegant und leicht zu erklären, aber jetzt hat sie keine Zeit. Zeitliche Logik, die wir möglicherweise nur für das Eigentum der Lebendigkeit benötigen, für die Sicherheit wird sie nicht benötigt. Zeitliche Logik als solche ist nicht angenehm, es ist keine ganz normale Mathematik, aber im Fall von Lebendigkeit ist es ein notwendiges Übel.
Im euklidischen Algorithmus gibt es für jeden Wert von x und y eindeutige Werte von x' und y' , die die Beziehung zum nächsten Zustand wahr machen. Mit anderen Worten ist der euklidische Algorithmus deterministisch. Um einen nicht deterministischen Algorithmus zu simulieren, ist es notwendig, dass der aktuelle Zustand mehrere mögliche zukünftige Zustände hat und dass jeder Wert der Variablen ohne Primzahl mehrere Werte der Variablen mit einem Strich hat, bei dem die Beziehung zum nächsten Zustand wahr ist. Dies ist nicht schwer zu tun, aber ich werde jetzt keine Beispiele nennen.
Um ein funktionierendes Werkzeug zu erstellen, benötigen Sie formale Mathematik. Wie macht man die Spezifikation formal? Dazu benötigen wir eine formale Sprache, zum Beispiel TLA + . Die Spezifikation des euklidischen Algorithmus in dieser Sprache sieht folgendermaßen aus:
Das Gleichheitszeichen mit einem Dreieck bedeutet, dass der Wert links vom Zeichen als gleich dem Wert rechts vom Zeichen definiert ist. Im Wesentlichen ist eine Spezifikation eine Definition, in unserem Fall zwei Definitionen. Sie müssen der Spezifikation in TLA + Deklarationen und eine Syntax hinzufügen, wie in der obigen Folie. In ASCII sieht es folgendermaßen aus:
Wie Sie sehen können, nichts kompliziertes. Die Spezifikation für TLA + kann überprüft werden, d. H. Alle möglichen Verhaltensweisen in einem kleinen Modell umgehen. In unserem Fall ist dieses Modell bestimmte Werte von M und N Dies ist eine sehr effiziente und einfache Überprüfungsmethode, die vollständig automatisch ausgeführt wird. Darüber hinaus können Sie formale Beweise für die Wahrheit schreiben und diese mechanisch überprüfen. Dies nimmt jedoch viel Zeit in Anspruch, sodass fast niemand dies tut.
Der Hauptnachteil von TLA + ist, dass es sich um Mathematik handelt und Programmierer und Informatiker Angst vor Mathematik haben. Auf den ersten Blick klingt das wie ein Witz, aber leider sage ich das in aller Ernsthaftigkeit. Mein Kollege hat mir gerade erzählt, wie er versucht hat, TLA + mehreren Entwicklern zu erklären. Sobald die Formeln auf dem Bildschirm erschienen, hatten sie sofort Glasaugen. Wenn TLA + also unheimlich ist, können Sie PlusCal verwenden , eine Art Programmiersprache für Spielzeug. Ein Ausdruck in PlusCal kann ein beliebiger TLA + -Ausdruck sein, dh im Großen und Ganzen ein beliebiger mathematischer Ausdruck. PlusCal verfügt auch über eine Syntax für nicht deterministische Algorithmen. Aufgrund der Tatsache, dass jeder TLA + -Ausdruck in PlusCal geschrieben werden kann, ist er für jede echte Programmiersprache viel ausdrucksvoller. PlusCal ist weiter in die einfach zu lesende TLA + -Spezifikation kompiliert. Dies bedeutet natürlich nicht, dass die komplexe PlusCal-Spezifikation in TLA + zu einer einfachen wird - nur die Entsprechung zwischen ihnen ist offensichtlich, es wird keine zusätzliche Komplexität geben. Schließlich kann diese Spezifikation mit TLA + -Tools überprüft werden. Im Allgemeinen kann PlusCal helfen, die Phobie der Mathematik zu überwinden, und es ist selbst für Programmierer und Informatiker leicht zu verstehen. In der Vergangenheit habe ich einige Zeit (ungefähr 10 Jahre) Algorithmen darauf veröffentlicht.
Vielleicht wird jemand Einwände erheben, dass TLA + und PlusCal Mathematik sind und Mathematik nur an erfundenen Beispielen funktioniert. In der Praxis benötigen Sie eine echte Sprache mit Typen, Prozeduren, Objekten usw. Es ist nicht so. Chris Newcomb, der bei Amazon gearbeitet hat, schreibt: „Wir haben TLA + in zehn großen Projekten verwendet, und in jedem Fall hat seine Verwendung einen wesentlichen Beitrag zur Entwicklung geleistet, da wir gefährliche Fehler erkennen konnten, bevor wir in Produktion gingen, und weil er uns gegeben hat Verständnis und Vertrauen, die für aggressive Leistungsoptimierungen erforderlich sind, die die Wahrheit des Programms nicht beeinflussen . “ Sie können oft hören, dass wir bei Verwendung formaler Methoden einen ineffizienten Code erhalten - in der Praxis ist alles genau umgekehrt. Darüber hinaus wird angenommen, dass Manager nicht von der Notwendigkeit formaler Methoden überzeugt werden können, selbst wenn Programmierer von ihrer Nützlichkeit überzeugt sind. Und Newcomb schreibt: „Manager bemühen sich jetzt in jeder Hinsicht, Spezifikationen für TLA + zu schreiben, und sie widmen sich speziell der Zeit dafür . “ Wenn Manager sehen, dass TLA + funktioniert, akzeptieren sie dies gerne. Chris Newcomb hat dies vor ungefähr sechs Monaten (im Oktober 2014) geschrieben, aber jetzt, soweit ich weiß, wird TLA + in 14 Projekten verwendet, nicht in 10. Ein weiteres Beispiel bezieht sich auf das Design der XBox 360. Ein Praktikant kam zu Charles Thacker und schrieb Spezifikation für ein Speichersystem. Dank dieser Spezifikation wurde ein Fehler gefunden, der sonst nicht bemerkt worden wäre und aufgrund dessen jede XBox 360 nach vier Stunden Betriebszeit fallen würde. IBM Ingenieure haben bestätigt, dass ihre Tests diesen Fehler nicht erkannt hätten.
Sie können mehr über TLA + im Internet lesen und jetzt über informelle Spezifikationen sprechen. Wir müssen selten Programme schreiben, die den am wenigsten verbreiteten Teiler und dergleichen berechnen. Häufiger schreiben wir Programme wie das hübsche Druckertool, das ich für TLA + geschrieben habe. Nach der einfachsten Verarbeitung würde der TLA + -Code folgendermaßen aussehen:
Im obigen Beispiel wollte der Benutzer jedoch höchstwahrscheinlich, dass die Konjunktion und die Gleichheitszeichen ausgerichtet werden. Die richtige Formatierung würde also eher so aussehen:
Betrachten Sie ein anderes Beispiel:
Im Gegensatz dazu war die Ausrichtung von Gleichheitszeichen, Addition und Multiplikation in der Quelle zufällig, so dass die einfachste Verarbeitung ausreicht. Im Allgemeinen gibt es keine genaue mathematische Definition der korrekten Formatierung, da "richtig" in diesem Fall "was der Benutzer will" bedeutet und dies nicht mathematisch bestimmt werden kann.
Es scheint, dass die Spezifikation nutzlos ist, wenn wir keine Definition der Wahrheit haben. Aber das ist nicht so. Wenn wir nicht genau wissen, was das Programm tun soll, heißt das nicht, dass wir seine Arbeit nicht durchdenken müssen - im Gegenteil, wir sollten uns noch mehr darum bemühen. Die Spezifikation hier ist besonders wichtig. Es ist unmöglich, das optimale Programm für die strukturelle Auflistung zu bestimmen, aber dies bedeutet nicht, dass wir es überhaupt nicht durchführen sollten, und das Schreiben von Code als Bewusstseinsstrom ist keine Sache. Am Ende habe ich eine Spezifikation von sechs Regeln mit Definitionen in Form von Kommentaren in einer Java-Datei geschrieben. Hier ist ein Beispiel für eine der Regeln: a left-comment token is LeftComment aligned with its covering token . Diese Regel ist beispielsweise in mathematischem Englisch geschrieben: LeftComment aligned , left-comment und covering token sind Begriffe mit Definitionen. So beschreiben Mathematiker Mathematik: Sie schreiben Definitionen von Begriffen und auf deren Grundlage Regeln. Der Vorteil dieser Spezifikation besteht darin, dass das Verstehen und Debuggen der sechs Regeln viel einfacher ist als 850 Codezeilen. Ich muss sagen, dass das Schreiben dieser Regeln nicht einfach war, es wurde ziemlich viel Zeit für das Debuggen aufgewendet. Speziell für diesen Zweck habe ich Code geschrieben, der angibt, welche Regel verwendet wurde. Aufgrund der Tatsache, dass ich diese sechs Regeln anhand einiger Beispiele überprüft habe, musste ich keine 850 Codezeilen debuggen, und die Fehler erwiesen sich als recht leicht zu finden. Java hat einige großartige Tools dafür. Wenn ich nur den Code schreiben würde, würde es viel länger dauern und die Formatierung würde sich als schlechter herausstellen.
Warum war es unmöglich, eine formale Spezifikation zu verwenden? Einerseits ist die korrekte Ausführung hier nicht sehr wichtig. Eine strukturelle Auflistung wird sicher niemandem gefallen, so dass ich nicht in allen ungewöhnlichen Situationen die richtige Arbeit finden musste. Noch wichtiger ist die Tatsache, dass ich keine geeigneten Werkzeuge hatte. Das Tool zum Testen von TLA + -Modellen ist hier nutzlos, daher müsste ich manuell Beispiele schreiben.
Die angegebene Spezifikation weist Merkmale auf, die allen Spezifikationen gemeinsam sind. Es ist von einer höheren Ebene als Code. Sie können es in jeder Sprache implementieren. Um es zu schreiben, sind alle Werkzeuge oder Methoden nutzlos. Kein Programmierkurs hilft Ihnen beim Schreiben dieser Spezifikation. Und es gibt keine Tools, die diese Spezifikation unnötig machen könnten, es sei denn, Sie schreiben natürlich eine Sprache speziell für das Schreiben von Strukturlistenprogrammen auf TLA +. Schließlich sagt diese Spezifikation nichts darüber aus, wie wir den Code genau schreiben werden, sondern gibt nur an, was dieser Code tut. Wir schreiben eine Spezifikation, die uns hilft, das Problem zu durchdenken, bevor wir über Code nachdenken.
Diese Spezifikation weist jedoch auch Merkmale auf, die sie von anderen Spezifikationen unterscheiden. 95% der anderen Spezifikationen sind viel kürzer und einfacher:
Ferner ist diese Spezifikation ein Satz von Regeln. Dies ist normalerweise ein Zeichen für eine schlechte Spezifikation. Das Verständnis der Auswirkungen des Regelsatzes ist ziemlich schwierig, weshalb ich viel Zeit damit verbringen musste, sie zu debuggen. In diesem Fall konnte ich jedoch keinen besseren Weg finden.
Es lohnt sich, ein paar Worte über Programme zu sagen, die kontinuierlich arbeiten. In der Regel arbeiten sie parallel, beispielsweise Betriebssysteme oder verteilte Systeme. Sehr wenige können sie in ihren Gedanken oder auf dem Papier verstehen, und ich bin keiner von ihnen, obwohl ich es mir einmal leisten konnte. Daher werden Tools benötigt, die unsere Arbeit testen - zum Beispiel TLA + oder PlusCal.
Warum mussten Sie eine Spezifikation schreiben, wenn ich bereits wusste, was genau der Code tun sollte? Tatsächlich schien es mir nur, dass ich es wusste. Wenn es eine Spezifikation gibt, muss ein Außenstehender nicht mehr in den Code einsteigen, um zu verstehen, was genau er tut. Ich habe eine Regel: Es sollte keine allgemeinen Regeln geben. Diese Regel hat natürlich eine Ausnahme. Dies ist die einzige allgemeine Regel, die ich befolge: Die Spezifikation des Codes besteht darin, den Leuten alles zu sagen, was sie wissen müssen, wenn sie diesen Code verwenden.
Was genau müssen Programmierer über das Denken wissen? Für den Anfang wie alle anderen: Wenn Sie nicht schreiben, denken Sie nur, dass Sie denken. Darüber hinaus müssen Sie vor dem Codieren nachdenken, was bedeutet, dass Sie vor dem Codieren schreiben müssen. Eine Spezifikation schreiben wir, bevor wir mit dem Codieren beginnen. Die Spezifikation wird für jeden Code benötigt, der von jedem verwendet oder geändert werden kann. Und dieser „Jemand“ könnte sich einen Monat nach dem Schreiben als Autor des Codes herausstellen. Die Spezifikation wird für große Programme und Systeme, für Klassen, für Methoden und manchmal sogar für komplexe Abschnitte einer einzelnen Methode benötigt. Was genau muss über den Code geschrieben werden? Es ist notwendig zu beschreiben, was er tut, dh etwas, das für jede Person, die diesen Code verwendet, nützlich sein kann. Manchmal kann es auch erforderlich sein, genau anzugeben, wie der Code sein Ziel erreicht. Wenn wir diese Methode im Verlauf von Algorithmen bestanden haben, nennen wir sie einen Algorithmus. Wenn es etwas Besonderes und Neues ist, dann nennen wir es High-Level-Design. Es gibt keinen formalen Unterschied: Beide sind ein abstraktes Modell des Programms.
Wie genau sollte eine Codespezifikation geschrieben werden? Hauptsache: Es sollte eine Ebene höher sein als der Code selbst. Es sollte Zustände und Verhaltensweisen beschreiben. Es sollte so streng sein, wie es die Aufgabe erfordert. Wenn Sie eine Spezifikation zur Implementierung der Aufgabe schreiben, kann diese in Pseudocode oder mit PlusCal geschrieben werden. Das Lernen, Spezifikationen zu schreiben, ist für formale Spezifikationen erforderlich. Dies gibt Ihnen die notwendigen Fähigkeiten, die helfen, auch diejenigen mit informellen. Und wie lernt man, formale Spezifikationen zu schreiben? Als wir das Programmieren gelernt haben, haben wir Programme geschrieben und sie dann debuggt.Das Gleiche gilt hier: Sie müssen eine Spezifikation schreiben, sie mit dem Modellprüfwerkzeug überprüfen und Fehler beheben. TLA + ist möglicherweise nicht die beste Sprache für eine formale Spezifikation, und eine andere Sprache ist wahrscheinlich besser für Ihre spezifischen Anforderungen. Der Vorteil von TLA + ist, dass es Ihnen großartiges mathematisches Denken beibringt.
Wie verknüpfe ich Spezifikation und Code? Mit Hilfe von Kommentaren, die mathematische Konzepte und deren Umsetzung verbinden. Wenn Sie mit Diagrammen arbeiten, haben Sie auf Programmebene Arrays von Knoten und Arrays von Links. Daher müssen Sie genau schreiben, wie der Graph von diesen Programmierstrukturen implementiert wird.
, . , , . , . . , , . , . , .
— . — Amazon. . ? . , , . , . — , . . .
. - , , . , - , , . . , . , , . , ? -, , , , . , . , . , , . -, , . . , , .
, , . - . , — . , , . , , , , . . , . , , — . , .
TLA+ PlusCal , . , .
, . — , . , Hydra 2019, 11-12 2019 -. .