Dieser Artikel ist eine Übersetzung . Aber vorher ein kurzes Intro. Wie entstehen Zombies? Jeder war schon einmal in einer Situation, in der man einen Freund oder Kollegen auf sein Niveau holen möchte, aber es nicht klappt. Und das „nicht klappt“ liegt nicht so sehr an dir, sondern an ihm: Auf der einen Seite steht ein normales Gehalt, Aufgaben und so weiter, auf der anderen die Notwendigkeit, nachzudenken. Nachdenken ist unangenehm und schmerzhaft. Er gibt schnell auf und schreibt einfach Code, ohne wirklich nachzudenken. Du kannst dir vorstellen, wie viel Kraft es kostet, die Barriere der erlernten Hilflosigkeit zu überwinden, und machst es einfach nicht. So entstehen Zombies, die man vielleicht heilen könnte, aber niemand wird sich wirklich darum kümmern.
Als ich sah, dass (ja, genau der aus den Lehrbüchern) Und macht keine Präsentation, sondern eine Frage-und-Antwort-Runde, war ich ein wenig skeptisch. Nur zur Info, Leslie ist ein weltweit anerkannter Wissenschaftler, Autor grundlegender Arbeiten über verteilte Berechnungen, und vielleicht kennen Sie ihn auch durch die Buchstaben La in LaTeX – «Lamport TeX». Der zweite Punkt, der mich skeptisch machte, war seine Anforderung: Jeder, der kommt, muss (ganz kostenlos) im Voraus ein paar seiner Vorträge anhören, mindestens eine Frage dazu ausdenken und dann erst erscheinen. Ich habe beschlossen, mir anzusehen, was Lamport zu vermitteln hat – und es ist großartig! Es ist genau das, das magische Link-Pillen-Rezept zur Behandlung von Zombie-Denkweisen. Ich warne: Der Text könnte den Freunden übermäßig flexibler Methodologien und den Gegnern von Tests und Code ziemlich sauer aufstoßen.
Nach dem Hub-Break beginnt eigentlich die Übersetzung des Seminars. Viel Spaß beim Lesen!
Egal, welche Aufgabe Sie übernehmen, Sie müssen immer drei Schritte durchlaufen:
- sich entscheiden, welches Ziel Sie erreichen möchten;
- festlegen, wie genau Sie Ihr Ziel erreichen wollen;
- zu Ihrem Ziel gelangen.
Das gilt auch für die Programmierung. Wenn wir Code schreiben, müssen wir:
- festlegen, was genau das Programm tun soll;
- definieren, wie sie ihre Aufgabe genau 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. Diese Schritte müssen jeder Programmierer durchlaufen, bevor er mit der Arbeit beginnt. Sie setzen sich nicht einfach hin und schreiben, ohne entschieden zu haben, was genau Sie erstellen möchten: einen Browser oder eine Datenbank. Eine klare Vorstellung vom Ziel muss unbedingt vorhanden sein. Sie überlegen sich, was das Programm tatsächlich tun wird, anstatt einfach draufloszuschreiben in der Hoffnung, dass der Code sich irgendwie in einen Browser verwandelt.
Wie genau funktioniert die Vorüberlegung beim Programmieren? Wie viel Aufwand sollten wir dafür einplanen? Das hängt stark davon ab, wie komplex das Problem ist, das wir lösen möchten. Nehmen wir an, wir wollen ein ausfallgesichertes verteiltes System erstellen. In diesem Fall sollten wir alles gründlich durchdenken, bevor wir mit dem Programmieren beginnen. Aber was ist, wenn wir einfach eine Ganzzahl um 1 erhöhen möchten? Auf den ersten Blick scheint das trivial und erfordert kein Nachdenken, doch dann erinnert man sich, dass es zu einem Überlauf kommen kann. Daher ist es wichtig, selbst bei vermeintlich einfachen Problemen zuerst Überlegungen anzustellen.
Wenn man mögliche Lösungen im Voraus durchdenkt, kann man Fehler vermeiden. Dafür ist es jedoch erforderlich, dass Ihr Denken klar ist. Um dies zu erreichen, sollten Sie Ihre Gedanken festhalten. Ein Zitat von Dick Hinden gefällt mir sehr gut: "Wenn Sie schreiben, zeigt Ihnen die Natur, wie unordentlich Ihr Denken ist." Wenn Sie nicht schreiben, haben Sie nur den Eindruck, dass Sie denken. Es ist jedoch notwendig, Ihre Gedanken in Form von Spezifikationen festzuhalten.
Spezifikationen erfüllen viele Funktionen, insbesondere in großen Projekten. Ich möchte jedoch nur über eine davon sprechen: Sie helfen uns, klar zu denken. Klar zu denken ist sehr wichtig und ziemlich schwierig, weshalb wir jede Unterstützung brauchen. In welcher Sprache sollten wir die Spezifikationen schreiben? Das ist in der Regel die erste Frage für Programmierer: In welcher Sprache werden wir schreiben? Es gibt keine einzige richtige Antwort darauf, da die Probleme, die wir lösen, zu vielfältig sind. Für einige ist TLA+ nützlich – das ist die von mir entwickelte Spezifikationssprache. Für andere ist Chinesisch praktischer. Es hängt alles von der Situation ab.
Eine wichtigere Frage ist: Wie erreichen wir klareres Denken? Die Antwort: Wir müssen wie Wissenschaftler denken. Dies ist eine Denkweise, die sich in den letzten 500 Jahren bewährt hat. In der Wissenschaft bauen wir mathematische Modelle der Realität auf. Die 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 Gebirgen und Ozeanen, Gezeiten und Strömungen sind. Dieses Modell, wie jedes andere, wurde erstellt, um bestimmte Probleme zu lösen. Es eignet sich hervorragend dafür, zu bestimmen, wohin das Teleskop gerichtet werden muss, um einen Planeten zu finden. Aber wenn Sie das Wetter auf diesem Planeten vorhersagen möchten, eignet sich dieses Modell nicht.
Mathematik ermöglicht uns das Verständnis der Eigenschaften eines Modells. Die Wissenschaft hingegen zeigt, wie diese Eigenschaften mit der Realität verknüpft sind. Lassen Sie uns über unsere Wissenschaft sprechen: Informatik. Die Realität, mit der wir arbeiten, umfasst Computersysteme unterschiedlichster Art: Prozessoren, Spielkonsolen, Computer, die Programme ausführen, und so weiter. Ich werde über die Ausführung von Programmen auf Computern sprechen, doch im Grunde genommen sind alle diese Erkenntnisse auf jede Art von Computersystem anwendbar. In unserer Wissenschaft nutzen wir zahlreiche verschiedene Modelle: die Turing-Maschine, teilweise geordnete Mengen von Ereignissen und viele andere.
Was ist ein Programm? Es handelt sich um jeden Code, der als eigenständig betrachtet werden kann. Angenommen, wir müssen einen Browser schreiben. Dabei haben wir drei Aufgaben: Wir entwerfen zunächst die Benutzeroberfläche des Programms, dann erstellen wir ein hohes Konzept des Programms und schließlich schreiben wir den Code. Während wir den Code schreiben, stellen wir fest, dass wir ein Tool zur Textformatierung benötigen. Hier müssen wir erneut drei Aufgaben lösen: Bestimmen, welchen Text dieses Tool zurückgeben soll; einen Algorithmus für die Formatierung auswählen; und den Code schreiben. Diese Aufgabe hat eine eigene Unteraufgabe: Das korrekte Einfügen von Bindestrichen in Wörter. Diese Unteraufgabe lösen wir ebenfalls in drei Schritten — wie wir sehen, wiederholen sich diese Schritte auf vielen Ebenen.
Lassen Sie uns den ersten Schritt genauer betrachten: Welches Problem löst das Programm? Hier modellieren wir das Programm häufig als Funktion, die bestimmte Eingabewerte erhält und bestimmte Ausgabewerte liefert. In der Mathematik wird eine Funktion normalerweise als geordnetes Paar von Mengen beschrieben. Zum Beispiel wird die Funktion zur Quadrierung von natürlichen Zahlen anhand der 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 deutlich 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 (ggT) von zwei Ganzzahlen zurückgibt. In der Spezifikation dieser Methode würden wir schreiben: berechnet ggT(M,N) für Argumente M und N, wobei ggT(M,N) — eine Funktion, deren Definitionsbereich die Menge der Paare von Ganzzahlen ist, und deren Rückgabewert die größte ganze Zahl ist, durch die teilbar ist M und N. Wie wird dieses Modell mit der Realität in Einklang gebracht? Das Modell arbeitet mit ganzen Zahlen, während wir in C oder Java 32-Bit haben. int. Dieses Modell ermöglicht es uns, zu überprüfen, ob der Algorithmus korrekt ist. GCD, aber es wird keine Überlauf-Fehler verhindern. Dazu wäre ein komplexeres Modell erforderlich, für das jedoch keine Zeit bleibt.
Lassen Sie uns über die Einschränkungen der Funktion als Modell sprechen. Die Funktionsweise mancher Programme (zum Beispiel Betriebssysteme) beschränkt sich nicht darauf, für bestimmte Argumente einen bestimmten Wert zurückzugeben; sie können kontinuierlich ausgeführt werden. Darüber hinaus ist die Funktion als Modell für den zweiten Schritt – die Planung eines Lösungsansatzes – schlecht geeignet. Schnellsortierung und Blasensortierung berechnen zwar die gleiche Funktion, sind jedoch völlig verschiedene Algorithmen. Daher verwende ich zur Beschreibung des Weges zur Zielerreichung der Programme ein anderes Modell, das wir das Standardverhaltensmodell nennen. In diesem Modell wird das Programm als Menge aller zulässigen Verhaltensweisen dargestellt, von denen jede wiederum eine Sequenz von Zuständen ist, wobei ein Zustand eine Zuweisung von Werten an Variablen darstellt.
Lass uns anschauen, 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, und subtrahieren dann wieder die kleinere der beiden Variablen von der größeren, bis sie gleich sind. Zum Beispiel, wenn 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 ein kurzer Hinweis zur Produktivität gemacht werden. Diese wird oft anhand der Anzahl der geschriebenen Codezeilen pro Tag gemessen. Doch Ihre Arbeit ist deutlich wertvoller, wenn Sie eine bestimmte Anzahl an Zeilen entfernt haben, denn damit verringern Sie die Möglichkeit für Bugs. Und das Entfernen von Code ist besonders im ersten Schritt am einfachsten. Es ist gut möglich, dass Sie all die Tricks, die Sie versuchen umzusetzen, gar nicht wirklich brauchen. Der schnellste Weg, um ein Programm zu vereinfachen und Zeit zu sparen, besteht darin, Dinge nicht zu tun, die nicht notwendig sind. Der zweite Schritt hat das zweitgrößte Potenzial zur Zeitersparnis. Wenn Sie Produktivität anhand der Anzahl geschriebener Zeilen messen, wird das Nachdenken über den besten Weg, eine Aufgabe zu erledigen, Sie weniger produktiv machen., da Sie dieselbe Aufgabe mit weniger Code lösen können. Genaue Statistiken kann ich hier nicht angeben, da ich keine Möglichkeit habe, die Anzahl der Zeilen zu zählen, die ich nicht geschrieben habe, weil ich Zeit für die Spezifikation aufgewendet habe, also für die ersten beiden Schritte. Ein Experiment lässt sich hier auch nicht durchführen, da wir im Experiment nicht das Recht haben, den ersten Schritt auszuführen; die Aufgabe ist vorher definiert.
In informellen Spezifikationen lassen sich viele Schwierigkeiten leicht übersehen. Es ist nicht schwierig, strenge Spezifikationen für Funktionen zu schreiben; darüber möchte ich nicht sprechen. Stattdessen werden wir über das Verfassen strenger Spezifikationen für Standardverhaltensmodelle sprechen. Es gibt einen Satz, der besagt, dass jede Menge von Verhaltensweisen durch ein Sicherheitsmerkmal beschrieben werden kann. (safety) und einem Überlebensmerkmal (liveness). Sicherheit bedeutet, dass nichts Schlimmes passiert, das Programm keine falschen Antworten gibt. Robustheit bedeutet, dass irgendwann etwas Gutes passiert, d. h. das Programm früher oder später die richtige Antwort liefert. In der Regel ist Sicherheit ein wichtigerer Indikator, da Fehler hier am häufigsten auftreten. Deshalb werde ich zum Zeitersparen nicht über Robustheit sprechen, obwohl diese natürlich ebenfalls wichtig ist.
Wir erzielen Sicherheit, indem wir erstens viele mögliche Ausgangszustände definieren. Und zweitens die Beziehungen zu allen möglichen Folgezuständen für jeden Zustand festlegen. Lassen Sie uns wie Wissenschaftler verhalten und die Zustände mathematisch definieren. Die Menge der Ausgangszustände wird durch eine Formel beschrieben, zum Beispiel im Fall des euklidischen Algorithmus: (x = M) ∧ (y = N). Für bestimmte Werte M und N gibt es nur einen einzigen Ausgangszustand. Die Beziehung zum Folgezustand wird durch eine Formel beschrieben, in der die Variablen des Folgezustands mit einem Strich und des aktuellen Zustands ohne Strich geschrieben werden. Im Fall des euklidischen Algorithmus haben wir es mit der Disjunktion zweier Formeln zu tun, wobei eine von ihnen x ist der größte Wert, während im zweiten Fall — y:
Im ersten Fall entspricht der neue Wert von y dem alten Wert von y, während wir den neuen Wert von x erhalten, indem wir von der größeren Variablen die kleinere abziehen. Im zweiten Fall machen wir es umgekehrt.
Kehren wir zum euklidischen Algorithmus zurück. Angenommen, wieder, dass M = 12, N = 18. Dies definiert einen einzigartigen Ausgangszustand, (x = 12) ∧ (y = 18). Dann setzen wir diese Werte in die obige Formel ein und erhalten:
Hier ist die einzige mögliche Lösung: x' = 18 - 12 ∧ y' = 12, und wir erhalten das Verhalten: [x = 12, y = 18]. Genauso 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, daher gibt es keinen nächsten Zustand. Somit haben wir eine vollständige Spezifikation des zweiten Schrittes — wie wir sehen, handelt es sich um ganz gewöhnliche Mathematik, wie sie bei Ingenieuren und Wissenschaftlern üblich ist, und nicht um etwas Seltsames, wie es in der Informatik der Fall ist.
Diese beiden Formeln können in eine Formel der temporalen Logik kombiniert werden. Sie ist elegant und leicht zu erklären, aber derzeit gibt es keine Zeit dafür. Temporale Logik ist nur für das Liveness-Property erforderlich, für die Sicherheit ist sie nicht notwendig. An sich mag ich die temporale Logik nicht, da sie keine gewöhnliche Mathematik ist, aber in Bezug auf Liveness ist sie ein notwendiges Übel.
Im Euklidischen Algorithmus für jeden Wert x und y gibt es einzigartige Werte x' und y', die die Beziehung 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 jedes Wert der variablen ohne Strich muss mehrere Werte der variablen mit Strich haben, bei denen die Beziehung zum nächsten Zustand wahr ist. Das ist nicht schwer zu machen, aber ich werde jetzt keine Beispiele bringen.
Um ein funktionierendes Werkzeug zu erstellen, ist formale Mathematik erforderlich. Wie macht man eine formale Spezifikation? Dafür benötigen wir eine formale Sprache, zum Beispiel, . Die Spezifikation des Euklidischen Algorithmus sieht in dieser Sprache wie folgt aus:
Das Symbol des Gleichheitszeichens mit dem Dreieck bedeutet, dass der Wert links vom Zeichen gleich dem Wert rechts vom Zeichen ist. Im Grunde genommen ist die Spezifikation eine Definition, in unserem Fall sind es zwei Definitionen. Zur Spezifikation in TLA+ müssen Deklarationen und eine gewisse Syntax hinzugefügt werden, wie auf der vorherigen Folie. In ASCII würde es so aussehen:
Wie wir sehen, ist das nicht kompliziert. Die Spezifikation in TLA+ kann überprüft werden, das heißt, alle möglichen Verhaltensweisen in einem kleinen Modell durchlaufen werden. In unserem Fall besteht dieses Modell aus bestimmten Werten. M und N. Dies ist ein sehr effektiver und einfacher Prüfmechanismus, der vollständig automatisiert abläuft. Zudem können formale Beweise der Wahrhaftigkeit geschrieben und mechanisch überprüft werden, jedoch erfordert dies viel Zeit, weshalb die meisten dies nicht tun.
Der Hauptnachteil von TLA+ ist, dass es sich um Mathematik handelt und Programmierer sowie Informatiker oft Angst davor haben. Auf den ersten Blick mag das wie ein Scherz klingen, aber leider meine ich das ernst. Mein Kollege erzählte mir gerade, dass er versucht hat, mehreren Entwicklern TLA+ zu erklären. Sobald die Formeln auf dem Bildschirm erschienen, hatten sie sofort leere Blicke. Wenn TLA+ beängstigend ist, kann man auch , es ist eine Art Spielersprache für Programmierung. Ein Ausdruck in PlusCal kann jede beliebige TLA+-Äußerung sein, also im Grunde genommen jeder mathematische Ausdruck. Außerdem gibt es in PlusCal eine Syntax für nichtdeterministische Algorithmen. Da in PlusCal jede TLA+-Äußerung geschrieben werden kann, ist es wesentlich ausdrucksstärker als jede reale Programmiersprache. Darüber hinaus wird PlusCal in eine leicht lesbare TLA+-Spezifikation kompiliert. Das bedeutet jedoch nicht, dass eine komplexe PlusCal-Spezifikation in eine einfache TLA+-Spezifikation umgewandelt wird – die Entsprechung zwischen ihnen ist zwar offensichtlich, aber es entstehen keine zusätzlichen Komplexitäten. Schließlich kann diese Spezifikation mit den TLA+-Werkzeugen überprüft werden. Insgesamt kann PlusCal helfen, die Angst vor Mathematik zu überwinden, und es ist auch für Programmierer und Informatiker leicht verständlich. In der Vergangenheit habe ich etwa 10 Jahre lang Algorithmen damit veröffentlicht.
Vielleicht wird jemand einwenden, dass TLA+ und PlusCal Mathematik sind und Mathematik nur auf erfundenen Beispielen funktioniert. In der Praxis benötigt man jedoch eine echte Sprache mit Typen, Prozeduren, Objekten und so weiter. Das ist nicht der Fall. Hier ist, was Chris Newcomb, der bei Amazon gearbeitet hat, schreibt: „Wir haben TLA+ in zehn großen Projekten verwendet, und in jedem Fall hat dessen Einsatz erheblich zur Entwicklung beigetragen, weil wir gefährliche Bugs identifizieren konnten, bevor sie in die Produktion gingen. Zudem gab es uns das Verständnis und das Vertrauen, die für aggressive Leistungsoptimierungen notwendig sind, ohne die Korrektheit des Programms zu beeinträchtigen.“„Oft hört man, dass die Verwendung formaler Methoden zu ineffizientem Code führt – in der Praxis ist es jedoch genau umgekehrt. Darüber hinaus gibt es die Meinung, dass es unmöglich ist, Manager von der Notwendigkeit formaler Methoden zu überzeugen, selbst wenn die Programmierer von deren Nützlichkeit überzeugt sind. Und Newcomb schreibt:„ „Die Manager drängen nun verstärkt darauf, Spezifikationen in TLA+ zu schreiben, und stellen dafür gezielt Zeit zur Verfügung.“. Wenn Manager sehen, dass TLA+ funktioniert, nehmen sie es erfreut an. Chris Newcomb hat das vor etwa sechs Monaten (im Oktober 2014) geschrieben; mittlerweile, soweit ich weiß, wird TLA+ in 14 Projekten eingesetzt und nicht nur in 10. Ein weiteres Beispiel касается des Designs der Xbox 360. Ein Praktikant kam zu Charles Takker und verfasste eine Spezifikation für das Speichersystem. Dank dieser Spezifikation wurde ein Fehler gefunden, der sonst unbemerkt geblieben wäre, und der dazu geführt hätte, dass jede Xbox 360 nach vier Stunden Nutzung abgestürzt wäre. Ingenieure von IBM bestätigten, dass ihre Tests diesen Fehler nicht entdeckt hätten.
Weitere Informationen zu TLA+ finden Sie im Internet, aber jetzt lassen Sie uns über informelle Spezifikationen sprechen. Selten müssen wir Programme schreiben, die den größten gemeinsamen Teiler berechnen usw. Häufiger schreiben wir Programme wie ein Tool für die strukturierte Ausgabe (pretty-printer), das ich für TLA+ entwickelt habe. Nach der einfachsten Verarbeitung würde der TLA+ Code folgendermaßen aussehen:
Im gegebenen Beispiel wollte der Benutzer wahrscheinlich, dass die Zeichen für Konjunktion und Gleichheit ausgerichtet sind. Das richtige Format würde somit eher so aussehen:
Betrachten wir ein weiteres Beispiel:
Hier war hingegen die Ausrichtung der Gleichheits-, Plus- und Malzeichen im Quelltext zufällig, daher genügt eine einfache Verarbeitung vollkommen. Insgesamt gibt es keine genaue mathematische Definition für das richtige Format, denn "richtig" bedeutet in diesem Fall "so, wie es der Benutzer möchte", was mathematisch nicht bestimmt werden kann.
Es scheint, dass die Spezifikation nutzlos ist, wenn wir keine Definition für die Richtigkeit haben. Das ist jedoch nicht der Fall. Wenn wir nicht wissen, was das Programm genau tun soll, bedeutet das nicht, dass wir uns keine Gedanken über seine Funktionsweise machen sollten – im Gegenteil, wir müssen dafür noch mehr Anstrengungen aufwenden. Die Spezifikation ist hier besonders wichtig. Es ist unmöglich, das optimale Programm für die strukturelle Ausgabe zu definieren, aber das bedeutet nicht, dass wir es nicht angehen sollten. Den Code einfach als Bewusstseinsstrom zu schreiben, ist nicht akzeptabel. Letztendlich habe ich eine Spezifikation mit sechs Regeln und Definitionen geschrieben. in Form von Kommentaren in der Java-Datei. Hier ist ein Beispiel für eine der Regeln: ein left-comment Token ist LeftComment, das mit seinem überdeckenden Token ausgerichtet ist. Diese Regel ist, sagen wir mal, in mathematischem Englisch verfasst: LeftComment ausgerichtet, left-comment und überdeckendes Token — Begriffe mit Definitionen. So beschreiben Mathematiker Mathematik: Sie schreiben Definitionen der Begriffe und darauf basierend die Regeln. Der Vorteil einer solchen Spezifikation ist, dass es wesentlich einfacher ist, sechs Regeln zu verstehen und zu debuggen, als 850 Zeilen Code. Ich muss sagen, das Schreiben dieser Regeln war nicht einfach; es hat ziemlich lange gedauert, sie zu debuggen. Speziell für diesen Zweck habe ich einen Code geschrieben, der angibt, welche Regel genau verwendet wird. Da ich diese sechs Regeln an mehreren Beispielen überprüft habe, musste ich nicht 850 Zeilen Code debuggen, und die Bugs waren ziemlich leicht auffindbar. In Java gibt es dafür ausgezeichnete Tools. Hätte ich einfach nur Code geschrieben, hätte ich erheblich mehr Zeit benötigt, und das Formatierungsergebnis wäre von schlechterer Qualität gewesen.
Warum konnte keine formale Spezifikation verwendet werden? Einerseits ist die Genauigkeit hier nicht allzu wichtig. Ein struktureller Ausdruck wird wohl jemandem nicht gefallen, weshalb ich nicht sicherstellen musste, dass alles in ungewöhnlichen Situationen korrekt funktioniert. Viel wichtiger ist, dass ich nicht über die geeigneten Werkzeuge verfügte. Ein Prüfwerkzeug für TLA+-Modelle ist hier nutzlos, weshalb ich Beispiele manuell schreiben müsste.
Die angegebene Spezifikation weist Merkmale auf, die für alle Spezifikationen typisch sind. Sie ist auf einer höheren Ebene als der Code und kann in jeder Programmiersprache umgesetzt werden. Für ihre Erstellung sind keine spezifischen Werkzeuge oder Methoden erforderlich. 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 entwerfen eine Sprache speziell zur Erstellung von strukturellen Ausdrucksprogrammen in TLA+. Letztendlich sagt diese Spezifikation nichts darüber aus, wie wir den Code tatsächlich schreiben werden; sie gibt lediglich an, was der Code tut. Wir erstellen die Spezifikation, um das Problem zu durchdenken, bevor wir mit dem Codieren beginnen.
Doch diese Spezifikation hat auch Eigenschaften, die sie von anderen Spezifikationen unterscheiden. 95% der anderen Spezifikationen sind erheblich kürzer und einfacher:
Darüber hinaus stellt diese Spezifikation einen Regelkatalog dar. In der Regel ist dies ein Zeichen für eine mangelhafte Spezifikation. Die Folgen eines Regelkatalogs zu verstehen, ist ziemlich schwierig, und genau deshalb habe ich viel Zeit mit deren Überarbeitung verbracht. Dennoch hatte ich in diesem Fall keine bessere Lösung gefunden.
Es ist wichtig, einige Worte über Programme zu verlieren, die kontinuierlich arbeiten. In der Regel laufen sie parallel, wie Betriebssysteme oder verteilte Systeme. Nur sehr wenige können sie im Kopf oder auf Papier durchdringen, und ich gehöre nicht dazu, obwohl ich früher in der Lage dazu war. Daher sind Werkzeuge notwendig, die unsere Arbeit überprüfen — zum Beispiel TLA+ oder PlusCal.
Warum sollte ich eine Spezifikation schreiben, wenn ich doch wusste, was der Code tun sollte? Tatsächlich dachte ich nur, ich wüsste es. Außerdem braucht eine externe Person mit einer Spezifikation nicht in den Code einzutauchen, um zu verstehen, was er tut. Ich habe eine Regel: Es sollte keine allgemeinen Regeln geben. Diese Regel hat jedoch eine Ausnahme, das ist die einzige allgemeine Regel, die ich befolge: Die Spezifikation dessen, was der Code tut, muss den Menschen alles mitteilen, was sie wissen müssen, um diesen Code zu verwenden.
Was müssen Programmierer also über das Denken wissen? Zuallererst gilt für sie dasselbe wie für alle: Wenn du nicht schreibst, scheint es nur so, als würdest du denken. Außerdem ist es wichtig, bevor man codiert, zu denken, was bedeutet, dass man zuerst schreiben muss. Eine Spezifikation ist das, was wir erstellen, bevor wir mit dem Codieren beginnen. Sie ist notwendig für jeden Code, der von jemandem genutzt oder verändert werden kann. Und dieses „jemand“ könnte der Autor des Codes selbst sein, einen Monat nach dessen Erstellung. Spezifikationen sind für große Programme und Systeme erforderlich, für Klassen, für Methoden und manchmal auch für komplexe Abschnitte einer einzelnen Methode. Was genau muss über den Code geschrieben werden? Es sollte beschrieben werden, was der Code tut, also was für jeden, der diesen Code nutzt, nützlich sein könnte. Manchmal kann es auch notwendig sein, anzugeben, wie genau der Code sein Ziel erreicht. Wenn wir diesen Ansatz im Rahmen eines Algorithmus behandelt haben, sprechen wir von einem Algorithmus. Wenn es sich jedoch um etwas Spezielles und Neues handelt, nennen wir es hochgradige Planung. In der Form gibt es hier keinen Unterschied: Beides ist ein abstraktes Modell des Programms.
Wie sollte man eine Codespezifikation schreiben? Das Wichtigste ist, dass sie eine Ebene über dem Code selbst liegt. Sie sollte Zustände und Verhaltensweisen beschreiben. Sie muss so strikt sein, wie es die Aufgabe erfordert. Wenn Sie eine Spezifikation für die Implementierung einer Aufgabe schreiben, kann diese in Pseudocode oder mit PlusCal verfasst werden. Das Schreiben von Spezifikationen sollte mit formalen Spezifikationen geübt werden. Dies vermittelt Ihnen die notwendigen Fähigkeiten, die auch bei informellen Spezifikationen hilfreich sind. Wie lernt man, formale Spezifikationen zu schreiben? Als wir das Programmieren lernten, schrieben wir Programme und debugten sie dann. Genauso hier: Sie müssen eine Spezifikation schreiben, diese mithilfe eines Modellprüfers ü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 ausgezeichnetes mathematisches Denken lehrt.
Wie verbindet man Spezifikation und Code? Durch Kommentare, die mathematische Konzepte mit ihrer Implementierung verknüpfen. Wenn Sie mit Grafen arbeiten, haben Sie auf der Programmebene Arrays von Knoten und Arrays von Verbindungen. Daher müssen Sie beschreiben, wie genau der Graph mit diesen Programmiersprachenstrukturen umgesetzt wird.
Es ist wichtig zu beachten, dass nichts von dem, was oben gesagt wurde, den eigentlichen Prozess des Codierens betrifft. Wenn Sie Code schreiben, also den dritten Schritt ausführen, müssen Sie ebenfalls über die Programmstruktur nachdenken und diese planen. Wenn eine Teilaufgabe komplex oder unklar ist, sollte dafür eine Spezifikation erstellt werden. Aber ich rede hier nicht direkt über den Code. Sie können jede Programmiersprache und jede Methodik verwenden, das ist nicht das Thema. Außerdem entbindet nichts von dem oben Gesagten von der Notwendigkeit, den Code zu testen und zu debuggen. Selbst wenn das abstrakte Modell korrekt geschrieben ist, können in der Implementierung Fehler auftreten.
Das Erstellen von Spezifikationen ist ein zusätzlicher Schritt im Programmierprozess. Damit lassen sich viele Fehler mit geringerer Anstrengung vermeiden – dies wissen wir aus der Erfahrung von Programmierern bei Amazon. Mit Spezifikationen steigt die Qualität der Software. Warum kommen wir also so oft ohne sie aus? Weil Schreiben schwierig ist. Und Schreiben ist schwierig, weil man dafür denken muss, und Denken ist ebenfalls nicht einfach. Es ist immer einfacher, so zu tun, als würde man denken. Man kann dies mit dem Laufen vergleichen – je weniger Sie laufen, desto langsamer werden Sie. Sie müssen Ihre Muskeln trainieren und im Schreiben üben. Übung ist notwendig.
Die Spezifikation könnte fehlerhaft sein. Möglicherweise haben Sie irgendwo einen Fehler gemacht, oder die Anforderungen haben sich geändert, oder es stellte sich heraus, dass Verbesserungen notwendig sind. Jeder Code, den jemand nutzt, muss angepasst werden, daher wird die Spezifikation irgendwann nicht mehr mit dem Programm übereinstimmen. Im Idealfall sollte in einem solchen Fall eine neue Spezifikation geschrieben und der Code komplett neu verfasst werden. Wir wissen jedoch, dass dies in der Praxis selten so gehandhabt wird. Stattdessen patchen wir den Code und aktualisieren möglicherweise die Spezifikation. Wenn dies unumgänglich ist und irgendwann passiert, warum sollten wir dann überhaupt Spezifikationen schreiben? Erstens wird jedes zusätzliche Wort in der Spezifikation für die Person, die Ihren Code bearbeitet, von großem Wert sein – und diese Person könnte durchaus Sie selbst sein. Ich schimpfe oft mit mir selbst über mangelhafte Spezifikationen, wenn ich meinen Code bearbeite. Dabei schreibe ich mehr Spezifikationen als Code. Daher ist es wichtig, beim Bearbeiten des Codes die Spezifikation immer zu aktualisieren. Zweitens wird der Code mit jeder Änderung schlechter, er wird zunehmend schwieriger lesbar und wartbar. Dies ist ein Anstieg der Entropie. Wenn Sie jedoch nicht mit einer Spezifikation beginnen, wird jede geschriebene Zeile eine Änderung 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 eine Menge über Schlachten. Es gibt die Meinung, dass das Schreiben von Spezifikationen Zeitverschwendung ist. Manchmal ist das wirklich der Fall, und die Aufgabe ist so einfach, dass es nichts zu planen gibt. Aber man sollte immer daran denken, dass, wenn man rät, keine Spezifikationen zu schreiben, man rät, nicht nachzudenken. Und darüber sollte man immer 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 Angelegenheit. Aber wenn man die Aufgabe nicht durchdenkt, macht man garantiert Fehler.
Mehr über TLA+ und PlusCal kann man auf der speziellen Webseite lesen, die Sie über meine Homepage erreichen können. Das wäre alles von mir, vielen Dank für Ihre Aufmerksamkeit.
Ich erinnere daran, dass dies eine Übersetzung ist. Wenn Sie Kommentare schreiben, denken Sie daran, dass der Autor sie nicht lesen wird. Wenn Sie wirklich mit dem Autor sprechen möchten, wird er auf der Hydra 2019 Konferenz sein, die am 11. und 12. Juli 2019 in St. Petersburg stattfindet. Tickets sind erhältlich. .
Quelle: habr.com
