Ceci est un article de traduction . Mais avant cela, une petite introduction. Comment se forment les zombies ? Chacun se retrouve dans une situation où il veut tirer un ami ou un collègue à son niveau, mais cela ne fonctionne pas. En fait, le problème ne vient pas tant de vous, mais de lui : d'un côté se trouve un salaire normal, des tâches, etc., et de l'autre, la nécessité de réfléchir. Penser est désagréable et douloureux. Il abandonne rapidement et continue à écrire du code sans vraiment réfléchir. Vous imaginez combien d'efforts il faut déployer pour surmonter le seuil d'impuissance apprise, et au final, on ne le fait tout simplement pas. C'est ainsi que se forment des zombies, que l'on pourrait sembler guérir, mais dont personne ne semble vraiment vouloir s'occuper.
Lorsque j'ai vu que (oui, oui, ce même gars des manuels) et fait non pas une conférence, mais une session de questions-réponses, j'ai été un peu méfiant. Pour info, Leslie est un érudit mondialement connu, auteur d'ouvrages fondamentaux en calcul distribué, et vous pourrez également peut-être le connaître par les lettres La dans le mot LaTeX — « Lamport TeX ». Le deuxième facteur inquiétant est sa demande : chacun qui viendra doit (totalement gratuitement) écouter au préalable quelques-unes de ses conférences, concevoir au moins une question à leur sujet, et seulement alors venir. J'ai décidé de voir ce que Lamport avait à dire — et c'est magnifique ! C'est exactement ce qu'il faut, un lien magique de guérison pour la zombification. Avertissement : le texte saura beaucoup irriter les amateurs de méthodologies ultra-flexibles et ceux qui n'aiment pas tester leur écriture.
Après le brouhaha, commence effectivement la traduction du séminaire. Bonne lecture !
Qu'importe la tâche que vous entreprendrez, vous devez toujours suivre trois étapes :
- déterminer quel objectif vous souhaitez atteindre;
- décider comment vous allez atteindre cet objectif;
- atteindre votre objectif.
Cela s'applique aussi à la programmation. Lorsque nous écrivons du code, nous devons :
- déterminer ce que le programme doit faire;
- définir comment il doit accomplir sa tâche;
- écrire le code correspondant.
Le dernier pas est bien sûr très important, mais je ne vais pas en parler aujourd'hui. À la place, nous allons discuter des deux premières étapes. Chaque programmeur les réalise avant de commencer à travailler. Vous ne vous asseyez pas pour écrire si vous n'avez pas décidé ce que vous allez écrire : un navigateur ou une base de données. Une certaine idée de l'objectif doit toujours être présente. Vous devez aussi réfléchir à ce que le programme va vraiment faire, plutôt que d'écrire au hasard en espérant que le code se transforme tout seul en navigateur.
Comment se déroule exactement cette réflexion préalable sur le code ? Combien d'efforts devrions-nous y consacrer ? Tout dépend de la complexité du problème que nous résolvons. Supposons que nous souhaitons écrire un système distribué résistant aux pannes. Dans ce cas, nous devons réfléchir soigneusement avant de nous mettre au code. Mais si nous devons simplement incrémenter une variable entière de 1 ? À première vue, cela semble trivial et nécessiter peu de réflexion, mais nous nous rappelons ensuite qu'il pourrait y avoir un débordement. Ainsi, même pour déterminer si un problème est simple ou complexe, il faut d'abord réfléchir.
Si vous réfléchissez à l'avance aux solutions possibles au problème, vous pouvez éviter des erreurs. Mais pour cela, il est essentiel que votre pensée soit claire. Pour y parvenir, vous devez écrire vos pensées. J'adore cette citation de Dick Gindin : « Lorsque vous écrivez, la nature vous montre à quel point votre pensée est désordonnée ». Si vous n'écrivez pas, vous avez juste l'impression de penser. Et vous devez formuler vos pensées sous forme de spécifications.
Les spécifications remplissent de nombreuses fonctions, en particulier dans les grands projets. Mais je ne vais parler que de l'une d'entre elles : elles nous aident à penser clairement. Penser clairement est très important et assez difficile, c'est pourquoi nous avons besoin de toute aide possible. Dans quelle langue devrions-nous écrire les spécifications ? C'est presque toujours la première question pour les programmeurs : dans quelle langue allons-nous écrire ? Il n'y a pas une seule bonne réponse : les problèmes que nous résolvons sont trop variés. Pour certains, TLA+ est utile — c'est un langage de spécifications que j'ai développé. Pour d'autres, il est plus pratique d'utiliser le chinois. Tout dépend de la situation.
Une autre question est encore plus importante : comment parvenir à un esprit plus clair ? Réponse : nous devons penser comme des scientifiques. C’est une manière de penser qui a prouvé son efficacité au cours des 500 dernières années. En science, nous construisons des modèles mathématiques de la réalité. L'astronomie a sans doute été la première science au sens strict du terme. Dans le modèle mathématique utilisé en astronomie, les corps célestes sont représentés comme des points dotés de masse, de position et de moment, bien qu'en réalité, ils soient des objets très complexes avec des montagnes et des océans, des marées et des flux. Ce modèle, comme tous les autres, est créé pour résoudre des problèmes spécifiques. Il est excellent pour déterminer où diriger un télescope si l'on veut trouver une planète. Mais si vous voulez prédire le temps sur cette planète, ce modèle ne conviendra pas.
Les mathématiques nous permettent de définir les propriétés d'un modèle. Et la science montre comment ces propriétés se rapportent à la réalité. Parlons de notre science, l'informatique. La réalité avec laquelle nous travaillons est celle des systèmes informatiques de toutes sortes : processeurs, consoles de jeux, ordinateurs exécutant des programmes, etc. Je vais parler de l'exécution de programmes sur un ordinateur, mais fondamentalement, toutes ces conclusions s'appliquent à tout type de système informatique. Dans notre science, nous utilisons de nombreux modèles différents : la machine de Turing, des ensembles d'événements partiellement ordonnés et bien d'autres.
Qu'est-ce qu'un programme ? C'est tout code qui peut être considéré de manière autonome. Supposons que nous devons écrire un navigateur. Nous avons trois tâches à accomplir : concevoir la présentation du programme pour l'utilisateur, puis écrire un schéma de haut niveau du programme, et enfin, écrire du code. Au fur et à mesure que nous écrivons le code, nous réalisons que nous devons créer un outil de formatage de texte. Là encore, nous devons résoudre trois tâches : définir quel texte cet outil renverra, choisir un algorithme de formatage et écrire du code. À ce stade, cette tâche a sa propre sous-tâche : insérer correctement des traits d'union dans les mots. Nous résolvons également cette sous-tâche en trois étapes – comme nous le voyons, elles se répètent à de nombreux niveaux.
Examinons plus en détail la première étape : quelle tâche le programme résout-il. Ici, nous modélisons souvent le programme comme une fonction, qui reçoit certaines données d'entrée et fournit certaines données en sortie. En mathématiques, une fonction est généralement décrite comme un ensemble ordonné de paires. Par exemple, la fonction de mise au carré pour les nombres naturels est décrite comme l'ensemble {, , , , ...}. Le domaine de définition de cette fonction est l'ensemble des premiers éléments de chaque paire, c'est-à-dire les nombres naturels. Pour définir une fonction, nous devons indiquer son domaine de définition et sa formule.
Mais les fonctions en mathématiques ne sont pas les mêmes que les fonctions dans les langages de programmation. Les mathématiques sont bien plus simples. Comme je n'ai pas le temps pour des exemples complexes, prenons un exemple simple : une fonction en C ou une méthode statique en Java qui renvoie le plus grand commun diviseur de deux entiers. Dans la spécification de cette méthode, nous écrirons : calcule GCD(M,N) pour les arguments M et N, où GCD(M,N) — une fonction dont le domaine de définition est l'ensemble des paires d'entiers, et la valeur de retour est le plus grand entier qui divise M et N. Comment ce modèle se rapporte-t-il à la réalité ? Le modèle opère avec des entiers, tandis qu'en C ou en Java, nous avons des int32 bits. Ce modèle nous permet de déterminer si l'algorithmeGCD
est correct, mais il ne préviendra pas les erreurs de dépassement de capacité. Pour cela, un modèle plus complexe serait nécessaire, mais il n'y a pas le temps. Parlons des limitations de la fonction en tant que modèle. Le fonctionnement de certains programmes (par exemple, les systèmes d'exploitation) ne se limite pas à retourner une certaine valeur pour des arguments spécifiques, ils peuvent s'exécuter en continu. De plus, la fonction en tant que modèle convient mal à la deuxième étape : planifier comment résoudre le problème. Le tri rapide et le tri à bulles calculent la même fonction, mais ce sont des algorithmes complètement différents. Par conséquent, pour décrire la façon d'atteindre l'objectif du programme, j'utilise un autre modèle, que nous appellerons modèle de comportement standard. Dans ce modèle, un programme est représenté comme un ensemble de tous les comportements valides, chacun étant à son tour une séquence d'états, et un état est une assignation de valeurs aux variables.
Voyons à quoi ressemblera la deuxième étape de l'algorithme d'Euclide. Nous devons calculer GCD(M, N). Nous initialisons M comment x, et N comment y, puis nous soustrayons l'une des variables de l'autre jusqu'à ce qu'elles soient égales. Par exemple, si M = 12, et N = 18, nous pouvons décrire le comportement suivant :
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Et si M = 0 et N = 0? Ноль делится на все числа, поэтому наибольшего делителя в этом случае нет. В этой ситуации нам нужно вернуться к первому шагу и спросить: действительно ли нам нужно вычислять НОД для неположительных чисел? Если в этом нет необходимости, то нужно просто изменить спецификацию.
Il convient de faire une petite parenthèse sur la productivité. Celle-ci est souvent mesurée par le nombre de lignes de code écrites par jour. Mais votre travail est beaucoup plus précieux si vous parvenez à réduire un certain nombre de lignes, car cela réduit le risque de bugs. Il est également plus facile de se débarrasser du code lors de la première étape. Il est tout à fait possible que vous n'ayez tout simplement pas besoin de toutes ces fonctionnalités que vous essayez de mettre en œuvre. Le moyen le plus rapide de simplifier un programme et de gagner du temps est de ne pas faire les choses qui ne valent pas la peine d'être faites. La deuxième étape arrive en deuxième position en termes de potentiel d'économie de temps. Si vous mesurez la productivité en lignes écrites, alors réfléchir à la manière de réaliser une tâche vous rendra moins productif, car vous serez en mesure de résoudre la même tâche avec moins de code. Je ne peux pas fournir de statistiques précises ici, car je n'ai pas de moyen de calculer le nombre de lignes que je n'ai pas écrites parce que j'ai pris le temps de spécifier, c'est-à-dire lors des premières et deuxièmes étapes. De plus, il est également difficile de faire une expérience ici, car dans une expérience, nous n'avons pas le droit de réaliser la première étape, la tâche étant définie à l'avance.
Dans des spécifications informelles, il est facile de manquer de nombreuses difficultés. Il n'y a rien de compliqué à écrire des spécifications strictes pour des fonctions, je ne vais pas en discuter. À la place, nous allons parler de l'écriture de spécifications strictes pour des modèles de comportement standard. Il existe un théorème selon lequel tout ensemble de comportements peut être décrit à l'aide de propriétés de sécurité (safety) et de propriétés de vivacité (liveness). La sécurité signifie qu'aucun mal ne se produira, le programme ne donnera pas de réponse incorrecte. La résilience signifie qu'à un moment donné, quelque chose de bon se produira, c'est-à-dire que le programme finira par donner la bonne réponse. En général, la sécurité est un indicateur plus important, les erreurs surviennent ici le plus souvent. C'est pourquoi, pour gagner du temps, je ne parlerai pas de résilience, bien qu'elle soit également importante.
Nous atteignons la sécurité en décrivant, d'une part, de nombreux états d'origine possibles. Et, d'autre part, les relations avec tous les états suivants possibles pour chaque état. Agissons comme des scientifiques et définissons mathématiquement les états. L'ensemble des états d'origine est décrit par une formule, par exemple, dans le cas de l'algorithme d'Euclide: (x = M) ∧ (y = N). Pour certaines valeurs M et N il n'existe qu'un seul état d'origine. La relation avec l'état suivant est décrite par une formule, dans laquelle les variables de l'état suivant sont notées avec une apostrophe, tandis que celles de l'état actuel le sont sans. Pour l'algorithme d'Euclide, nous aurons affaire à une disjonction de deux formules, dans l'une desquelles x est la valeur maximale, tandis que dans l'autre, y:
Dans le premier cas, la nouvelle valeur y est égale à l'ancienne valeur y, et la nouvelle valeur x est obtenue en soustrayant la plus petite variable de la plus grande. Dans le second cas, nous faisons le contraire.
Retournons à l'algorithme d'Euclide. Supposons à nouveau que M = 12, N = 18. Cela définit un unique état d'origine, (x = 12) ∧ (y = 18). Ensuite, nous substituons ces valeurs dans la formule ci-dessus et obtenons:
Ici, la seule solution possible est: x' = 18 - 12 ∧ y' = 12, et nous obtenons le comportement: [x = 12, y = 18]. De la même manière, nous pouvons décrire tous les états dans notre comportement: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Dans le dernier état [x = 6, y = 6] les deux parties de l'expression seront fausses, par conséquent, il n'a pas d'état suivant. Ainsi, nous avons une spécification complète de la deuxième étape — comme nous le voyons, c'est une mathématique tout à fait ordinaire, comme chez les ingénieurs et les scientifiques, et non étrange, comme dans l'informatique.
Ces deux formules peuvent être combinées en une seule formule de logique temporelle. Elle est élégante et il n'est pas difficile de l'expliquer, mais il n'y a pas de temps pour cela en ce moment. La logique temporelle peut être nécessaire pour la propriété de vivacité, mais elle n'est pas nécessaire pour la sécurité. La logique temporelle en tant que telle n'est pas appréciée, ce n'est pas tout à fait des mathématiques ordinaires, mais dans le cas de la vivacité, elle est un mal nécessaire.
Dans l'algorithme d'Euclide pour chaque valeur x et y il existe des valeurs uniques x' et y', qui rendent la relation avec l'état suivant vraie. Autrement dit, l'algorithme d'Euclide est déterministe. Pour modéliser un algorithme non déterministe, il faut que l'état actuel ait plusieurs états futurs possibles, et que pour chaque valeur de la variable sans accent, il y ait plusieurs valeurs de la variable avec accent, pour lesquelles la relation avec l'état suivant est vraie. Ce n'est pas difficile à faire, mais je ne vais pas donner d'exemples maintenant.
Pour créer un outil fonctionnel, il faut des mathématiques formelles. Comment rendre la spécification formelle ? Pour cela, nous aurons besoin d'un langage formel, par exemple, . La spécification de l'algorithme d'Euclide dans ce langage ressemblerait à ceci :
Le symbole de l'égalité avec un triangle indique que la valeur à gauche du signe est définie comme étant égale à la valeur à droite du signe. En essence, une spécification est une définition, dans notre cas deux définitions. À la spécification en TLA+, il faut ajouter des déclarations et une certaine syntaxe, comme sur la diapositive ci-dessus. En ASCII, cela ressemblera à ceci :
Comme nous le voyons, rien de compliqué. La spécification en TLA+ peut être vérifiée, c'est-à-dire passer en revue tous les comportements possibles dans un petit modèle. Dans notre cas, ce modèle comprendra des valeurs spécifiques M et N. C'est une méthode de vérification très efficace et simple, qui s'effectue entièrement de manière automatique. De plus, il est possible d'écrire des preuves formelles de vérité et de les vérifier de manière mécanique, mais cela prend beaucoup de temps, c'est pourquoi presque personne ne le fait.
Le principal inconvénient de TLA+ est que c'est des mathématiques, et les programmeurs et les informaticiens ont peur des mathématiques. À première vue, cela ressemble à une blague, mais malheureusement, je le dis très sérieusement. Mon collègue m'a récemment raconté comment il a essayé d'expliquer TLA+ à plusieurs développeurs. Dès que des formules sont apparues à l'écran, leurs yeux se sont tout de suite figés. Donc, si TLA+ fait peur, on peut utiliser , c'est une sorte de langage de programmation simplifié. Une expression en PlusCal peut être n'importe quelle expression TLA+, c'est-à-dire, fondamentalement, n'importe quelle expression mathématique. De plus, PlusCal dispose d'une syntaxe pour les algorithmes non déterministes. Étant donné que PlusCal peut exprimer n'importe quelle expression TLA+, il est nettement plus expressif que tout langage de programmation réel. Ensuite, PlusCal se compile en une spécification TLA+ facilement lisible. Cela ne signifie pas, bien sûr, qu'une spécification complexe en PlusCal se transformera en une simple en TLA+ — il suffit d'avoir une correspondance évidente entre elles, sans complexité supplémentaire. Enfin, cette spécification peut être vérifiée à l'aide des outils TLA+. En résumé, PlusCal peut aider à surmonter la peur des mathématiques, il est facile à comprendre même pour les programmeurs et les informaticiens. Dans le passé, j'ai publié des algorithmes sur PlusCal pendant un certain temps (environ 10 ans).
Peut-être que quelqu'un argumentera que TLA+ et PlusCal sont des mathématiques, et que les mathématiques ne fonctionnent qu'avec des exemples fictifs. En pratique, il faut un vrai langage avec des types, des procédures, des objets, etc. Ce n'est pas vrai. Voici ce que dit Chris Newcomb, qui a travaillé chez Amazon : « Nous avons utilisé TLA+ dans dix grands projets, et dans chaque cas, son utilisation a considérablement contribué au développement, car nous avons pu détecter des bugs dangereux avant qu'ils n'atteignent la production, et parce qu'il nous a donné la compréhension et la confiance nécessaires pour des optimisations de performance agressives, sans nuire à la validité du programme ». On entend souvent dire qu'en utilisant des méthodes formelles nous obtenons du code inefficace — en pratique, c'est tout le contraire. De plus, il est courant de croire qu'il est impossible de convaincre les managers de la nécessité des méthodes formelles, même si les programmeurs sont convaincus de leur utilité. Et Newcomb écrit : «Les managers encouragent désormais activement à rédiger des spécifications en TLA+, en allouant même du temps pour cela». Donc, lorsque les managers constatent que TLA+ fonctionne, ils l'acceptent avec plaisir. Chris Newcomb a écrit cela il y a environ six mois (en octobre 2014), et maintenant, autant que je sache, TLA+ est utilisé dans 14 projets, au lieu de 10. Un autre exemple concerne la conception de la Xbox 360. Un stagiaire est venu voir Charles Tecker et a rédigé une spécification pour le système de mémoire. Grâce à cette spécification, un bug a été identifié, qui autrement serait passé inaperçu, et qui aurait fait planter chaque Xbox 360 après quatre heures d'utilisation. Les ingénieurs d'IBM ont confirmé que leurs tests n'auraient pas détecté ce bug.
Pour en savoir plus sur TLA+, vous pouvez lire sur Internet, mais maintenant parlons des spécifications informelles. Nous sommes rarement amenés à écrire des programmes qui calculent le plus grand commun diviseur et des choses similaires. Bien plus souvent, nous écrivons des programmes comme un outil de mise en forme (pretty-printer), que j'ai créé pour TLA+. Après le traitement le plus simple, le code en TLA+ ressemblerait à ceci :
Mais dans l'exemple donné, l'utilisateur souhaitait probablement que les signes de conjonction et d'égalité soient alignés. Donc, le formatage correct ressemblerait plutôt à ceci :
Considérons un autre exemple :
Ici, au contraire, l'alignement des signes d'égalité, d'addition et de multiplication dans la source était aléatoire, donc le traitement le plus simple suffit amplement. En général, il n'existe pas de définition mathématique précise du formatage correct, car «correct» dans ce cas signifie «tel que le veut l'utilisateur», et cela ne peut pas être défini mathématiquement.
On pourrait penser que si nous n'avons pas de définition de vérité, alors la spécification est inutile. Mais ce n'est pas le cas. Si nous ne savons pas exactement ce que le programme doit faire, cela ne signifie pas que nous ne devons pas réfléchir à son fonctionnement — au contraire, nous devons y consacrer encore plus d'efforts. La spécification est ici particulièrement importante. Il est impossible de définir un programme optimal pour la mise en forme, mais cela ne veut pas dire que nous ne devrions pas nous en occuper du tout, et écrire du code comme un flux de conscience n'est pas la solution. En fin de compte, j'ai rédigé une spécification de six règles avec des définitions sous forme de commentaires dans le fichier Java. Voici un exemple d'une des règles : un jeton left-comment est LeftComment aligné avec son jeton de couverture. Cette règle est écrite dans ce qu'on pourrait appeler de l'anglais mathématique : LeftComment aligné, left-comment et jeton de couverture — des termes avec des définitions. C'est ainsi que les mathématiciens décrivent les mathématiques : ils écrivent des définitions de termes et à partir de celles-ci, des règles. L'avantage d'une telle spécification est qu'il est beaucoup plus facile de comprendre et de déboguer six règles que 850 lignes de code. Il faut dire qu'il n'a pas été facile d'écrire ces règles, cela m'a pris beaucoup de temps pour les déboguer. Spécialement pour ce but, j'ai écrit un code qui indiquait quelle règle était utilisée. Grâce à la vérification de ces six règles sur plusieurs exemples, je n'ai pas eu à déboguer 850 lignes de code, et les bugs se sont révélés relativement faciles à identifier. En Java, il existe d'excellents outils pour cela. Si j'avais simplement écrit le code, cela m'aurait pris beaucoup plus de temps, et le formatage aurait été de moins bonne qualité.
Pourquoi ne pas utiliser de spécification formelle ? D'une part, la correction de l'exécution n'est pas vraiment importante ici. L'impression structurelle ne plaira certainement à personne, donc je n'avais pas besoin d'assurer un fonctionnement correct dans toutes les situations inhabituelles. Encore plus important est le fait que je n'avais pas d'outils adéquats. Un outil de vérification de modèles TLA+ est ici inutile, donc je devrais écrire des exemples manuellement.
La spécification présentée a des caractéristiques communes à toutes les spécifications. Elle est de niveau supérieur au code. Elle peut être réalisée dans n'importe quel langage. Aucun outil ou méthode n'est utile pour son écriture. Aucun cours de programmation ne vous aidera à écrire cette spécification. Et il n'existe pas d'outils qui pourraient rendre cette spécification inutile, sauf si vous écrivez un langage spécifiquement pour rédiger des programmes d'impression structurelle en TLA+. Enfin, cette spécification ne dit rien sur la manière dont nous allons écrire le code, elle indique seulement ce que ce code fait. Nous rédigeons une spécification pour nous aider à réfléchir au problème avant de commencer à penser au code.
Mais cette spécification a aussi des caractéristiques qui la distinguent des autres spécifications. 95 % des autres spécifications sont significativement plus courtes et plus simples :
Ensuite, cette spécification est un ensemble de règles. En général, cela signale une mauvaise spécification. Comprendre les conséquences de cet ensemble de règles est assez difficile, et c'est pourquoi j'ai dû passer beaucoup de temps à les déboguer. Néanmoins, dans ce cas, je n'ai pas trouvé de meilleure façon de faire.
Il vaut la peine de dire quelques mots sur les programmes qui fonctionnent de manière continue. En général, ils fonctionnent en parallèle, comme les systèmes d'exploitation ou les systèmes distribués. Très peu de gens peuvent les comprendre dans leur esprit ou sur papier, et je ne fais pas partie de ce groupe, bien que cela ait déjà été à ma portée. Par conséquent, des outils sont nécessaires pour vérifier notre travail — par exemple, TLA+ ou PlusCal.
Pourquoi avoir écrit une spécification si je savais déjà ce que le code devait faire ? En réalité, je pensais seulement le savoir. De plus, avec une spécification, une personne extérieure n'a plus besoin de plonger dans le code pour comprendre ce qu'il fait. J'ai une règle : il ne devrait y avoir aucune règle générale. Cette règle a bien sûr une exception, c'est la seule règle générale que je suis : la spécification de ce que fait le code doit informer les gens de tout ce qu'ils doivent savoir pour utiliser ce code.
Alors, que doivent savoir les programmeurs sur la pensée ? Pour commencer, la même chose que tout le monde : si tu n'écris pas, tu as juste l'impression de penser. De plus, il faut réfléchir avant de coder, ce qui signifie qu'il faut écrire avant de coder. La spécification est ce que nous écrivons avant de commencer à coder. Une spécification est nécessaire pour tout code qui peut être utilisé ou modifié par quelqu'un d'autre. Et ce « quelqu'un d'autre » pourrait être l'auteur du code lui-même un mois après l'avoir écrit. La spécification est nécessaire pour les grands programmes et systèmes, pour les classes, pour les méthodes et parfois même pour des sections complexes d'une méthode unique. Que faut-il écrire sur le code ? Il faut décrire ce qu'il fait, c'est-à-dire ce qui peut être utile à quiconque utilisant ce code. Il peut parfois être nécessaire d'indiquer comment le code atteint son objectif. Si ce moyen a été vu dans le cours des algorithmes, nous l'appelons un algorithme. Si c'est quelque chose de plus spécifique et nouveau, nous l'appelons conception de haut niveau. Il n'y a pas de différence formelle ici : les deux sont un modèle abstrait du programme.
Comment doit-on écrire une spécification de code ? La principale exigence : elle doit être d'un niveau supérieur au code lui-même. Elle doit décrire les états et les comportements. Elle doit être aussi stricte que l'exige la tâche. Si vous écrivez une spécification sur la manière de réaliser une tâche, elle peut être rédigée en pseudocode ou à l'aide de PlusCal. Il est important d'apprendre à écrire des spécifications en se basant sur des spécifications formelles. Cela vous donnera les compétences nécessaires, y compris pour les spécifications informelles. Mais comment apprendre à écrire des spécifications formelles ? Quand nous avons appris à programmer, nous avons écrit des programmes puis les avons débogués. C'est la même chose ici : il faut écrire une spécification, la vérifier à l'aide d'un outil de vérification de modèle et corriger les erreurs. TLA+ n'est peut-être pas le meilleur langage pour la spécification formelle, et pour vos besoins spécifiques, un autre langage conviendrait probablement mieux. L'avantage de TLA+ est qu'il enseigne très bien la pensée mathématique.
Comment lier la spécification et le code ? Grâce à des commentaires qui relient les concepts mathématiques à leur mise en œuvre. Si vous travaillez avec des graphes, vous aurez des tableaux de nœuds et des tableaux de liens au niveau du programme. Il est donc nécessaire d'expliquer comment le graphe est réellement mis en œuvre par ces structures de programmation.
Il convient de noter que rien de ce qui a été dit précédemment ne se rapporte au processus même d'écriture du code. Lorsque vous écrivez du code, c'est-à-dire que vous exécutez la troisième étape, il est également nécessaire de réfléchir et de conceptualiser le programme. Si une sous-tâche s'avère difficile ou peu claire, il faut rédiger une spécification pour elle. Cependant, je ne parle pas de la code lui-même ici. Vous pouvez utiliser n'importe quel langage de programmation, n'importe quelle méthodologie, ce n'est pas le sujet. De plus, rien de ce qui a été dit précédemment ne vous dispense de tester et déboguer le code. Même si le modèle abstrait est correctement écrit, des bugs peuvent se cacher dans sa mise en œuvre.
La rédaction de spécifications est une étape supplémentaire dans le processus d'écriture du code. Grâce à cela, de nombreuses erreurs peuvent être détectées avec moins d'efforts — nous le savons par l'expérience des programmeurs d'Amazon. Avec des spécifications, la qualité des programmes s'améliore. Alors pourquoi nous passons-nous si souvent sans elles ? Parce que c'est difficile d'écrire. Et écrire est difficile parce qu'il faut penser, et penser est également difficile. Il est toujours plus facile de faire semblant de réfléchir. On peut établir une analogie avec la course — plus vous courez peu, plus vous courez lentement. Il est nécessaire d'entraîner ses muscles et de s'exercer à l'écriture. La pratique est essentielle.
La spécification peut être incorrecte. Vous avez peut-être fait une erreur quelque part, ou les exigences ont pu changer, ou il s'est avéré nécessaire d'apporter des améliorations. Tout code utilisé par quelqu'un doit être modifié, donc tôt ou tard, la spécification ne correspondra plus au programme. Idéalement, dans ce cas, il faudrait écrire une nouvelle spécification et réécrire complètement le code. Nous savons tous que cela n'arrive jamais. En pratique, nous patchons le code et, peut-être, mettons à jour la spécification. Si cela doit inéluctablement arriver tôt ou tard, pourquoi écrire des spécifications ? Premièrement, pour la personne qui devra corriger votre code, chaque mot superflu dans la spécification sera précieux, et cette personne pourrait être vous-même. Je me reproche souvent une spécification insuffisante lorsque je corrige mon code. Et j'écris plus de spécifications que de code. Donc, lorsque vous corrigez du code, il est toujours nécessaire de mettre à jour la spécification. Deuxièmement, à chaque correction, le code devient moins bon, il devient de plus en plus difficile à lire et à maintenir. C'est une montée de l'entropie. Mais si vous ne commencez pas par une spécification, chaque ligne écrite sera une correction, et le code sera encombrant et difficile à lire dès le départ.
Comme disait , aucune bataille n'a été gagnée selon un plan, et aucune bataille n'a été gagnée sans plan. Et il savait quelque chose sur les batailles. Beaucoup pensent que l'écriture de spécifications est une perte de temps. Parfois, c'est effectivement le cas, et la tâche est si simple qu'il n'y a rien à réfléchir. Mais il faut toujours se rappeler que lorsque l'on vous conseille de ne pas écrire de spécifications, cela signifie que l'on vous conseille de ne pas penser. Et cela mérite réflexion à chaque fois. Réfléchir à une tâche ne garantit pas que vous ne ferez pas d'erreurs. Comme nous le savons, personne n'a inventé de baguette magique, et la programmation est un métier complexe. Mais si vous ne réfléchissez pas à la tâche, vous ferez inévitablement des erreurs.
Vous pouvez en savoir plus sur TLA+ et PlusCal sur un site dédié, accessible depuis ma page d'accueil . C'est tout pour moi, merci de votre attention.
Je rappelle que ceci est une traduction. Lorsque vous laisserez des commentaires, souvenez-vous que l'auteur ne les lira pas. Si vous souhaitez vraiment discuter avec l'auteur, il sera à la conférence Hydra 2019, qui se déroulera les 11 et 12 juillet 2019 à Saint-Pétersbourg. Les billets peuvent être achetés .
Source : habr.com
