Cet article est une traduction . Mais avant elle une petite introduction. Comment se forment les zombies ? Tout le monde s'est retrouvé dans une situation où il voulait mettre un ami ou un collègue à son niveau, mais cela ne fonctionnait pas. Et ce n'est pas tant avec vous qu'avec lui que « ça ne va pas » : d'un côté de l'échelle se trouve un salaire normal, des tâches, etc., et de l'autre, le besoin de réfléchir. Penser est désagréable et douloureux. Il abandonne rapidement et continue à écrire du code sans allumer son cerveau du tout. Vous imaginez combien d'efforts il faut pour surmonter la barrière de l'impuissance apprise, et vous ne le faites tout simplement pas. C'est ainsi que se forment les zombies, qui, semble-t-il, peuvent être guéris, mais il semble que personne ne le fera.
Quand j'ai vu ça (oui, le même camarade des manuels) et ne fait pas un rapport, mais une séance de questions-réponses, j'étais un peu méfiant. Juste au cas où, Leslie est un scientifique de renommée mondiale, l'auteur de travaux fondamentaux en informatique distribuée, et vous pouvez également le connaître par les lettres La dans le mot LaTeX - "Lamport TeX". Le deuxième facteur alarmant est son exigence : tous ceux qui viennent doivent (absolument gratuitement) écouter quelques-uns de ses rapports à l'avance, proposer au moins une question à leur sujet, et venir seulement ensuite. J'ai décidé de voir ce que Lamport diffusait là-bas - et c'est super ! C'est exactement ce truc, la pilule magique pour soigner les zombies. Je vous préviens : dès le texte, les amateurs de méthodologies ultra-flexibles et ceux qui n'aiment pas tester ce qui est écrit peuvent notamment s'épuiser.
Après habrokat, en effet, commence la traduction du séminaire. Bonne lecture!
Quelle que soit la tâche que vous entreprenez, vous devez toujours passer par trois étapes :
- décidez quel objectif vous voulez atteindre;
- décidez comment vous atteindrez votre objectif;
- venez à votre but.
Cela s'applique également à la programmation. Lorsque nous écrivons du code, nous devons :
- décider ce que le programme doit faire ;
- déterminer comment il doit s'acquitter de sa tâche ;
- écrire le code correspondant.
La dernière étape, bien sûr, est très importante, mais je n'en parlerai pas aujourd'hui. Au lieu de cela, nous discuterons des deux premiers. Chaque programmeur les exécute avant de commencer à travailler. Vous ne vous asseyez pas pour écrire à moins que vous n'ayez décidé si vous écrivez un navigateur ou une base de données. Une certaine idée du but doit être présente. Et vous réfléchissez certainement à ce que le programme fera exactement, et n'écrivez pas d'une manière ou d'une autre dans l'espoir que le code se transformera d'une manière ou d'une autre en navigateur.
Comment cette pré-réflexion sur le code se produit-elle exactement ? Combien d'efforts devrions-nous y consacrer ? Tout dépend de la complexité du problème que nous résolvons. Supposons que nous voulions écrire un système distribué tolérant aux pannes. Dans ce cas, nous devrions bien réfléchir avant de nous asseoir pour coder. Et si nous avions juste besoin d'incrémenter une variable entière de 1 ? A première vue, tout est trivial ici, et aucune réflexion n'est nécessaire, mais ensuite on se rappelle qu'un débordement peut se produire. Par conséquent, même pour comprendre si un problème est simple ou complexe, vous devez d'abord réfléchir.
Si vous réfléchissez à l'avance aux solutions possibles au problème, vous pouvez éviter les erreurs. Mais cela nécessite que votre pensée soit claire. Pour y parvenir, vous devez écrire vos pensées. J'aime beaucoup la citation de Dick Guindon : "Lorsque vous écrivez, la nature vous montre à quel point votre pensée est bâclée." Si vous n'écrivez pas, vous pensez seulement que vous pensez. Et vous devez écrire vos pensées sous forme de spécifications.
Les spécifications remplissent de nombreuses fonctions, en particulier dans les grands projets. Mais je ne parlerai que de l'un d'entre eux : ils nous aident à penser clairement. Penser clairement est très important et assez difficile, donc ici nous avons besoin d'aide. Dans quelle langue devrions-nous écrire les spécifications ? En général, c'est toujours la première question pour les programmeurs : dans quel langage allons-nous écrire. Il n'y a pas de bonne réponse : les problèmes que nous résolvons sont trop divers. Pour certains, TLA+ est un langage de spécification que j'ai développé. Pour d'autres, il est plus pratique d'utiliser le chinois. Tout dépend de la situation.
Plus importante est une autre question : comment parvenir à une pensée plus claire ? Réponse : Nous devons penser comme des scientifiques. C'est une façon de penser qui a fait ses preuves au cours des 500 dernières années. En science, nous construisons des modèles mathématiques de la réalité. L'astronomie fut peut-être la première science au sens strict du terme. Dans le modèle mathématique utilisé en astronomie, les corps célestes apparaissent comme des points avec masse, position et impulsion, bien qu'en réalité ce soient des objets extrêmement complexes avec des montagnes et des océans, des marées et des marées. Ce modèle, comme tout autre, a été créé pour résoudre certains problèmes. Il est idéal pour déterminer où pointer le télescope si vous avez besoin de trouver une planète. Mais si vous voulez prédire le temps qu'il fera sur cette planète, ce modèle ne fonctionnera pas.
Les mathématiques nous permettent de déterminer les propriétés du modèle. Et la science montre comment ces propriétés sont liées à la réalité. Parlons de notre science, l'informatique. La réalité avec laquelle nous travaillons est constituée de systèmes informatiques de toutes sortes : processeurs, consoles de jeux, ordinateurs, programmes d'exécution, etc. Je parlerai de l'exécution d'un programme sur un ordinateur, mais dans l'ensemble, toutes ces conclusions s'appliquent à n'importe quel 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 n'importe quel code qui peut être considéré indépendamment. Supposons que nous ayons besoin d'écrire un navigateur. Nous effectuons trois tâches : nous concevons la vue utilisateur du programme, puis nous écrivons le diagramme de haut niveau du programme, et enfin nous écrivons le code. Au fur et à mesure que nous écrivons le code, nous réalisons que nous devons écrire un formateur de texte. Là encore, nous devons résoudre trois problèmes : déterminer quel texte cet outil renverra ; sélectionner un algorithme de formatage ; écrire du code. Cette tâche a sa propre sous-tâche : insérer correctement un trait d'union dans les mots. Nous résolvons également cette sous-tâche en trois étapes - comme vous pouvez le voir, elles sont répétées à plusieurs niveaux.
Considérons plus en détail la première étape: quel problème le programme résout. Ici, nous modélisons le plus souvent un programme comme une fonction qui prend des entrées et produit des sorties. En mathématiques, une fonction est généralement décrite comme un ensemble ordonné de paires. Par exemple, la fonction d'élévation au carré des nombres naturels est décrite comme l'ensemble {<0,0>, <1,1>, <2,4>, <3,9>, …}. Le domaine d'une telle fonction est l'ensemble des premiers éléments de chaque paire, c'est-à-dire les nombres naturels. Pour définir une fonction, nous devons spécifier sa portée et sa formule.
Mais les fonctions en mathématiques ne sont pas les mêmes que les fonctions dans les langages de programmation. Le calcul est beaucoup plus facile. Comme je n'ai pas le temps pour des exemples complexes, considérons un exemple simple : une fonction en C ou une méthode statique en Java qui renvoie le plus grand diviseur commun de deux entiers. Dans la spécification de cette méthode, nous écrirons : calcule GCD(M,N) pour les arguments M и NOù GCD(M,N) - une fonction dont le domaine est l'ensemble des paires d'entiers, et la valeur de retour est le plus grand entier divisible par M и N. Comment ce modèle se rapporte-t-il à la réalité ? Le modèle fonctionne sur des entiers, alors qu'en C ou Java nous avons un 32 bits int. Ce modèle nous permet de décider si l'algorithme est correct GCD, mais cela n'empêchera pas les erreurs de débordement. Cela nécessiterait un modèle plus complexe, pour lequel le temps manque.
Parlons des limites d'une fonction en tant que modèle. Certains programmes (tels que les systèmes d'exploitation) ne se contentent pas de renvoyer une certaine valeur pour certains arguments, ils peuvent s'exécuter en continu. De plus, la fonction en tant que modèle n'est pas bien adaptée à 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 comment l'objectif du programme est atteint, j'utilise un modèle différent, appelons-le le modèle comportemental standard. Le programme qu'il contient est représenté comme un ensemble de tous les comportements autorisés, chacun étant à son tour une séquence d'états, et l'état est l'attribution de valeurs à des variables.
Voyons à quoi ressemblerait la deuxième étape de l'algorithme d'Euclide. Nous devons calculer GCD(M, N). Nous initialisons M comme xEt N comme y, puis soustrayez à plusieurs reprises la plus petite de ces variables de la plus grande jusqu'à ce qu'elles soient égales. Par exemple, si M = 12Et N = 18, nous pouvons décrire le comportement suivant :
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Et si l' M = 0 и N = 0? Zéro est divisible par tous les nombres, il n'y a donc pas de plus grand diviseur dans ce cas. Dans cette situation, nous devons revenir à la première étape et nous demander : avons-nous vraiment besoin de calculer le PGCD pour les nombres non positifs ? Si cela n'est pas nécessaire, il vous suffit de modifier la spécification.
Ici, nous devrions faire une petite digression sur la productivité. Il est souvent mesuré en nombre de lignes de code écrites par jour. Mais votre travail est beaucoup plus utile si vous vous débarrassez d'un certain nombre de lignes, car vous avez moins de place pour les bogues. Et le moyen le plus simple de se débarrasser du code est à la première étape. Il est tout à fait possible que vous n'ayez tout simplement pas besoin de toutes les cloches et de tous les sifflets 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 des choses qui ne devraient pas être faites. La deuxième étape est le deuxième potentiel de gain de temps. Si vous mesurez la productivité en termes de lignes écrites, alors réfléchir à la façon d'accomplir une tâche vous fera moins productif, car vous pouvez résoudre le même problème avec moins de code. Je ne peux pas donner de statistiques exactes ici, car je n'ai aucun moyen de compter le nombre de lignes que je n'ai pas écrites du fait que j'ai passé du temps sur la spécification, c'est-à-dire sur les première et deuxième étapes. Et l'expérience ne peut pas non plus être mise en place ici, car dans l'expérience nous n'avons pas le droit de terminer la première étape, la tâche est prédéterminée.
Il est facile de négliger de nombreuses difficultés dans les spécifications informelles. Il n'y a rien de difficile à écrire des spécifications strictes pour les fonctions, je n'en discuterai pas. Au lieu de cela, nous parlerons de la rédaction de spécifications solides pour les comportements standard. Il existe un théorème qui dit que tout ensemble de comportements peut être décrit à l'aide de la propriété de sécurité (sécurité) et propriétés de survie (vivacité). La sécurité signifie que rien de mal ne se passera, le programme ne donnera pas de réponse incorrecte. La capacité de survie signifie que tôt ou tard, quelque chose de bien se produira, c'est-à-dire que le programme donnera la bonne réponse tôt ou tard. En règle générale, la sécurité est un indicateur plus important, les erreurs se produisent le plus souvent ici. Par conséquent, pour gagner du temps, je ne parlerai pas de capacité de survie, même si cela est bien sûr également important.
Nous obtenons la sécurité en prescrivant, premièrement, l'ensemble des états initiaux possibles. Et deuxièmement, 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 initiaux est décrit par une formule, par exemple, dans le cas de l'algorithme d'Euclide : (x = M) ∧ (y = N). Pour certaines valeurs M и N il n'y a qu'un seul état initial. La relation avec l'état suivant est décrite par une formule dans laquelle les variables de l'état suivant sont écrites avec un prime, et les variables de l'état courant sont écrites sans prime. Dans le cas de l'algorithme d'Euclide, nous traiterons de la disjonction de deux formules, dans l'une desquelles x est la plus grande valeur, et dans la seconde - y:
Dans le premier cas, la nouvelle valeur de y est égale à la valeur précédente de y, et nous obtenons la nouvelle valeur de x en soustrayant la plus petite variable de la plus grande variable. Dans le second cas, on fait l'inverse.
Revenons à l'algorithme d'Euclide. Supposons à nouveau que M = 12, N = 18. Cela définit un seul état initial, (x = 12) ∧ (y = 18). Nous insérons ensuite ces valeurs dans la formule ci-dessus et obtenons :
Voici la seule solution possible : x' = 18 - 12 ∧ y' = 12et on obtient le comportement : [x = 12, y = 18]. De même, nous pouvons décrire tous les états de notre comportement : [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
En dernier état [x = 6, y = 6] les deux parties de l'expression seront fausses, donc elle n'a pas d'état suivant. Donc, nous avons une spécification complète de la deuxième étape - comme vous pouvez le voir, ce sont des mathématiques tout à fait ordinaires, comme chez les ingénieurs et les scientifiques, et pas étranges, comme en informatique.
Ces deux formules peuvent être combinées en une seule formule de logique temporelle. Elle est élégante et facile à expliquer, mais il n'y a pas de temps pour elle maintenant. Nous pouvons avoir besoin de logique temporelle uniquement pour la propriété de vivacité, elle n'est pas nécessaire pour la sécurité. Je n'aime pas la logique temporelle en tant que telle, ce ne sont pas des mathématiques tout à fait ordinaires, mais dans le cas de la vivacité, c'est un mal nécessaire.
Dans l'algorithme d'Euclide, pour chaque valeur x и y avoir des valeurs uniques x' и y', ce qui rend vraie la relation avec l'état suivant. En d'autres termes, l'algorithme d'Euclide est déterministe. Pour modéliser un algorithme non déterministe, l'état actuel doit avoir plusieurs états futurs possibles, et que chaque valeur de variable non amorcée a plusieurs valeurs de variables amorcées de sorte que la relation avec l'état suivant soit vraie. C'est facile à faire, mais je ne donnerai pas d'exemples maintenant.
Pour fabriquer un outil de travail, il faut des mathématiques formelles. Comment formaliser le cahier des charges ? Pour ce faire, nous avons besoin d'un langage formel, par exemple, . La spécification de l'algorithme d'Euclide ressemblerait à ceci dans ce langage :
Un symbole de signe égal avec un triangle signifie que la valeur à gauche du signe est définie comme étant égale à la valeur à droite du signe. Essentiellement, la spécification est une définition, dans notre cas deux définitions. À la spécification dans TLA+, vous devez ajouter des déclarations et une certaine syntaxe, comme dans la diapositive ci-dessus. En ASCII, cela ressemblerait à ceci :
Comme vous pouvez le voir, rien de compliqué. La spécification pour TLA+ peut être testée, c'est-à-dire contourner tous les comportements possibles dans un petit modèle. Dans notre cas, ce modèle sera certaines valeurs M и N. Il s'agit d'une méthode de vérification très efficace et simple qui est entièrement automatique. Il est également possible d'écrire des preuves de vérité formelles et de les vérifier mécaniquement, mais cela prend beaucoup de temps, donc presque personne ne le fait.
Le principal inconvénient de TLA+ est qu'il s'agit de mathématiques, et que les programmeurs et les informaticiens ont peur des mathématiques. À première vue, cela ressemble à une blague, mais, malheureusement, je le pense très sérieusement. Mon collègue vient de me raconter comment il a tenté d'expliquer TLA+ à plusieurs développeurs. Dès que les formules sont apparues sur l'écran, elles sont immédiatement devenues des yeux vitreux. Donc si TLA+ vous fait peur, vous pouvez utiliser , c'est une sorte de langage de programmation jouet. Une expression dans PlusCal peut être n'importe quelle expression TLA+, c'est-à-dire, en gros, n'importe quelle expression mathématique. De plus, PlusCal a une syntaxe pour les algorithmes non déterministes. Étant donné que PlusCal peut écrire n'importe quelle expression TLA+, PlusCal est beaucoup plus expressif que n'importe quel langage de programmation réel. Ensuite, PlusCal est compilé dans une spécification TLA+ facilement lisible. Cela ne signifie pas, bien sûr, que la spécification complexe PlusCal se transformera en une spécification simple sur TLA + - seule la correspondance entre elles est évidente, il n'y aura pas de complexité supplémentaire. Enfin, cette spécification peut être vérifiée par les outils TLA+. Dans l'ensemble, PlusCal peut aider à surmonter la phobie des mathématiques et est facile à comprendre, même pour les programmeurs et les informaticiens. Dans le passé, j'ai publié des algorithmes dessus pendant un certain temps (environ 10 ans).
Peut-être que quelqu'un objectera que TLA + et PlusCal sont des mathématiques, et que les mathématiques ne fonctionnent que sur des exemples inventés. En pratique, il faut un vrai langage avec des types, des procédures, des objets, etc. C'est faux. Voici ce que Chris Newcomb, qui travaillait chez Amazon, écrit : "Nous avons utilisé TLA+ sur dix projets majeurs, et dans chaque cas, son utilisation a fait une différence significative pour le développement, car nous avons pu détecter des bogues dangereux avant d'entrer en production, et parce qu'il nous a donné la perspicacité et la confiance dont nous avions besoin pour faire des optimisations de performances agressives sans affecter la vérité du programme". Vous pouvez souvent entendre dire qu'en utilisant des méthodes formelles, nous obtenons un code inefficace - en pratique, tout est exactement le contraire. De plus, il existe une opinion selon laquelle les gestionnaires ne peuvent pas être convaincus de la nécessité des méthodes formelles, même si les programmeurs sont convaincus de leur utilité. Et Newcomb écrit : "Les managers poussent maintenant fort pour écrire des spécifications pour TLA +, et allouer spécifiquement du temps pour cela". Ainsi, lorsque les managers voient que TLA+ fonctionne, ils sont heureux de l'accepter. Chris Newcomb a écrit ceci il y a environ six mois (octobre 2014), mais maintenant, pour autant que je sache, TLA+ est utilisé dans 14 projets, et non 10. Un autre exemple est dans la conception de la XBox 360. Un stagiaire est venu voir Charles Thacker et a écrit la spécification pour le système de mémoire. Grâce à cette spécification, un bogue a été trouvé qui autrement passerait inaperçu, et à cause duquel chaque XBox 360 planterait après quatre heures d'utilisation. Les ingénieurs d'IBM ont confirmé que leurs tests n'auraient pas trouvé ce bogue.
Vous pouvez en savoir plus sur TLA + sur Internet, mais parlons maintenant des spécifications informelles. Nous avons rarement à écrire des programmes qui calculent le plus petit diviseur commun, etc. Beaucoup plus souvent, nous écrivons des programmes comme l'outil de jolie imprimante que j'ai écrit pour TLA+. Après le traitement le plus simple, le code TLA+ ressemblerait à ceci :
Mais dans l'exemple ci-dessus, l'utilisateur souhaitait très probablement que la conjonction et les signes égal soient alignés. Ainsi, le formatage correct ressemblerait plus à ceci :
Considérons un autre exemple:
Ici, au contraire, l'alignement des signes égal, addition et multiplication dans la source était aléatoire, donc le traitement le plus simple suffit amplement. En général, il n'y a pas de définition mathématique exacte du formatage correct, car "correct" dans ce cas signifie "ce que l'utilisateur veut", et cela ne peut pas être déterminé mathématiquement.
Il semblerait que si nous n'avons pas de définition de la vérité, alors la spécification est inutile. Mais ce n'est pas. Ce n'est pas parce que nous ne savons pas ce qu'un programme est censé faire que nous n'avons pas besoin de réfléchir à son fonctionnement, au contraire, nous devons y mettre encore plus d'efforts. La spécification est particulièrement importante ici. Il est impossible de déterminer le programme optimal pour l'impression structurée, mais cela ne signifie pas que nous ne devrions pas le prendre du tout, et écrire du code comme un flux de conscience n'est pas une bonne chose. Au final, j'ai écrit une spécification de six règles avec des définitions sous forme de commentaires dans un fichier java. Voici un exemple d'une des règles : a left-comment token is LeftComment aligned with its covering token. Cette règle est écrite, dirons-nous, en anglais mathématique : LeftComment aligned, left-comment и covering token - termes avec 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 que six règles sont beaucoup plus faciles à comprendre et à déboguer que 850 lignes de code. Je dois dire que l'écriture de ces règles n'a pas été facile, il a fallu pas mal de temps pour les déboguer. Spécialement dans ce but, j'ai écrit un code qui indiquait quelle règle était utilisée. Grâce au fait que j'ai testé ces six règles sur plusieurs exemples, je n'ai pas eu à déboguer 850 lignes de code, et les bogues se sont avérés assez faciles à trouver. Java a d'excellents outils pour cela. Si je venais d'écrire le code, cela m'aurait pris beaucoup plus de temps, et le formatage aurait été de moins bonne qualité.
Pourquoi une spécification formelle n'a-t-elle pas pu être utilisée ? D'une part, l'exécution correcte n'est pas trop importante ici. Les impressions structurelles ne plairont à personne, donc je n'ai pas eu à le faire fonctionner correctement dans toutes les situations étranges. Encore plus important est le fait que je n'avais pas les outils adéquats. Le vérificateur de modèle TLA + est inutile ici, donc je devrais écrire manuellement les exemples.
La spécification ci-dessus a des caractéristiques communes à toutes les spécifications. C'est un niveau supérieur au code. Il peut être implémenté dans n'importe quelle langue. Tous les outils ou méthodes sont inutiles pour l'écrire. Aucun cours de programmation ne vous aidera à rédiger cette spécification. Et il n'y a aucun outil qui pourrait rendre cette spécification inutile, à moins, bien sûr, que vous écriviez un langage spécifiquement pour écrire des programmes d'impression structurés en TLA+. Enfin, cette spécification ne dit rien sur la manière exacte dont nous allons écrire le code, elle indique seulement ce que fait ce code. Nous écrivons la 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 nettement plus courtes et plus simples :
De plus, cette spécification est un ensemble de règles. En règle générale, c'est un signe de mauvaise spécification. Comprendre les conséquences d'un ensemble de règles est assez difficile, c'est pourquoi j'ai dû passer beaucoup de temps à les déboguer. Cependant, dans ce cas, je ne pouvais pas trouver de meilleur moyen.
Il vaut la peine de dire quelques mots sur les programmes qui fonctionnent en continu. En règle générale, ils fonctionnent en parallèle, par exemple, des systèmes d'exploitation ou des systèmes distribués. Très peu de gens peuvent les comprendre mentalement ou sur papier, et je n'en fais pas partie, même si j'ai pu le faire autrefois. Par conséquent, nous avons besoin d'outils qui vérifieront notre travail - par exemple, TLA + ou PlusCal.
Pourquoi était-il nécessaire d'écrire une spécification si je savais déjà exactement ce que le code devait faire ? En fait, je pensais juste que je le savais. De plus, avec un cahier des charges, un outsider n'a plus besoin d'entrer dans le code pour comprendre exactement ce qu'il fait. J'ai une règle : il ne devrait pas y avoir de règles générales. Il y a une exception à cette règle, bien sûr, c'est la seule règle générale que je suis : la spécification de ce que fait le code doit dire aux gens tout ce qu'ils doivent savoir lorsqu'ils utilisent le code.
Alors, qu'est-ce que les programmeurs doivent savoir exactement sur la pensée ? Pour commencer, comme tout le monde : si vous n'écrivez pas, alors il vous semble seulement que vous pensez. De plus, vous devez réfléchir avant de coder, ce qui signifie que vous devez é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 n'importe qui. Et ce "quelqu'un" peut être l'auteur du code lui-même un mois après sa rédaction. Une spécification est nécessaire pour les grands programmes et systèmes, pour les classes, pour les méthodes et parfois même pour les sections complexes d'une seule méthode. Que faut-il exactement écrire sur le code ? Vous devez décrire ce qu'il fait, c'est-à-dire ce qui peut être utile à toute personne utilisant ce code. Parfois, il peut également être nécessaire de spécifier comment le code accomplit son objectif. Si nous avons utilisé cette méthode au cours des algorithmes, nous l'appelons un algorithme. S'il s'agit de quelque chose de plus spécial et de 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 d'un programme.
Comment exactement devez-vous écrire une spécification de code ? L'essentiel : il devrait être d'un niveau supérieur au code lui-même. Il doit décrire les états et les comportements. Il doit être aussi strict que la tâche l'exige. Si vous écrivez une spécification sur la manière dont une tâche doit être implémentée, vous pouvez l'écrire en pseudocode ou avec PlusCal. Vous devez apprendre à rédiger des spécifications sur des spécifications formelles. Cela vous donnera les compétences nécessaires qui vous aideront également avec les compétences informelles. Comment apprend-on à rédiger des spécifications formelles ? Lorsque nous avons appris à programmer, nous avons écrit des programmes puis les avons débogués. C'est la même chose ici : écrivez la spécification, vérifiez-la avec le vérificateur de modèle et corrigez les bogues. TLA+ n'est peut-être pas le meilleur langage pour une spécification formelle, et un autre langage sera probablement mieux adapté à vos besoins spécifiques. L'avantage de TLA+ est qu'il enseigne très bien la pensée mathématique.
Comment lier spécification et code ? A l'aide de commentaires qui relient les concepts mathématiques et leur mise en œuvre. Si vous travaillez avec des graphiques, au niveau du programme, vous aurez des tableaux de nœuds et des tableaux de liens. Par conséquent, vous devez écrire exactement comment le graphe est implémenté par ces structures de programmation.
Il convient de noter qu'aucun des éléments ci-dessus ne s'applique au processus réel d'écriture de code. Lorsque vous écrivez le code, c'est-à-dire que vous effectuez la troisième étape, vous devez également réfléchir et réfléchir au programme. Si une sous-tâche s'avère complexe ou non évidente, vous devez rédiger une spécification pour celle-ci. Mais je ne parle pas du code lui-même ici. Vous pouvez utiliser n'importe quel langage de programmation, n'importe quelle méthodologie, il ne s'agit pas d'eux. De plus, rien de ce qui précède n'élimine la nécessité de tester et de déboguer le code. Même si le modèle abstrait est écrit correctement, il peut y avoir des bogues dans son implémentation.
La rédaction des spécifications est une étape supplémentaire dans le processus de codage. Grâce à cela, de nombreuses erreurs peuvent être détectées avec moins d'effort - nous le savons grâce à l'expérience des programmeurs d'Amazon. Avec les spécifications, la qualité des programmes devient plus élevée. Alors pourquoi s'en passe-t-on si souvent ? Parce que l'écriture est difficile. Et écrire est difficile, car pour cela, il faut réfléchir, et penser est également difficile. Il est toujours plus facile de prétendre ce que vous pensez. Ici, vous pouvez faire une analogie avec la course - moins vous courez, plus vous courez lentement. Vous devez entraîner vos muscles et vous entraîner à écrire. Besoin de pratique.
La spécification peut être incorrecte. Vous avez peut-être fait une erreur quelque part, ou les exigences ont peut-être changé, ou une amélioration peut être nécessaire. Tout code que quelqu'un utilise doit être changé, donc tôt ou tard la spécification ne correspondra plus au programme. Idéalement, dans ce cas, vous devez écrire une nouvelle spécification et réécrire complètement le code. Nous savons très bien que personne ne fait cela. En pratique, nous corrigeons le code et éventuellement mettons à jour la spécification. Si cela doit arriver tôt ou tard, alors pourquoi écrire des spécifications ? Premièrement, pour la personne qui éditera votre code, chaque mot supplémentaire dans la spécification vaudra son pesant d'or, et cette personne pourrait bien être vous-même. Je me reproche souvent de ne pas avoir suffisamment de spécifications lorsque je modifie mon code. Et j'écris plus de spécifications que de code. Par conséquent, lorsque vous modifiez le code, la spécification doit toujours être mise à jour. Deuxièmement, à chaque révision, le code empire, il devient de plus en plus difficile à lire et à maintenir. Il s'agit d'une augmentation de l'entropie. Mais si vous ne commencez pas avec une spécification, chaque ligne que vous écrivez sera une modification, et le code sera lourd et difficile à lire dès le début.
Comme dit , aucune bataille n'a été gagnée par un plan, et aucune bataille n'a été gagnée sans un plan. Et il savait une chose ou deux sur les batailles. Il existe une opinion selon laquelle la rédaction d'un cahier des charges est une perte de temps. Parfois, c'est vrai, et la tâche est si simple qu'il n'y a rien à réfléchir. Mais vous devez toujours vous rappeler que lorsqu'on vous dit de ne pas écrire de spécifications, on vous dit de ne pas réfléchir. Et vous devriez y penser à chaque fois. Réfléchir à la tâche ne garantit pas que vous ne ferez pas d'erreurs. Comme nous le savons, personne n'a inventé la baguette magique et la programmation est une tâche difficile. Mais si vous ne réfléchissez pas au problème, vous êtes assuré de faire des erreurs.
Vous pouvez en savoir plus sur TLA + et PlusCal sur un site Web spécial, vous pouvez y accéder depuis ma page d'accueil . C'est tout pour moi, merci de votre attention.
Veuillez noter qu'il s'agit d'une traduction. Lorsque vous écrivez des commentaires, n'oubliez pas que l'auteur ne les lira pas. Si vous voulez vraiment discuter avec l'auteur, alors il sera à la conférence Hydra 2019, qui se tiendra les 11 et 12 juillet 2019 à Saint-Pétersbourg. Les billets peuvent être achetés .
Source: habr.com