Dies ist ein Übersetzungsartikel . Aber davor eine kleine Einleitung. Wie entstehen Zombies? Jeder war schon einmal in der Situation, dass man einen Freund oder Kollegen auf sein Niveau ziehen möchte, es aber nicht gelingt. Dabei liegt das "Nicht-Gelingen" nicht so sehr an dir, sondern an ihm: Auf der einen Seite der Waage steht ein normales Gehalt, Aufgaben usw., und auf der anderen die Notwendigkeit zu denken. Denken ist unangenehm und schmerzhaft. Er gibt schnell auf und macht weiter mit dem Codieren, ohne sein Gehirn einzuschalten. Du kannst dir vorstellen, wie viel Energie notwendig ist, um die Barriere der erlernten Hilflosigkeit zu überwinden, und deshalb tust du es einfach nicht. So entstehen Zombies, von denen es scheint, dass man sie heilen könnte, aber irgendwie wird sich auch niemand darum kümmern.
Als ich sah, dass (ja, ja, der gleiche Typ aus den Lehrbüchern) und keinen Vortrag, sondern eine Fragestunde macht, war ich etwas skeptisch. Falls es jemand nicht weiß: Leslie ist ein weltweit anerkannter Wissenschaftler, Autor grundlegender Arbeiten in verteiltem Rechnen, und vielleicht kennst du ihn auch aus den Buchstaben La im Wort LaTeX – "Lamport TeX". Ein weiterer beunruhigender Faktor ist seine Forderung: Jeder, der kommt, muss (völlig kostenlos) vorher einige seiner Vorträge anhören, mindestens eine Frage dazu ausdenken und dann erst kommen. Ich wollte sehen, was Lamport zu sagen hat – und es ist großartig! Es ist genau die Sache, die magische Link-Pille zur Heilung der Zombie-Mentalität. Ich warne vor: Der Text könnte bei Liebhabern von überflexiblen Methoden und Gegnern des Testens des Geschriebenen ordentlich Aufregung hervorrufen.
Nach dem Intro beginnt nun die Übersetzung des Seminars. Viel Freude beim Lesen!
Egal, welche Aufgabe Sie übernehmen, Sie müssen immer drei Schritte durchlaufen:
- sich darüber klar werden, welches Ziel Sie erreichen möchten;
- entscheiden, wie genau Sie Ihr Ziel verfolgen werden;
- zu Ihrem Ziel gelangen.
Das gilt auch für das Programmieren. Wenn wir Code schreiben, müssen wir:
- festlegen, was genau das Programm tun soll;
- bestimmen, wie es seine Aufgabe ausführen soll;
- den entsprechenden Code schreiben.
Der letzte Schritt ist natürlich sehr wichtig, aber darüber werde ich heute nicht sprechen. Stattdessen werden wir die ersten beiden diskutieren. Die führt jeder Programmierer aus, bevor er mit der Arbeit beginnt. Man setzt sich nicht einfach hin und schreibt, ohne sich darüber klar zu sein, was genau man schreibt: einen Browser oder eine Datenbank. Eine klare Vorstellung vom Ziel muss unbedingt vorhanden sein. Und man überlegt sich unbedingt, was genau das Programm tun soll, anstatt einfach drauflos zu schreiben in der Hoffnung, dass der Code irgendwie zu einem Browser wird.
Wie genau erfolgt dieses Vorüberlegen beim Codieren? Wie viel Mühe sollten wir dafür aufwenden? Das hängt ganz davon ab, wie komplex das Problem ist, das wir lösen wollen. Angenommen, wir möchten ein fehlertolerantes verteiltes System entwickeln. In diesem Fall sollten wir alles gut durchdenken, bevor wir mit dem Codieren beginnen. Wenn wir jedoch einfach nur eine Ganzzahl um 1 erhöhen müssen? Auf den ersten Blick scheint dies trivial zu sein, und es sind keine Überlegungen erforderlich, aber dann fällt uns ein, dass ein Überlauf auftreten kann. Daher muss man, selbst um zu verstehen, ob es sich um ein einfaches oder komplexes Problem handelt, zunächst nachdenken.
Wenn man mögliche Lösungen für ein Problem im Voraus überlegt, kann man Fehler vermeiden. Um dies zu erreichen, muss das eigene Denken klar sein. Um dies zu erreichen, sollte man seine Gedanken aufschreiben. Mir gefällt das Zitat von Dick Gindin sehr: „Wenn Sie schreiben, zeigt die Natur Ihnen, wie unordentlich Ihr Denken ist.“ Wenn Sie nicht schreiben, haben Sie nur den Eindruck, dass Sie denken. Man sollte seine Gedanken in Form von Spezifikationen festhalten.
Spezifikationen erfüllen viele Funktionen, insbesondere bei großen Projekten. Ich werde jedoch nur über eine davon sprechen: Sie helfen uns, klar zu denken. Klar zu denken ist sehr wichtig und relativ schwierig, daher benötigen wir dazu jede Unterstützung. In welcher Sprache sollten wir Spezifikationen schreiben? Dies ist immer die erste Frage für Programmierer: In welcher Sprache werden wir schreiben? Auf diese Frage gibt es keine eindeutige Antwort: Die Probleme, die wir lösen, sind zu vielfältig. Für einige ist TLA+ hilfreich – das ist eine Spezifikationssprache, die ich entwickelt habe. Für andere ist es bequemer, Chinesisch zu verwenden. Alles hängt von der Situation ab.
Eine wichtigere Frage ist: Wie können wir klareres Denken erreichen? Die Antwort: Wir müssen wie Wissenschaftler denken. Dies ist eine Denkweise, die sich in den letzten 500 Jahren hervorragend bewährt hat. In der Wissenschaft bauen wir mathematische Modelle der Realität. Astronomie war wohl die erste Wissenschaft im strengen Sinne des Wortes. In dem mathematischen Modell, das in der Astronomie verwendet wird, erscheinen Himmelskörper als Punkte mit Masse, Position und Impuls, obwohl sie in Wirklichkeit äußerst komplexe Objekte mit Bergen und Ozeanen, Gezeiten und Strömungen sind. Dieses Modell, wie jedes andere, wurde zur Lösung bestimmter Aufgaben entwickelt. Es eignet sich hervorragend dafür, zu bestimmen, wohin das Teleskop gerichtet werden muss, wenn ein Planet gefunden werden soll. Aber wenn Sie das Wetter auf diesem Planeten vorhersagen wollen, eignet sich dieses Modell nicht.
Die Mathematik ermöglicht es uns, die Eigenschaften des Modells zu bestimmen. Und die Wissenschaft zeigt, wie diese Eigenschaften mit der Realität in Beziehung stehen. Lassen Sie uns über unsere Wissenschaft sprechen: die Informatik. Die Realität, mit der wir arbeiten, sind Computer Systeme aller Art: Prozessoren, Spielkonsolen, Computer, die Programme ausführen, und so weiter. Ich werde über die Ausführung eines Programms auf einem Computer sprechen, aber im Grunde genommen sind alle diese Schlüsse auf jedes Rechensystem anwendbar. In unserer Wissenschaft verwenden wir viele verschiedene Modelle: die Turingmaschine, teilweise geordnete Mengen von Ereignissen und viele andere.
Was ist ein Programm? Es ist jeder Code, der eigenständig betrachtet werden kann. Angenommen, wir müssen einen Browser schreiben. Wir führen drei Aufgaben aus: Wir gestalten die Benutzeroberfläche des Programms, dann schreiben wir ein hochrangiges Programm-Schema und schließlich schreiben wir den Code. Während wir den Code schreiben, erkennen wir, dass wir ein Tool zum Formatieren von Text benötigen. Hier müssen wir erneut drei Aufgaben lösen: Bestimmen, welchen Text dieses Tool zurückgeben soll; einen Algorithmus zum Formatieren auswählen; den Code schreiben. Diese Aufgabe hat ihre eigene Teilaufgabe: korrekt Bindestriche in Wörtern einzufügen. Diese Teilaufgabe lösen wir ebenfalls in drei Schritten — wie wir sehen, wiederholt sich dies auf vielen Ebenen.
Betrachten wir den ersten Schritt genauer: welches Problem das Programm löst. Hier modellieren wir das Programm am häufigsten als Funktion, die bestimmte Eingabedaten erhält und bestimmte Ausgabedaten liefert. In der Mathematik wird eine Funktion normalerweise als geordnetes Paar beschrieben. Zum Beispiel wird die Funktion, die eine Zahl quadriert, für natürliche Zahlen als Menge {, , , , …} beschrieben. Der Definitionsbereich dieser Funktion ist die Menge der ersten Elemente jedes Paares, also die natürlichen Zahlen. Um eine Funktion zu definieren, müssen wir ihren Definitionsbereich und die Formel angeben.
Aber Funktionen in der Mathematik sind nicht dasselbe wie Funktionen in Programmiersprachen. Mathematik ist um ein Vielfaches 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 von zwei ganzen Zahlen zurückgibt. In der Spezifikation dieser Methode schreiben wir: berechnet GCD(M,N) für die Argumente M und NGCD(M,N) — eine Funktion, deren Definitionsbereich die Menge der Paare ganzer Zahlen und deren Rückgabewert die größte ganze Zahl ist, die M und Nteilt. Wie steht diese Modellierung zur Realität? Das Modell arbeitet mit ganzen Zahlen, während wir in C oder Java 32-Bit- inthaben. Dieses Modell lässt uns bestimmen, ob der Algorithmus GCDkorrekt ist, aber es wird keine Überlauf-Fehler verhindern. Dafür wäre ein komplexeres Modell erforderlich, wofür keine Zeit bleibt.
Sprechen wir über die Einschränkungen der Funktion als Modell. Die Arbeit mancher Programme (z.B. Betriebssysteme) beschränkt sich nicht darauf, einen bestimmten Wert für bestimmte Argumente zurückzugeben; sie können kontinuierlich ausgeführt werden. Zudem eignet sich die Funktion als Modell schlecht für den zweiten Schritt: die Planung des Lösungswegs. Quicksort und Bubblesort berechnen dieselbe Funktion, sind jedoch völlig unterschiedliche Algorithmen. Daher verwende ich ein anderes Modell, um den Weg zum Ziel des Programms zu beschreiben; nennen wir es das Standardverhaltensmodell. In diesem wird das Programm als Menge aller zulässigen Verhaltensweisen dargestellt, wobei jede von ihnen wiederum eine Sequenz von Zuständen ist, und ein Zustand ist die Zuweisung von Werten zu Variablen.
Lassen Sie uns sehen, wie der zweite Schritt des Euklidischen Algorithmus aussehen wird. Wir müssen berechnen GCD(M, N). Wir initialisieren M als x, und N als y, dann subtrahieren wir die kleinere dieser Variablen von der größeren, bis sie gleich sind. Wenn zum Beispiel 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? Ноль делится на все числа, поэтому наибольшего делителя в этом случае нет. В этой ситуации нам нужно вернуться к первому шагу и спросить: действительно ли нам нужно вычислять НОД для неположительных чисел? Если в этом нет необходимости, то нужно просто изменить спецификацию.
Hier sollte man einen kleinen Exkurs zur Produktivität machen. Diese wird oft in der Anzahl der pro Tag geschriebenen Codezeilen gemessen. Aber Ihre Arbeit ist viel nützlicher, wenn Sie eine bestimmte Anzahl an Zeilen entfernt haben, da dadurch weniger Platz für Bugs bleibt. Und das Entfernen von Code ist am einfachsten im ersten Schritt. Es ist durchaus möglich, dass Sie die ganzen Raffinessen, die Sie zu implementieren versuchen, einfach nicht benötigen. Der schnellste Weg, ein Programm zu vereinfachen und Zeit zu sparen, ist, Dinge zu vermeiden, die nicht notwendig sind. Der zweite Schritt steht an zweiter Stelle, wenn es um das Sparpotential geht. Wenn Sie Produktivität in der Anzahl geschriebener Zeilen messen, wird ein durchdachter Ansatz zur Lösung einer Aufgabe Sie weniger produktivmachen, da Sie das gleiche Problem mit weniger Code lösen können. Genaue Statistiken kann ich hier nicht angeben, da ich keinen Weg habe, die Anzahl der Zeilen zu zählen, die ich nicht geschrieben habe, weil ich Zeit auf die Spezifikation verwendet habe, also auf die ersten beiden Schritte. Und ein Experiment kann hier auch nicht durchgeführt werden, denn im Experiment dürfen wir den ersten Schritt nicht ausführen, die Aufgabe ist im Voraus festgelegt.
In informellen Spezifikationen ist es leicht, viele Schwierigkeiten zu übersehen. Es ist nicht schwierig, strenge Spezifikationen für Funktionen zu schreiben, darüber werde ich nicht diskutieren. Stattdessen werden wir über das Verfassen strenger Spezifikationen für Standardverhaltensmodelle sprechen. Es gibt einen Satz, der besagt, dass jede Menge von Verhaltensweisen durch Sicherheits- (safety) und Lebensfähigkeit (liveness) beschrieben werden kann.. Sicherheit bedeutet, dass nichts Schlimmes passieren wird, das Programm keine falschen Antworten ausgibt. Robustheit bedeutet, dass irgendwann etwas Gutes passieren wird, d.h. das Programm wird früher oder später die richtige Antwort geben. Im Allgemeinen ist Sicherheit ein wichtigerer Indikator, Fehler treten hier am häufigsten auf. Daher werde ich der Zeitersparnis zuliebe nicht über Robustheit sprechen, obwohl sie natürlich auch wichtig ist.
Wir erreichen Sicherheit, indem wir zunächst eine Vielzahl möglicher Ausgangszustände festlegen. Zum Zweiten definieren wir die Beziehungen zu allen möglichen nachfolgenden Zuständen für jeden Zustand. Lassen Sie uns wissenschaftlich verhalten und die Zustände mathematisch definieren. Die Menge der Ausgangszustände wird durch eine Formel beschrieben, zum Beispiel im Falle des euklidischen Algorithmus: (x = M) ∧ (y = N). Für bestimmte Werte M und N gibt es nur einen Ausgangszustand. Die Beziehung zum nachfolgenden Zustand wird durch eine Formel beschrieben, in der die Variablen des nachfolgenden Zustands mit einem Strich und die des aktuellen Zustands ohne Strich geschrieben werden. Im Falle des euklidischen Algorithmus werden wir mit der Disjunktion von zwei Formeln umgehen, in einer von denen x der größte Wert ist und in der anderen — y:
Im ersten Fall ist der neue Wert von y gleich dem bisherigen Wert von y, und der neue Wert von x erhalten wir, indem wir von der größeren Variablen die kleinere subtrahieren. Im zweiten Fall machen wir es umgekehrt.
Kehren wir zum euklidischen Algorithmus zurück. Angenommen, dass M = 12, N = 18. Dies bestimmt den einzigen Ausgangszustand, (x = 12) ∧ (y = 18). Dann setzen wir diese Werte in die obige Formel ein und erhalten:
Hier gibt es nur eine mögliche Lösung: x' = 18 - 12 ∧ y' = 12, und wir erhalten folgendes 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] werden beide Teile des Ausdrucks falsch sein, folglich gibt es keinen nachfolgenden Zustand. Daher haben wir eine vollständige Spezifikation des zweiten Schrittes — wie gesehen, ist dies ganz gewöhnliche Mathematik, wie bei Ingenieuren und Wissenschaftlern, und nicht seltsam, wie in der Informatik.
Diese beiden Formeln können in eine Formel der temporalen Logik kombiniert werden. Sie ist elegant und leicht zu erklären, aber wir haben gerade keine Zeit dafür. Temporale Logik ist nur für das Liveness-Eigenschaft notwendig, für die Sicherheit ist sie nicht erforderlich. Temporale Logik selbst gefällt nicht, sie ist keine ganz gewöhnliche Mathematik, aber im Fall von Liveness ist sie ein notwendiges Übel.
Im Euklidischen Algorithmus für jeden Wert x und y gibt es eindeutige Werte x' und y', die das Verhältnis zum nächsten Zustand wahr machen. Mit anderen Worten, der Euklidische Algorithmus ist deterministisch. Um einen nicht-deterministischen Algorithmus zu modellieren, muss der aktuelle Zustand mehrere mögliche zukünftige Zustände haben, und jede Variable ohne Strich muss mehrere Werte der Variablen mit Strich haben, bei denen das Verhältnis zum nächsten Zustand wahr ist. Das ist nicht schwierig zu machen, aber ich werde jetzt keine Beispiele bringen.
Um ein funktionierendes Werkzeug zu schaffen, ist formale Mathematik notwendig. Wie macht man die Spezifikation formal? Dafür benötigen wir eine formale Sprache, zum Beispiel, . Die Spezifikation des Euklidischen Algorithmus sieht in dieser Sprache folgendermaßen aus:
Das Symbol des Gleichheitszeichens mit einem Dreieck bedeutet, dass der Wert links vom Zeichen als gleich dem Wert rechts vom Zeichen definiert ist. Im Wesentlichen ist die Spezifikation eine Definition, in unserem Fall zwei Definitionen. Zur Spezifikation in TLA+ müssen Deklarationen und einige Syntax hinzugefügt werden, wie auf der Folie oben. In ASCII würde das so aussehen:
Wie wir sehen, ist nichts kompliziert. Die Spezifikation in TLA+ kann überprüft werden, d.h. alle möglichen Verhaltensweisen in einem kleinen Modell durchlaufen. In unserem Fall wird dieses Modell durch bestimmte Werte M und N. Dies ist eine sehr effektive und einfache Methode der Überprüfung, die vollständig automatisch durchgeführt wird. Außerdem kann man formale Beweise der Wahrhaftigkeit schreiben und mechanisch überprüfen, aber dafür braucht man viel Zeit, weshalb das fast niemand macht.
Der Hauptnachteil von TLA+ ist, dass es Mathematik ist, und Programmierer sowie Informatiker haben Angst vor Mathematik. Auf den ersten Blick mag das wie ein Scherz klingen, aber leider meine ich es ernst. Mein Kollege hat mir gerade erzählt, wie er versucht hat, TLA+ einigen Entwicklern zu erklären. Sobald Formeln auf dem Bildschirm erschienen, hatten sie sofort leere Blicke. Wenn TLA+ also abschreckend wirkt, kann man , eine Art Spiel-Programmiersprache, verwenden. Ein Ausdruck in PlusCal kann beliebig sein, das heißt, im Grunde genommen, jede mathematische Ausdrucksform von TLA+. Darüber hinaus hat PlusCal eine Syntax für nichtdeterministische Algorithmen. Da man in PlusCal jeden TLA+-Ausdruck schreiben kann, ist es wesentlich ausdrucksvoller als jede echte Programmiersprache. Außerdem wird PlusCal in eine leicht verständliche TLA+-Spezifikation kompiliert. Das bedeutet jedoch nicht, dass eine komplexe PlusCal-Spezifikation in eine einfache TLA+-Spezifikation übersetzt wird – die Entsprechung zwischen ihnen ist offensichtlich, zusätzliche Komplexität tritt nicht auf. Schließlich kann diese Spezifikation mit den TLA+-Tools überprüft werden. Insgesamt kann PlusCal helfen, die Angst vor Mathematik zu überwinden; es ist leicht verständlich, selbst für Programmierer und Informatiker. In der Vergangenheit habe ich eine Zeit lang (rund 10 Jahre) Algorithmen damit veröffentlicht.
Vielleicht wird jemand einwenden, dass TLA+ und PlusCal Mathematik sind und Mathematik nur an erfundenen Beispielen funktioniert. In der Praxis benötigt man jedoch eine echte Sprache mit Typen, Prozeduren, Objekten usw. Das stimmt nicht. Hier ist, was Chris Newcomb, der bei Amazon gearbeitet hat, schreibt: „Wir haben TLA+ in zehn großen Projekten eingesetzt, und in jedem Fall hat seine Anwendung erheblich zur Entwicklung beigetragen, weil wir gefährliche Bugs vor dem Produktionsstart identifizieren konnten, und weil es uns das Verständnis und das Vertrauen gegeben hat, das notwendig war für aggressive Leistungsoptimierungen, die die Wahrheit des Programms nicht beeinflussen“. Oft hört man, dass bei der Verwendung formaler Methoden ineffizienter Code entsteht – in der Praxis ist es jedoch genau das Gegenteil. Außerdem gibt es die Meinung, dass es unmöglich ist, das Management von der Notwendigkeit formaler Methoden zu überzeugen, selbst wenn Programmierer von deren Nützlichkeit überzeugt sind. Aber Newcomb schreibt: „Die Manager drängen jetzt, Spezifikationen für TLA+ zu erstellen und räumen dafür extra Zeit ein“. Wenn die Manager also sehen, dass TLA+ funktioniert, nehmen sie es erfreut an. Chris Newcomb hat das vor etwa sechs Monaten (im Oktober 2014) geschrieben, und jetzt, sofern ich weiß, wird TLA+ in 14 Projekten eingesetzt, nicht in 10. Ein weiteres Beispiel betrifft das Entwerfen der Xbox 360. Ein Praktikant kam zu Charles Ticker und schrieb eine Spezifikation für das Speichersystem. Dank dieser Spezifikation wurde ein Fehler gefunden, der sonst nicht bemerkt worden wäre, und der dazu geführt hätte, dass jede Xbox 360 nach vier Stunden Nutzung abstürzt. Ingenieure von IBM bestätigten, dass ihre Tests diesen Fehler nicht entdeckt hätten.
Genaueres über TLA+ können Sie im Internet lesen, und jetzt lasst uns über informelle Spezifikationen sprechen. Es kommt selten vor, dass wir Programme schreiben, die den größten gemeinsamen Teiler berechnen und Ähnliches. Viel häufiger schreiben wir Programme wie ein Tool für die strukturierte Ausgabe (pretty-printer), 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 wahrscheinlich, dass die Zeichen für Konjunktion und Gleichheit ausgerichtet sind. Das richtige Format würde eher so aussehen:
Betrachten wir ein weiteres Beispiel:
Hier war die Ausrichtung der Gleichheits-, Additions- und Multiplikationszeichen im Quelltext zufällig, sodass die einfachste Verarbeitung völlig ausreichend ist. Generell gibt es keine genaue mathematische Definition für das richtige Format, da „richtig“ in diesem Fall bedeutet „so, wie der Benutzer es wünscht“, und das lässt sich mathematisch nicht bestimmen.
Es scheint, dass, wenn wir keine Definition von Wahrheit haben, die Spezifikation nutzlos ist. Das ist jedoch nicht der Fall. Wenn wir nicht wissen, was genau das Programm tun soll, heißt das nicht, dass wir uns nicht mit seiner Funktionsweise auseinandersetzen sollten — im Gegenteil, wir müssen dafür sogar noch mehr Aufwand betreiben. Die Spezifikation ist hier besonders wichtig. Es ist unmöglich, das optimale Programm für die strukturierte Ausgabe zu bestimmen, aber das bedeutet nicht, dass wir es nicht versuchen sollten. Den Code einfach als einen Fluss des Bewusstseins zu schreiben, ist nicht der richtige Weg. Letztendlich habe ich eine Spezifikation in Form von sechs Regeln mit Definitionen geschrieben in Form von Kommentaren in einer Java-Datei. Hier ist ein Beispiel für eine der Regeln: ein linkes Kommentartoken ist LeftComment, das mit seinem übergeordneten Token ausgerichtet ist. Diese Regel ist sozusagen in mathematischem Englisch geschrieben: LeftComment ausgerichtet, linkes Kommentartoken und übergeordnetes Token – Begriffe mit Definitionen. So beschreiben Mathematiker Mathematik: sie schreiben Begriffserklärungen und daraus - Regeln. Der Nutzen einer solchen Spezifikation besteht darin, dass es viel einfacher ist, sechs Regeln zu verstehen und zu überprüfen, als 850 Zeilen Code. Es ist anzumerken, dass es nicht einfach war, diese Regeln zu schreiben; es hat ziemlich viel Zeit gekostet, sie zu debuggen. Speziell für dieses Ziel habe ich einen Code geschrieben, der meldete, welche Regel tatsächlich verwendet wird. Da ich diese sechs Regeln anhand mehrerer Beispiele überprüft habe, musste ich nicht 850 Zeilen Code debuggen, und es war ziemlich einfach, Fehler zu finden. In Java gibt es dafür ausgezeichnete Werkzeuge. Hätte ich einfach Code geschrieben, würde es viel länger gedauert haben, und das Formatieren wäre von schlechterer Qualität gewesen.
Warum konnte keine formale Spezifikation verwendet werden? Einerseits ist die Richtigkeit hier nicht allzu wichtig. Die strukturelle Druckausgabe wird sicherlich jemandem nicht gefallen, sodass ich nicht darauf hinarbeiten musste, dass alles in allen außergewöhnlichen Situationen korrekt funktioniert. Noch wichtiger ist die Tatsache, dass ich keine angemessenen Werkzeuge hatte. Ein TLA+-Modellprüfwerkzeug ist hier nutzlos, sodass ich Beispiele manuell schreiben müsste.
Die angegebene Spezifikation hat Eigenschaften, die für alle Spezifikationen gemeinsam sind. Sie ist eine höhere Ebene als der Code. Sie kann in jeder Sprache realisiert werden. Für ihre Erstellung sind keine Werkzeuge oder Methoden hilfreich. Kein Programmierkurs wird Ihnen helfen, diese Spezifikation zu schreiben. Und es gibt keine Werkzeuge, die diese Spezifikation überflüssig machen könnten, es sei denn, Sie schreiben eine Sprache speziell für das Schreiben von Programmen, die auf struktureller Druckausgabe in TLA+ basieren. Schließlich sagt diese Spezifikation nichts darüber aus, wie genau wir den Code schreiben werden; sie zeigt nur, was dieser Code tut. Wir schreiben eine Spezifikation, um uns zu helfen, das Problem zu durchdenken, bevor wir beginnen, über Code nachzudenken.
Aber diese Spezifikation hat auch Eigenheiten, die sie von anderen Spezifikationen unterscheiden. 95% anderer Spezifikationen sind deutlich kürzer und einfacher:
Diese Spezifikation ist eine Reihe von Regeln. In der Regel ist dies ein Zeichen für eine mangelhafte Spezifikation. Die Konsequenzen eines Regelwerks zu verstehen, ist ziemlich schwierig, und genau deshalb habe ich viel Zeit mit deren Überarbeitung verbracht. Dennoch kann ich in diesem speziellen Fall keinen besseren Weg finden.
Es ist erwähnenswert, einige Worte über Programme zu verlieren, die kontinuierlich laufen. In der Regel arbeiten sie parallel, wie zum Beispiel Betriebssysteme oder verteilte Systeme. Nur sehr wenige können sie im Kopf oder auf Papier nachvollziehen, und ich gehöre nicht dazu, obwohl ich das früher konnte. Daher sind Werkzeuge notwendig, die unsere Arbeit überprüfen – wie zum Beispiel TLA+ oder PlusCal.
Warum war es notwendig, eine Spezifikation zu schreiben, wenn ich doch bereits wusste, was der Code tun sollte? Tatsächlich hatte ich nur den Eindruck, dass ich das wüsste. Darüber hinaus braucht eine externe Person mit einer Spezifikation nicht in den Code einzutauchen, um zu verstehen, was er macht. Ich habe eine Regel: Es sollten keine allgemeinen Regeln existieren. Diese Regel hat natürlich eine Ausnahme, das ist die einzige allgemeine Regel, die ich befolge: Die Spezifikation dessen, was der Code tut, sollte den Menschen alles mitteilen, was sie wissen müssen, um diesen Code zu verwenden.
Was müssen Programmierer also über das Denken wissen? Zunächst einmal das Gleiche wie alle: Wenn du nicht schreibst, denkst du nur, dass du denkst. Darüber hinaus musst du nachdenken, bevor du codierst, was bedeutet, dass du schreiben musst, bevor du codierst. Die Spezifikation ist das, was wir schreiben, bevor wir mit dem Codieren beginnen. Eine Spezifikation ist notwendig für jeden Code, der von jemandem verwendet oder geändert werden kann. Und dieser „jemand“ kann der Autor des Codes selbst einen Monat nach dem Schreiben sein. Spezifikationen sind notwendig für große Programme und Systeme, für Klassen, für Methoden und manchmal sogar für komplexe Abschnitte einzelner Methoden. Was genau muss über den Code geschrieben werden? Es sollte beschrieben werden, was er tut, das heißt, was für jede Person, die diesen Code verwendet, nützlich sein kann. Manchmal kann es auch notwendig sein zu beschreiben, wie genau der Code sein Ziel erreicht. Falls wir diesen Ansatz im Algorithmenkurs behandelt haben, nennen wir es einen Algorithmus. Wenn es sich jedoch um etwas Spezielleres und Neues handelt, nennen wir es hochgradige Entwurf. Formal gibt es keinen Unterschied: Beide sind ein abstraktes Modell eines Programms.
Wie genau sollte die Spezifikation des Codes verfasst werden? Das Wichtigste: Sie sollte auf einer höheren Ebene als der Code selbst sein. Sie sollte Zustände und Verhaltensweisen beschreiben. Sie sollte so strikt sein, wie es die Aufgabe erfordert. Wenn Sie die Spezifikation einer Implementierungsmethode schreiben, kann sie in Pseudocode oder mit Hilfe von PlusCal verfasst werden. Das Schreiben von Spezifikationen sollte auf formalen Spezifikationen basieren. Das wird Ihnen die notwendigen Fähigkeiten geben, die auch bei informellen Spezifikationen helfen. Und wie lernt man, formale Spezifikationen zu schreiben? Als wir Programmieren gelernt haben, haben wir Programme geschrieben und sie dann debuggt. Das ist hier ähnlich: Sie müssen eine Spezifikation schreiben, sie mit einem Modellprüfungswerkzeug überprüfen und Fehler korrigieren. TLA+ ist vielleicht nicht die beste Sprache für formale Spezifikationen, und für Ihre speziellen Bedürfnisse ist wahrscheinlich eine andere Sprache besser geeignet. Der Vorteil von TLA+ ist, dass es hervorragendes mathematisches Denken vermittelt.
Wie verbindet man Spezifikation und Code? Durch Kommentare, die mathematische Konzepte und deren Implementierung verknüpfen. Wenn Sie mit Grafen arbeiten, haben Sie auf Programmebene Arrays von Knoten und Arrays von Verbindungen. Daher müssen Sie beschreiben, wie genau der Graph durch diese Programmierstrukturen realisiert wird.
Es ist zu beachten, dass nichts von dem, was oben gesagt wurde, sich auf den tatsächlichen Prozess des Codierens bezieht. Wenn Sie Code schreiben, also den dritten Schritt ausführen, müssen Sie auch weiter denken und die Programme durchdenken. Wenn sich eine Teilaufgabe als kompliziert oder nicht offensichtlich herausstellt, müssen Sie dafür eine Spezifikation schreiben. Aber über den Code selbst spreche ich hier nicht. Sie können jede Programmiersprache und jede Methodik verwenden, darum geht es hier nicht. Darüber hinaus entbindet nichts von dem, was gesagt wurde, von der Notwendigkeit, den Code zu testen und zu debuggen. Selbst wenn das abstrakte Modell richtig geschrieben ist, können in seiner Umsetzung Fehler vorhanden sein.
Das Schreiben von Spezifikationen ist ein zusätzlicher Schritt im Prozess des Codierens. Durch ihn lassen sich viele Fehler mit weniger Aufwand auffangen — das wissen wir aus der Erfahrung von Programmierern bei Amazon. Mit Spezifikationen wird die Qualität von Programmen besser. Warum kommen wir dann so oft ohne sie aus? Weil das Schreiben schwierig ist. Und es ist schwierig zu schreiben, weil man dafür denken muss, und auch das ist schwierig. Es ist immer einfacher, so zu tun, als ob man denkt. Hier lässt sich eine Analogie zum Laufen ziehen — je weniger Sie laufen, desto langsamer werden Sie. Sie müssen Ihre Muskeln trainieren und im Schreiben üben. Übung ist erforderlich.
Die Spezifikation kann falsch sein. Vielleicht haben Sie irgendwo einen Fehler gemacht, oder die Anforderungen haben sich geändert, oder es war notwendig, eine Verbesserung vorzunehmen. Jeder Code, den jemand verwendet, muss geändert werden, daher wird die Spezifikation irgendwann nicht mehr zur Software passen. Im Idealfall sollte man in einem solchen Fall eine neue Spezifikation schreiben und den Code vollständig neu schreiben. Wir wissen jedoch alle, dass das in der Praxis niemand macht. In der Praxis patchen wir den Code und aktualisieren möglicherweise die Spezifikation. Wenn das zwangsläufig irgendwann geschieht, warum sollte man dann überhaupt Spezifikationen schreiben? Erstens wird für die Person, die Ihren Code überarbeiten wird, jedes überflüssige Wort in der Spezifikation von unschätzbarem Wert sein, und diese Person könnten Sie selbst sein. Oft kritisiere ich mich für unzureichende Spezifikationen, wenn ich meinen Code bearbeite. Ich schreibe mehr Spezifikationen als Code. Daher muss die Spezifikation immer aktualisiert werden, wenn Sie den Code überarbeiten. Zweitens wird der Code mit jeder Bearbeitung schlechter, er wird immer schwieriger zu lesen und zu warten. Das ist ein Anstieg der Entropie. Aber wenn Sie nicht mit einer Spezifikation beginnen, wird jede geschriebene Zeile eine Bearbeitung sein und der Code wird von Anfang an unhandlich und schwer lesbar sein.
Wie Eisenhower sagte , wurde keine Schlacht nach Plan gewonnen, und keine Schlacht wurde ohne Plan gewonnen. Und er wusste einiges über Schlachten. Es gibt die Meinung, dass das Schreiben von Spezifikationen Zeitverschwendung ist. Manchmal ist das tatsächlich der Fall, und die Aufgabe ist so einfach, dass es nichts zu durchdenken gibt. Aber man sollte immer daran denken, dass, wenn Ihnen geraten wird, keine Spezifikationen zu schreiben, Ihnen geraten wird, nicht nachzudenken. Und darüber sollte man jedes Mal nachdenken. Das Durchdenken einer Aufgabe garantiert nicht, dass man keine Fehler macht. Wie wir wissen, hat niemand einen Zauberstab erfunden, und Programmierung ist eine komplexe Aufgabe. Aber wenn Sie die Aufgabe nicht durchdenken, machen Sie garantiert Fehler.
Mehr über TLA+ und PlusCal können Sie auf einer speziellen Website lesen, die Sie über meine Homepage erreichen können . Das wäre es von meiner Seite, danke für Ihre Aufmerksamkeit.
Ich erinnere daran, dass dies eine Übersetzung ist. Wenn Sie Kommentare schreiben, denken Sie daran, dass der Autor diese nicht lesen wird. Wenn Sie wirklich mit dem Autor kommunizieren möchten, wird er auf der Konferenz Hydra 2019 sein, die am 11. und 12. Juli 2019 in Sankt Petersburg stattfindet. Tickets können gekauft werden .
Quelle: habr.com
