Programmieren ist mehr als nur Programmieren

Dieser Artikel ist eine Übersetzung Stanford-Seminar. Aber vor ihr eine kleine Einführung. Wie entstehen Zombies? Jeder kommt in die Situation, dass er einen Freund oder Kollegen auf sein Niveau bringen möchte, es aber nicht klappt. Und es ist nicht so sehr bei Ihnen, sondern bei ihm, dass „es nicht klappt“: Auf der einen Seite der Skala steht ein normales Gehalt, Aufgaben usw. und auf der anderen Seite der Drang zum Nachdenken. Denken ist unangenehm und schmerzhaft. Er gibt schnell auf und schreibt weiter Code, ohne sein Gehirn überhaupt einzuschalten. Sie stellen sich vor, wie viel Mühe es kostet, die Barriere der erlernten Hilflosigkeit zu überwinden, und Sie tun es einfach nicht. Auf diese Weise entstehen Zombies, die anscheinend geheilt werden können, aber es scheint, dass niemand es tun wird.

Als ich das sah Leslie Lamport (Ja, derselbe Kamerad aus den Lehrbüchern) kommt nach Russland und keinen Bericht macht, sondern eine Frage-und-Antwort-Runde, da war ich etwas vorsichtig. Nur für den Fall, Leslie ist ein weltberühmter Wissenschaftler, der Autor grundlegender Arbeiten zum verteilten Rechnen, und Sie können ihn auch an den Buchstaben La im Wort LaTeX kennen – „Lamport TeX“. Der zweite alarmierende Faktor ist seine Forderung: Jeder, der kommt, muss sich (völlig kostenlos) vorab ein paar seiner Berichte anhören, mindestens eine Frage dazu stellen und erst dann kommen. Ich beschloss, zu sehen, was Lamport dort sendete – und es war großartig! Es ist genau das Ding, die magische Verbindungspille, um Zombies zu heilen. Ich warne Sie: Liebhaber superflexibler Methoden und diejenigen, die nicht gerne testen, was geschrieben steht, können aufgrund des Textes merklich ausbrennen.

Nach Habrokat beginnt tatsächlich die Übersetzung des Seminars. Viel Spaß beim Lesen!

Welche Aufgabe Sie auch immer übernehmen, Sie müssen immer drei Schritte durchlaufen:

• 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 Code schreiben, müssen wir:

• entscheiden, was das Programm tun soll;
• bestimmen, wie es seine Aufgabe erfüllen soll;
• Schreiben Sie den entsprechenden Code.

Der letzte Schritt ist natürlich sehr wichtig, aber darüber werde ich heute nicht sprechen. Stattdessen werden wir die ersten beiden besprechen. Jeder Programmierer führt sie aus, bevor er mit der Arbeit beginnt. Sie setzen sich nicht zum Schreiben hin, es sei denn, Sie haben sich entschieden, ob Sie einen Browser oder eine Datenbank schreiben. Eine bestimmte Vorstellung vom Ziel muss vorhanden sein. Und Sie denken auf jeden Fall darüber nach, was genau das Programm tun wird, und schreiben nicht irgendwie in der Hoffnung, dass sich der Code irgendwie in einen Browser verwandelt.

Wie genau geschieht dieses Code-Vordenken? Wie viel Aufwand sollten wir dafür investieren? Es hängt alles davon ab, wie komplex das Problem ist, das wir lösen. Angenommen, wir möchten ein fehlertolerantes verteiltes System schreiben. In diesem Fall sollten wir die Dinge sorgfältig durchdenken, bevor wir uns an die Programmierung machen. Was wäre, wenn wir nur eine ganzzahlige Variable um 1 erhöhen müssten? Auf den ersten Blick ist hier alles trivial und es bedarf keines Nachdenkens, doch dann fällt uns ein, dass es zu einem Überlauf kommen kann. Selbst um zu verstehen, ob ein Problem einfach oder komplex ist, müssen Sie daher zunächst nachdenken.

Wenn Sie sich im Vorfeld über mögliche Problemlösungen Gedanken machen, können Sie Fehler vermeiden. Dies erfordert jedoch, dass Ihr Denken klar ist. Um dies zu erreichen, müssen Sie Ihre Gedanken aufschreiben. Ich mag das Zitat von Dick Guindon sehr: „Wenn du schreibst, zeigt dir die Natur, wie schlampig du denkst.“ Wenn Sie nicht schreiben, denken Sie nur, dass Sie denken. Und Sie müssen Ihre Gedanken in Form von Spezifikationen niederschreiben.

Spezifikationen erfüllen insbesondere bei großen Projekten viele Funktionen. Aber ich möchte nur auf eine davon eingehen: Sie helfen uns, klar zu denken. Klares Denken ist sehr wichtig und ziemlich schwierig, daher brauchen wir hier Hilfe. In welcher Sprache sollten wir Spezifikationen schreiben? Im Allgemeinen ist dies für Programmierer immer die erste Frage: In welcher Sprache werden wir schreiben? Darauf gibt es keine richtige Antwort: Zu vielfältig sind die Probleme, die wir lösen. Für einige ist TLA+ eine Spezifikationssprache, die ich entwickelt habe. Für andere ist es bequemer, Chinesisch zu verwenden. Alles hängt von der Situation ab.

Wichtiger ist eine andere Frage: Wie erreicht man ein klareres Denken? Antwort: Wir müssen wie Wissenschaftler denken. Dies ist eine Denkweise, die sich in den letzten 500 Jahren bewährt hat. In der Wissenschaft erstellen wir mathematische Modelle der Realität. Die Astronomie war vielleicht die erste Wissenschaft im engeren Sinne des Wortes. Im mathematischen Modell der Astronomie erscheinen Himmelskörper als Punkte mit Masse, Position und Impuls, obwohl es sich in Wirklichkeit um äußerst komplexe Objekte mit Bergen und Ozeanen, Gezeiten und Gezeiten handelt. Dieses Modell wurde wie jedes andere entwickelt, um bestimmte Probleme zu lösen. Es eignet sich hervorragend, um zu bestimmen, wohin das Teleskop ausgerichtet werden muss, wenn Sie einen Planeten finden müssen. Wenn Sie jedoch das Wetter auf diesem Planeten vorhersagen möchten, wird dieses Modell nicht funktionieren.

Die Mathematik ermöglicht es uns, die Eigenschaften des Modells zu bestimmen. Und die Wissenschaft zeigt, wie diese Eigenschaften mit der Realität zusammenhängen. Reden wir über unsere Wissenschaft, die Informatik. Die Realität, mit der wir arbeiten, sind Computersysteme unterschiedlicher Art: Prozessoren, Spielekonsolen, Computer, die Programme ausführen und so weiter. Ich werde über die Ausführung eines Programms auf einem Computer sprechen, aber im Großen und Ganzen gelten alle diese Schlussfolgerungen für jedes Computersystem. In unserer Wissenschaft verwenden wir viele verschiedene Modelle: die Turing-Maschine, teilweise geordnete Ereignismengen 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 Benutzeransicht des Programms, dann schreiben wir das High-Level-Diagramm des Programms und schließlich schreiben wir den Code. Während wir den Code schreiben, wird uns klar, dass wir einen Textformatierer schreiben müssen. Auch hier müssen wir drei Probleme lösen: Bestimmen Sie, welchen Text dieses Tool zurückgibt. Wählen Sie einen Algorithmus zur Formatierung aus. Code schreiben. Diese Aufgabe hat eine eigene Unteraufgabe: Einen Bindestrich korrekt in Wörter einfügen. Auch diese Teilaufgabe lösen wir in drei Schritten – wie Sie sehen, wiederholen sie sich auf vielen Ebenen.

Betrachten wir den ersten Schritt genauer: welches Problem das Programm löst. Hier modellieren wir ein Programm meist als Funktion, die einige Eingaben entgegennimmt und einige Ausgaben erzeugt. In der Mathematik wird eine Funktion üblicherweise als eine 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 Definitionsbereich einer solchen Funktion ist die Menge der ersten Elemente jedes Paares, also der natürlichen Zahlen. Um eine Funktion zu definieren, müssen wir ihren Umfang und ihre Formel angeben.

Aber Funktionen in der Mathematik sind nicht dasselbe wie Funktionen in Programmiersprachen. Die Mathematik ist viel einfacher. Da ich keine Zeit für komplexe Beispiele habe, betrachten wir ein einfaches: eine Funktion in C oder eine statische Methode in Java, die den größten gemeinsamen Teiler zweier Ganzzahlen zurückgibt. In der Spezifikation dieser Methode schreiben wir: berechnet GCD(M,N) für Argumente M и NWo GCD(M,N) - eine Funktion, deren Domäne die Menge von Ganzzahlpaaren ist und deren Rückgabewert die größte ganze Zahl ist, durch die teilbar ist M и N. Wie verhält sich dieses Modell zur Realität? Das Modell arbeitet mit Ganzzahlen, während wir in C oder Java ein 32-Bit-Modell haben int. Dieses Modell ermöglicht es uns zu entscheiden, ob der Algorithmus korrekt ist GCD, aber es verhindert keine Überlauffehler. Dies würde ein komplexeres Modell erfordern, für das keine Zeit vorhanden ist.

Lassen Sie uns über die Einschränkungen einer Funktion als Modell sprechen. Einige Programme (z. B. Betriebssysteme) geben für bestimmte Argumente nicht nur einen bestimmten Wert zurück, sondern können kontinuierlich ausgeführt werden. Darüber hinaus eignet sich die Funktion als Modell nicht gut für den zweiten Schritt: die Planung der Lösung des Problems. Schnelle Sortierung und Blasensortierung berechnen dieselbe Funktion, es handelt sich jedoch um völlig unterschiedliche Algorithmen. Um zu beschreiben, wie das Ziel des Programms erreicht wird, verwende ich daher ein anderes Modell, nennen wir es das Standardverhaltensmodell. Das darin enthaltene Programm wird als eine Menge aller zulässigen Verhaltensweisen dargestellt, von denen jedes wiederum eine Folge von Zuständen ist und der Zustand die Zuweisung von Werten zu Variablen ist.

Sehen wir uns an, wie der zweite Schritt für den Euklid-Algorithmus aussehen würde. Wir müssen rechnen GCD(M, N). Wir initialisieren M als xUnd N als y, dann subtrahiere wiederholt die kleinere dieser Variablen von der größeren, bis sie gleich sind. Zum Beispiel, wenn M = 12Und N = 18können wir folgendes Verhalten beschreiben:

[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]

Und wenn die M = 0 и 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 den GCD wirklich für nicht positive Zahlen berechnen? Wenn dies nicht erforderlich ist, müssen Sie lediglich die Spezifikation ändern.

Hier sollten wir einen kleinen Exkurs zur Produktivität machen. Sie wird oft in der Anzahl der pro Tag geschriebenen Codezeilen gemessen. Aber Ihre Arbeit ist viel nützlicher, wenn Sie eine bestimmte Anzahl von Zeilen loswerden, weil Sie weniger Raum für Fehler haben. Und der einfachste Weg, den Code loszuwerden, ist der erste Schritt. Es ist möglich, dass Sie einfach nicht den ganzen Schnickschnack brauchen, den Sie implementieren möchten. Der schnellste Weg, ein Programm zu vereinfachen und Zeit zu sparen, besteht darin, Dinge nicht zu tun, die nicht getan werden sollten. Der zweite Schritt bietet das zweitgrößte Zeiteinsparpotenzial. Wenn Sie die Produktivität anhand der geschriebenen Zeilen messen, werden Sie sich überlegen, wie Sie eine Aufgabe erledigen können weniger produktiv, weil Sie das gleiche Problem mit weniger Code lösen können. Ich kann hier keine genauen Statistiken angeben, da ich keine Möglichkeit habe, die Anzahl der Zeilen zu zählen, die ich nicht geschrieben habe, da ich Zeit mit der Spezifikation, also mit dem ersten und zweiten Schritt, verbracht habe. Und das Experiment kann hier auch nicht aufgebaut werden, denn im Experiment haben wir nicht das Recht, den ersten Schritt abzuschließen, die Aufgabe ist vorgegeben.

Bei informellen Spezifikationen kann es leicht passieren, dass viele Schwierigkeiten übersehen werden. Es ist nichts Schwieriges, strenge Spezifikationen für Funktionen zu schreiben, ich werde darauf nicht näher eingehen. Stattdessen werden wir über das Schreiben starker Spezifikationen für Standardverhalten sprechen. Es gibt einen Satz, der besagt, dass jede Reihe von Verhaltensweisen mithilfe der Sicherheitseigenschaft beschrieben werden kann (Sicherheit) und Überlebenseigenschaften (Lebendigkeit). Sicherheit bedeutet, dass nichts Schlimmes passiert und das Programm keine falsche Antwort gibt. Überlebensfähigkeit bedeutet, dass früher oder später etwas Gutes passieren wird, d. h. das Programm wird früher oder später die richtige Antwort geben. Sicherheit ist in der Regel ein wichtigerer Indikator, Fehler treten hier am häufigsten auf. Um Zeit zu sparen, werde ich daher nicht über die Überlebensfähigkeit sprechen, obwohl sie natürlich auch wichtig ist.

Wir erreichen Sicherheit, indem wir zunächst die Menge der möglichen Anfangszustände vorschreiben. Und zweitens Beziehungen zu allen möglichen nächsten Staaten für jeden Staat. Handeln wir wie Wissenschaftler und definieren wir Zustände mathematisch. Die Menge der Anfangszustände wird durch eine Formel beschrieben, zum Beispiel im Fall des Euklid-Algorithmus: (x = M) ∧ (y = N). Für bestimmte Werte M и N Es gibt nur einen Ausgangszustand. Die Beziehung zum nächsten Zustand wird durch eine Formel beschrieben, in der die Variablen des nächsten Zustands mit einer Primzahl und die Variablen des aktuellen Zustands ohne Primzahl geschrieben werden. Im Fall des Euklid-Algorithmus werden wir uns mit der Disjunktion zweier Formeln befassen, in einer davon x ist der größte Wert und im 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 die kleinere Variable von der größeren subtrahieren. Im zweiten Fall machen wir das Gegenteil.

Kehren wir zum Euklid-Algorithmus zurück. Nehmen wir das noch einmal an M = 12, N = 18. Dies definiert einen einzelnen Anfangszustand, (x = 12) ∧ (y = 18). Anschließend setzen wir diese Werte in die obige Formel ein und erhalten:

Hier ist die einzig mögliche Lösung: x' = 18 - 12 ∧ y' = 12und wir erhalten das Verhalten: [x = 12, y = 18]. Ebenso 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 sind falsch, daher gibt es keinen nächsten Zustand. Wir haben also eine vollständige Spezifikation des zweiten Schritts – wie Sie sehen, ist dies ganz normale Mathematik, wie bei Ingenieuren und Wissenschaftlern, und nicht seltsam, wie in der Informatik.

Diese beiden Formeln können zu einer Formel der zeitlichen Logik zusammengefasst werden. Sie ist elegant und leicht zu erklären, aber jetzt ist keine Zeit für sie. Wir benötigen zeitliche Logik möglicherweise nur für die Lebendigkeitseigenschaft, sie wird nicht für die Sicherheit benötigt. Ich mag zeitliche Logik als solche nicht, es ist keine ganz gewöhnliche Mathematik, aber im Fall von Lebendigkeit ist sie ein notwendiges Übel.

Im Euklid-Algorithmus für jeden Wert x и y einzigartige Werte haben x' и y', die die Beziehung zum nächsten Zustand wahr machen. Mit anderen Worten: Euklids Algorithmus ist deterministisch. Um einen nichtdeterministischen Algorithmus zu modellieren, muss der aktuelle Zustand mehrere mögliche zukünftige Zustände haben und jeder nicht gestrichene Variablenwert muss mehrere gestrichene Variablenwerte haben, sodass die Beziehung zum nächsten Zustand wahr ist. Das ist einfach, aber ich werde jetzt keine Beispiele nennen.

Um ein funktionierendes Werkzeug herzustellen, benötigen Sie formale Mathematik. Wie gestaltet man die Spezifikation formal? Dazu benötigen wir eine formale Sprache, zum Beispiel TLA +. Die Spezifikation des Euklid-Algorithmus würde in dieser Sprache so aussehen:

Ein Gleichheitszeichensymbol mit einem Dreieck bedeutet, dass der Wert links vom Zeichen als gleich dem Wert rechts vom Zeichen definiert ist. Im Wesentlichen handelt es sich bei der Spezifikation um eine Definition, in unserem Fall um zwei Definitionen. Zur Spezifikation in TLA+ müssen Sie Deklarationen und etwas Syntax hinzufügen, wie in der Folie oben. In ASCII würde es so aussehen:

Wie Sie sehen, nichts Kompliziertes. Die Spezifikation für TLA+ kann getestet werden, d. h. alle möglichen Verhaltensweisen in einem kleinen Modell umgehen. In unserem Fall handelt es sich bei diesem Modell um bestimmte Werte M и N. Dies ist eine sehr effiziente und einfache Verifizierungsmethode, die vollständig automatisch abläuft. Es ist auch möglich, formale Wahrheitsbeweise zu schreiben und diese mechanisch zu überprüfen, aber das kostet viel Zeit, deshalb macht das fast niemand.

Der Hauptnachteil von TLA+ besteht darin, dass es sich um Mathematik handelt und Programmierer und Informatiker Angst vor Mathematik haben. Das hört sich auf den ersten Blick wie ein Scherz an, aber leider meine ich es ernst. Mein Kollege hat mir gerade erzählt, wie er versucht hat, mehreren Entwicklern TLA+ zu erklären. Sobald die Formeln auf dem Bildschirm erschienen, wurden sie sofort zu glasigen Augen. Wenn Ihnen TLA+ also Angst macht, können Sie es verwenden PlusCal, es ist eine Art Spielzeugprogrammiersprache. Ein Ausdruck in PlusCal kann jeder TLA+-Ausdruck sein, also im Großen und Ganzen jeder mathematische Ausdruck. Darüber hinaus verfügt PlusCal über eine Syntax für nichtdeterministische Algorithmen. Da PlusCal jeden TLA+-Ausdruck schreiben kann, ist PlusCal viel ausdrucksvoller als jede echte Programmiersprache. Als nächstes wird PlusCal in eine leicht lesbare TLA+-Spezifikation kompiliert. Das bedeutet natürlich nicht, dass die komplexe PlusCal-Spezifikation bei TLA+ zu einer einfachen wird – nur die Übereinstimmung zwischen ihnen ist offensichtlich, es wird keine zusätzliche Komplexität entstehen. Schließlich kann diese Spezifikation durch TLA+-Tools überprüft werden. Alles in allem kann PlusCal helfen, Mathe-Phobie zu überwinden und ist selbst für Programmierer und Informatiker leicht zu verstehen. In der Vergangenheit habe ich einige Zeit (ca. 10 Jahre) Algorithmen dazu veröffentlicht.

Vielleicht wird jemand einwenden, 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. Das ist nicht so. Das schreibt Chris Newcomb, der bei Amazon gearbeitet hat: „Wir haben TLA+ bei zehn großen Projekten eingesetzt, und in jedem Fall hat der Einsatz einen erheblichen Unterschied in der Entwicklung gemacht, weil wir gefährliche Fehler erkennen konnten, bevor wir mit der Produktion begannen, und weil es uns die Einblicke und das Vertrauen gab, die wir brauchten Nehmen Sie aggressive Leistungsoptimierungen vor, ohne die Wahrheit des Programms zu beeinträchtigen.. Man hört oft, dass wir bei der Verwendung formaler Methoden ineffizienten Code erhalten – in der Praxis ist alles genau das Gegenteil. Darüber hinaus besteht die Meinung, dass Manager nicht von der Notwendigkeit formaler Methoden überzeugt werden können, selbst wenn Programmierer von deren Nützlichkeit überzeugt sind. Und Newcomb schreibt: „Manager drängen nun darauf, Spezifikationen für TLA+ zu verfassen und dafür gezielt Zeit einzuplanen“. Wenn Manager also sehen, dass TLA+ funktioniert, akzeptieren sie es gerne. Chris Newcomb hat dies vor etwa sechs Monaten (Oktober 2014) geschrieben, aber mittlerweile wird TLA+ meines Wissens in 14 Projekten verwendet, nicht in 10. Ein weiteres Beispiel ist das Design der XBox 360. Ein Praktikant kam zu Charles Thacker und schrieb eine Spezifikation für das Speichersystem. Dank dieser Spezifikation wurde ein Fehler gefunden, der sonst unbemerkt bleiben würde und aufgrund dessen jede XBox 360 nach vier Stunden Nutzung abstürzte. IBM-Ingenieure bestätigten, dass ihre Tests diesen Fehler nicht gefunden hätten.

Sie können mehr über TLA+ im Internet lesen, aber jetzt sprechen wir über informelle Spezifikationen. Wir müssen selten Programme schreiben, die den kleinsten gemeinsamen Teiler und dergleichen berechnen. Viel häufiger schreiben wir Programme wie das Pretty-Printer-Tool, das ich für TLA+ geschrieben habe. Nach der einfachsten Verarbeitung würde der TLA+-Code so aussehen:

Aber im obigen Beispiel wollte der Benutzer höchstwahrscheinlich, dass die Konjunktion und das Gleichheitszeichen ausgerichtet sind. Die korrekte Formatierung würde also eher so aussehen:

Betrachten Sie ein anderes Beispiel:

Hier hingegen war die Ausrichtung der Gleichheits-, Additions- und Multiplikationszeichen in der Quelle zufällig, sodass die einfachste Verarbeitung völlig ausreicht. Im Allgemeinen gibt es keine exakte mathematische Definition einer korrekten Formatierung, da „richtig“ in diesem Fall „was der Benutzer möchte“ bedeutet und dies mathematisch nicht ermittelt werden kann.

Es scheint, dass die Spezifikation nutzlos ist, wenn wir keine Definition der Wahrheit haben. Aber das ist nicht so. Nur weil wir nicht wissen, was ein Programm tun soll, heißt das nicht, dass wir nicht darüber nachdenken müssen, wie es funktioniert – im Gegenteil, wir müssen uns noch mehr Mühe geben. Die Spezifikation ist hier besonders wichtig. Es ist unmöglich, das optimale Programm für strukturiertes Drucken zu bestimmen, aber das bedeutet nicht, dass wir es überhaupt nicht verwenden sollten, und Code als Bewusstseinsstrom zu schreiben ist keine gute Sache. Am Ende habe ich eine Spezifikation von sechs Regeln mit Definitionen geschrieben in Form von Kommentaren in einer Java-Datei. Hier ist ein Beispiel für eine der Regeln: a left-comment token is LeftComment aligned with its covering token. Diese Regel ist, sagen wir mal, in mathematischem Englisch geschrieben: LeftComment aligned, left-comment и covering token - Begriffe mit Definitionen. So beschreiben Mathematiker Mathematik: Sie schreiben Definitionen von Begriffen und darauf basierend Regeln. Der Vorteil einer solchen Spezifikation besteht darin, dass sechs Regeln viel einfacher zu verstehen und zu debuggen sind als 850 Codezeilen. Ich muss sagen, dass das Schreiben dieser Regeln nicht einfach war, es hat ziemlich viel Zeit gekostet, sie zu debuggen. Speziell zu diesem Zweck habe ich einen Code geschrieben, der meldet, welche Regel verwendet wurde. Dank der Tatsache, dass ich diese sechs Regeln an mehreren Beispielen getestet habe, musste ich nicht 850 Codezeilen debuggen und Fehler waren recht einfach zu finden. Java hat dafür tolle Tools. Wenn ich den Code einfach geschrieben hätte, hätte es viel länger gedauert und die Formatierung wäre von schlechterer Qualität gewesen.

Warum konnte keine formale Spezifikation verwendet werden? Einerseits kommt es hier nicht allzu sehr auf die korrekte Ausführung an. Strukturausdrucke werden bestimmt niemandem gefallen, deshalb musste ich es nicht in allen seltsamen Situationen zum Laufen bringen. Noch wichtiger ist die Tatsache, dass ich nicht über ausreichende Werkzeuge verfügte. Der TLA+-Modellprüfer ist hier nutzlos, daher müsste ich die Beispiele manuell schreiben.

Die obige Spezifikation weist Merkmale auf, die allen Spezifikationen gemeinsam sind. Es ist eine höhere Ebene als der Code. Es kann in jeder Sprache implementiert werden. Alle Tools oder Methoden sind zum Schreiben nutzlos. Kein Programmierkurs wird Ihnen beim Schreiben dieser Spezifikation helfen. Und es gibt keine Tools, die diese Spezifikation überflüssig machen könnten, es sei denn natürlich, Sie schreiben eine Sprache speziell zum Schreiben strukturierter Druckprogramme in TLA+. Schließlich sagt diese Spezifikation nichts darüber aus, wie genau wir den Code schreiben werden, sondern nur, was der Code tut. Wir schreiben die Spezifikation, um uns beim Durchdenken des Problems zu helfen, bevor wir anfangen, über den Code nachzudenken.

Diese Spezifikation weist aber auch Merkmale auf, die sie von anderen Spezifikationen unterscheiden. 95 % der anderen Spezifikationen sind deutlich kürzer und einfacher:

Darüber hinaus handelt es sich bei dieser Spezifikation um eine Reihe von Regeln. Dies ist in der Regel ein Zeichen für eine mangelhafte Spezifikation. Es ist ziemlich schwierig, die Konsequenzen eines Regelwerks zu verstehen, 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 zu Programmen zu sagen, die kontinuierlich laufen. In der Regel arbeiten sie parallel, beispielsweise Betriebssysteme oder verteilte Systeme. Nur sehr wenige Menschen können sie mental oder auf dem Papier verstehen, und ich gehöre nicht dazu, obwohl ich es einmal konnte. Daher benötigen wir Tools, die unsere Arbeit überprüfen – zum Beispiel TLA+ oder PlusCal.

Warum war es notwendig, eine Spezifikation zu schreiben, wenn ich bereits wusste, was genau der Code tun sollte? Tatsächlich dachte ich einfach, ich wüsste es. Darüber hinaus muss ein Außenstehender mit einer Spezifikation nicht mehr in den Code eindringen, um zu verstehen, was er genau tut. Ich habe eine Regel: Es sollte keine allgemeinen Regeln geben. Es gibt natürlich eine Ausnahme von dieser Regel, es ist die einzige allgemeine Regel, die ich befolge: Die Spezifikation dessen, was der Code tut, sollte den Leuten alles sagen, was sie wissen müssen, wenn sie den Code verwenden.

Was genau müssen Programmierer also über das Denken wissen? Für den Anfang gilt das Gleiche wie für alle anderen: Wenn Sie nicht schreiben, kommt es Ihnen nur so vor, als würden Sie denken. Außerdem müssen Sie nachdenken, bevor Sie programmieren, was bedeutet, dass Sie schreiben müssen, bevor Sie programmieren. Die Spezifikation ist das, was wir schreiben, bevor wir mit dem Codieren beginnen. Für jeden Code, der von jedem verwendet oder geändert werden kann, ist eine Spezifikation erforderlich. Und dieser „Jemand“ könnte einen Monat, nachdem er geschrieben wurde, selbst der Autor des Codes sein. Eine 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 soll über den Code geschrieben werden? Sie müssen beschreiben, was es tut, d. h. was für jede Person, die diesen Code verwendet, nützlich sein kann. Manchmal kann es auch erforderlich sein, anzugeben, wie der Code seinen Zweck erfüllt. Wenn wir diese Methode im Zuge der Algorithmen durchlaufen haben, dann nennen wir sie einen Algorithmus. Wenn es etwas Besonderes und Neues ist, dann nennen wir es High-Level-Design. Hier gibt es keinen formalen Unterschied: Bei beiden handelt es sich um ein abstraktes Modell eines Programms.

Wie genau sollte man eine Codespezifikation schreiben? Die 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 dafür schreiben, wie eine Aufgabe implementiert werden soll, können Sie diese in Pseudocode oder mit PlusCal schreiben. Sie müssen lernen, wie man Spezifikationen zu formalen Spezifikationen schreibt. Dadurch erhalten Sie die notwendigen Fähigkeiten, die Ihnen auch bei informellen Aufgaben helfen. Wie lernt man, formale Spezifikationen zu schreiben? Als wir das Programmieren lernten, schrieben wir Programme und debuggten sie dann. Hier ist es dasselbe: Schreiben Sie die Spezifikation, überprüfen Sie sie mit dem Model Checker und beheben Sie die Fehler. 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 geeignet. Der Vorteil von TLA+ besteht darin, dass mathematisches Denken sehr gut vermittelt wird.

Wie verknüpfe ich Spezifikation und Code? Mithilfe von Kommentaren, die mathematische Konzepte und deren Umsetzung verknüpfen. Wenn Sie mit Diagrammen arbeiten, verfügen Sie auf Programmebene über Arrays von Knoten und Arrays von Links. Daher müssen Sie genau schreiben, wie der Graph durch diese Programmierstrukturen implementiert wird.

Es ist zu beachten, dass keiner der oben genannten Punkte auf den eigentlichen Prozess des Codeschreibens zutrifft. Wenn Sie den Code schreiben, also den dritten Schritt ausführen, müssen Sie auch über das Programm nachdenken und es durchdenken. Wenn sich eine Teilaufgabe als komplex oder nicht offensichtlich erweist, müssen Sie eine Spezifikation dafür verfassen. Aber ich rede hier nicht vom Code selbst. Sie können jede Programmiersprache und jede Methodik verwenden, es geht nicht darum. Außerdem entfällt bei keiner der oben genannten Maßnahmen die Notwendigkeit, Code zu testen und zu debuggen. Selbst wenn das abstrakte Modell korrekt geschrieben ist, kann es bei seiner Implementierung zu Fehlern kommen.

Das Schreiben von Spezifikationen ist ein zusätzlicher Schritt im Codierungsprozess. Dadurch lassen sich viele Fehler mit weniger Aufwand abfangen – das wissen wir aus der Erfahrung von Programmierern von Amazon. Mit Spezifikationen wird die Qualität der Programme höher. Warum verzichten wir dann so oft darauf? Weil Schreiben schwer ist. Und Schreiben ist schwierig, denn dafür muss man nachdenken, und Denken ist auch schwierig. Es ist immer einfacher, vorzutäuschen, was man denkt. Hier können Sie eine Analogie zum Laufen ziehen: Je weniger Sie laufen, desto langsamer laufen Sie. Sie müssen Ihre Muskeln trainieren und das Schreiben üben. Brauche Übung.

Möglicherweise ist die Angabe falsch. Möglicherweise haben Sie irgendwo einen Fehler gemacht, die Anforderungen haben sich geändert oder es muss eine Verbesserung vorgenommen werden. Jeder Code, den jemand verwendet, muss geändert werden, sodass die Spezifikation früher oder später nicht mehr mit dem Programm übereinstimmt. Idealerweise müssen Sie in diesem Fall eine neue Spezifikation schreiben und den Code komplett neu schreiben. Wir wissen ganz genau, dass das niemand tut. In der Praxis patchen wir den Code und aktualisieren möglicherweise die Spezifikation. Wenn dies früher oder später passieren muss, warum dann überhaupt Spezifikationen schreiben? Erstens ist für die Person, die Ihren Code bearbeitet, jedes zusätzliche Wort in der Spezifikation Gold wert, und diese Person können durchaus Sie selbst sein. Ich mache mir oft Vorwürfe, dass ich beim Bearbeiten meines Codes nicht genügend Spezifikationen bekomme. Und ich schreibe mehr Spezifikationen als Code. Wenn Sie den Code bearbeiten, muss daher die Spezifikation immer aktualisiert werden. Zweitens wird der Code mit jeder Überarbeitung schlechter, es wird immer schwieriger, ihn zu lesen und zu warten. Dies ist eine Zunahme der Entropie. Wenn Sie jedoch nicht mit einer Spezifikation beginnen, ist jede Zeile, die Sie schreiben, eine Bearbeitung, und der Code ist von Anfang an unhandlich und schwer zu lesen.

Wie gesagt Eisenhower, Keine Schlacht wurde durch Plan gewonnen, und keine Schlacht wurde ohne Plan gewonnen. Und er wusste ein oder zwei Dinge über Schlachten. Es herrscht die Meinung, dass das Verfassen von Spezifikationen Zeitverschwendung sei. Manchmal ist das wahr, und die Aufgabe ist so einfach, dass es keinen Grund zum Nachdenken gibt. Aber Sie sollten immer bedenken, dass Ihnen gesagt wird, dass Sie nicht nachdenken sollen, wenn Sie aufgefordert werden, keine Spezifikationen zu schreiben. Und Sie sollten jedes Mal darüber nachdenken. Das Durchdenken der Aufgabe garantiert nicht, dass Sie keine Fehler machen. Wie wir wissen, hat niemand den Zauberstab erfunden und Programmieren ist eine schwierige Aufgabe. Aber wenn Sie das Problem nicht durchdenken, werden Sie garantiert Fehler machen.

Mehr über TLA+ und PlusCal können Sie auf einer speziellen Website lesen, die Sie von meiner Homepage aus erreichen können Link. Das ist alles für mich, vielen Dank für Ihre Aufmerksamkeit.

Bitte beachten Sie, dass es sich hierbei um eine Übersetzung handelt. Denken Sie beim Schreiben von Kommentaren daran, dass der Autor diese nicht liest. Wenn Sie wirklich mit dem Autor chatten möchten, dann wird er auf der Hydra 2019-Konferenz sein, die vom 11. bis 12. Juli 2019 in St. Petersburg stattfindet. Tickets können erworben werden auf der offiziellen Website.

Source: habr.com