Aquest article és una traducció . Però abans d'ella una petita presentació. Com es formen els zombis? Tothom es va trobar en una situació en què volia portar un amic o un company al seu nivell, però no funciona. I no és tant amb tu com amb ell que “no surt”: a un costat de la balança hi ha un sou normal, tasques, etc., i a l'altre, la necessitat de pensar. Pensar és desagradable i dolorós. Ràpidament es rendeix i continua escrivint codi sense encendre el cervell en absolut. T'imagines quant esforç es necessita per superar la barrera de la impotència apresa, i simplement no ho fas. Així es formen els zombis que, segons sembla, es poden curar, però sembla que ningú ho farà.
Quan vaig veure això (sí, el mateix camarada dels llibres de text) i no fa un informe, sinó una sessió de preguntes i respostes, em desconfiava una mica. Per si de cas, Leslie és un científic de fama mundial, autor d'obres fonamentals en informàtica distribuïda, i també el podeu conèixer per les lletres La de la paraula LaTeX - "Lamport TeX". El segon factor alarmant és la seva exigència: tothom que vingui ha d'escoltar (absolutament gratuïtament) un parell dels seus informes per endavant, plantejar almenys una pregunta sobre ells i només després venir. Vaig decidir veure què estava emetent Lamport allà, i és genial! És exactament això, la píndola màgica d'enllaç per curar zombis. Us adverteixo: des del text, els amants de les metodologies súper flexibles i els que no els agrada provar el que està escrit es poden esgotar notablement.
Després de l'habrokat, de fet, comença la traducció del seminari. Gaudeix de la lectura!
Sigui quina sigui la tasca que facis, sempre has de seguir tres passos:
- decidiu quin objectiu voleu assolir;
- decideix com aconseguiràs el teu objectiu;
- arriba al teu objectiu.
Això també s'aplica a la programació. Quan escrivim codi, hem de:
- decidir què ha de fer el programa;
- determinar com ha de realitzar la seva tasca;
- escriu el codi corresponent.
L'últim pas, és clar, és molt important, però avui no en parlaré. En canvi, parlarem dels dos primers. Cada programador les realitza abans de començar a treballar. No us asseieu a escriure tret que hàgiu decidit si esteu escrivint un navegador o una base de dades. Una certa idea de l'objectiu ha d'estar present. I definitivament penseu què farà exactament el programa, i no escriviu d'alguna manera amb l'esperança que el codi es converteixi d'alguna manera en un navegador.
Com es produeix exactament aquest pre-pensament del codi? Quant d'esforç hem de posar en això? Tot depèn de la complexitat del problema que estem resolent. Suposem que volem escriure un sistema distribuït tolerant a errors. En aquest cas, hauríem de pensar bé les coses abans de seure a programar. Què passa si només necessitem incrementar una variable entera en 1? A primera vista, aquí tot és trivial i no cal pensar-hi, però després recordem que es pot produir un desbordament. Per tant, fins i tot per entendre si un problema és simple o complex, primer cal pensar.
Si penseu amb antelació en possibles solucions al problema, podeu evitar errors. Però això requereix que el teu pensament sigui clar. Per aconseguir-ho, heu d'escriure els vostres pensaments. M'agrada molt la cita de Dick Guindon: "Quan escrius, la natura et mostra com de descuidat és el teu pensament". Si no escrius, només penses que estàs pensant. I heu d'escriure els vostres pensaments en forma d'especificacions.
Les especificacions fan moltes funcions, especialment en projectes grans. Però només en parlaré d'un d'ells: ens ajuden a pensar amb claredat. Pensar amb claredat és molt important i bastant difícil, així que aquí necessitem ajuda. En quin idioma hem d'escriure les especificacions? En general, aquesta és sempre la primera pregunta per als programadors: en quin llenguatge escriurem. No hi ha cap resposta correcta: els problemes que estem resolent són massa diversos. Per a alguns, TLA+ és un llenguatge d'especificació que vaig desenvolupar. Per a altres, és més convenient utilitzar el xinès. Tot depèn de la situació.
Més important és una altra pregunta: com aconseguir un pensament més clar? Resposta: Hem de pensar com els científics. Aquesta és una manera de pensar que s'ha demostrat durant els últims 500 anys. En ciència, construïm models matemàtics de la realitat. L'astronomia va ser potser la primera ciència en el sentit estricte de la paraula. En el model matemàtic utilitzat en astronomia, els cossos celestes apareixen com a punts amb massa, posició i impuls, encara que en realitat són objectes extremadament complexos amb muntanyes i oceans, marees i marees. Aquest model, com qualsevol altre, va ser creat per resoldre determinats problemes. És ideal per determinar cap a on apuntar el telescopi si necessiteu trobar un planeta. Però si voleu predir el temps en aquest planeta, aquest model no funcionarà.
Les matemàtiques ens permeten determinar les propietats del model. I la ciència mostra com aquestes propietats es relacionen amb la realitat. Parlem de la nostra ciència, informàtica. La realitat amb la qual treballem són sistemes informàtics de diversa índole: processadors, consoles de jocs, ordinadors, programes executius, etc. Parlaré d'executar un programa en un ordinador, però en general, totes aquestes conclusions s'apliquen a qualsevol sistema informàtic. A la nostra ciència, fem servir molts models diferents: la màquina de Turing, conjunts d'esdeveniments parcialment ordenats i molts altres.
Què és un programa? Aquest és qualsevol codi que es pugui considerar independentment. Suposem que necessitem escriure un navegador. Realitzem tres tasques: dissenyem la vista de l'usuari del programa, després escrivim el diagrama d'alt nivell del programa i finalment escrivim el codi. Mentre escrivim el codi, ens adonem que hem d'escriure un formatador de text. Aquí hem de tornar a resoldre tres problemes: determinar quin text retornarà aquesta eina; seleccionar un algorisme per al format; escriure codi. Aquesta tasca té la seva pròpia subtasca: inserir correctament un guionet a les paraules. També resolem aquesta subtasca en tres passos: com podeu veure, es repeteixen a molts nivells.
Considerem amb més detall el primer pas: quin problema resol el programa. Aquí, sovint modelem un programa com una funció que pren una mica d'entrada i produeix una mica de sortida. En matemàtiques, una funció es descriu normalment com un conjunt ordenat de parells. Per exemple, la funció de quadrat per als nombres naturals es descriu com el conjunt {<0,0>, <1,1>, <2,4>, <3,9>, …}. El domini d'aquesta funció és el conjunt dels primers elements de cada parell, és a dir, els nombres naturals. Per definir una funció, hem d'especificar el seu abast i fórmula.
Però les funcions en matemàtiques no són el mateix que les funcions en llenguatges de programació. Les matemàtiques són molt més fàcils. Com que no tinc temps per a exemples complexos, considerem-ne un de simple: una funció en C o un mètode estàtic en Java que retorna el màxim comú divisor de dos nombres enters. En l'especificació d'aquest mètode, escriurem: calcula GCD(M,N) per arguments M и NOn GCD(M,N) - una funció el domini de la qual és el conjunt de parells de nombres enters, i el valor de retorn és el nombre enter més gran que és divisible per M и N. Com es relaciona aquest model amb la realitat? El model funciona amb nombres enters, mentre que en C o Java tenim un de 32 bits int. Aquest model ens permet decidir si l'algorisme és correcte GCD, però no evitarà errors de desbordament. Això requeriria un model més complex, per al qual no hi ha temps.
Parlem de les limitacions d'una funció com a model. Alguns programes (com ara els sistemes operatius) no només retornen un valor determinat per a determinats arguments, sinó que es poden executar contínuament. A més, la funció com a model no és adequada per al segon pas: planificar com resoldre el problema. L'ordenació ràpida i l'ordenació de bombolles calculen la mateixa funció, però són algorismes completament diferents. Per tant, per descriure com s'aconsegueix l'objectiu del programa, faig servir un model diferent, anomenem-lo el model de comportament estàndard. El programa en ell es representa com un conjunt de tots els comportaments permesos, cadascun dels quals, al seu torn, és una seqüència d'estats, i l'estat és l'assignació de valors a les variables.
Vegem com seria el segon pas de l'algorisme d'Euclides. Hem de calcular GCD(M, N). Inicialitzem M как xI N как y, després resta repetidament la menor d'aquestes variables de la més gran fins que siguin iguals. Per exemple, si M = 12I N = 18, podem descriure el comportament següent:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
I si M = 0 и N = 0? El zero és divisible per tots els nombres, de manera que no hi ha el màxim divisor en aquest cas. En aquesta situació, hem de tornar al primer pas i preguntar-nos: realment necessitem calcular el GCD per a nombres no positius? Si això no és necessari, només cal que canvieu l'especificació.
Aquí hauríem de fer una petita digressió sobre la productivitat. Sovint es mesura en el nombre de línies de codi escrites al dia. Però la teva feina és molt més útil si t'elimines un cert nombre de línies, perquè tens menys espai per als errors. I la manera més senzilla de desfer-se del codi és en el primer pas. És totalment possible que no necessiteu totes les campanes i xiulets que intenteu implementar. La manera més ràpida de simplificar un programa i estalviar temps és no fer coses que no s'haurien de fer. El segon pas és el segon potencial d'estalvi de temps. Si mesureu la productivitat en termes de línies escrites, pensar en com realitzar una tasca us farà menys productiu, perquè podeu resoldre el mateix problema amb menys codi. No puc donar aquí estadístiques exactes, perquè no tinc manera de comptar el nombre de línies que no he escrit pel fet que he dedicat temps a l'especificació, és a dir, al primer i segon pas. I aquí tampoc es pot configurar l'experiment, perquè a l'experiment no tenim dret a completar el primer pas, la tasca està predeterminada.
És fàcil passar per alt moltes dificultats en especificacions informals. No hi ha res difícil escriure especificacions estrictes per a les funcions, no parlaré d'això. En lloc d'això, parlarem d'escriure especificacions fortes per a comportaments estàndard. Hi ha un teorema que diu que qualsevol conjunt de comportaments es pot descriure mitjançant la propietat de seguretat (seguretat) i propietats de supervivència (vivència). La seguretat vol dir que no passarà res dolent, el programa no donarà una resposta incorrecta. La supervivència significa que tard o d'hora passarà alguna cosa bona, és a dir, el programa donarà la resposta correcta tard o d'hora. Com a regla general, la seguretat és un indicador més important, els errors es produeixen amb més freqüència aquí. Per tant, per estalviar temps, no parlaré de la supervivència, encara que, és clar, també és important.
Aconseguim seguretat prescrivant, en primer lloc, el conjunt de possibles estats inicials. I en segon lloc, les relacions amb tots els estats següents possibles per a cada estat. Actuem com a científics i definim els estats matemàticament. El conjunt d'estats inicials es descriu mitjançant una fórmula, per exemple, en el cas de l'algorisme d'Euclides: (x = M) ∧ (y = N). Per a determinats valors M и N només hi ha un estat inicial. La relació amb el següent estat es descriu mitjançant una fórmula en què les variables del següent estat s'escriuen amb un primer, i les variables de l'estat actual s'escriuen sense primer. En el cas de l'algorisme d'Euclides, tractarem la disjunció de dues fórmules, en una de les quals x és el valor més gran, i en el segon - y:
En el primer cas, el nou valor de y és igual al valor anterior de y, i obtenim el nou valor de x restant la variable més petita de la variable més gran. En el segon cas, fem el contrari.
Tornem a l'algorisme d'Euclides. Suposem de nou que M = 12, N = 18. Això defineix un únic estat inicial, (x = 12) ∧ (y = 18). A continuació, connectem aquests valors a la fórmula anterior i obtenim:
Aquí teniu l'única solució possible: x' = 18 - 12 ∧ y' = 12i obtenim el comportament: [x = 12, y = 18]. De la mateixa manera, podem descriure tots els estats del nostre comportament: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
En últim estat [x = 6, y = 6] ambdues parts de l'expressió seran falses, de manera que no té el següent estat. Per tant, tenim una especificació completa del segon pas; com podeu veure, es tracta de matemàtiques força normals, com en enginyers i científics, i no estranyes, com en informàtica.
Aquestes dues fórmules es poden combinar en una fórmula de lògica temporal. És elegant i fàcil d'explicar, però ara no hi ha temps per a ella. Potser necessitem la lògica temporal només per a la propietat de vivacitat, no és necessària per a la seguretat. No m'agrada la lògica temporal com a tal, no són matemàtiques del tot corrents, però en el cas de la vivacitat és un mal necessari.
En l'algorisme d'Euclides, per a cada valor x и y tenen valors únics x' и y', que fan certa la relació amb el següent estat. En altres paraules, l'algorisme d'Euclides és determinista. Per modelar un algorisme no determinista, l'estat actual ha de tenir múltiples estats futurs possibles i que cada valor de variable no cebada tingui múltiples valors de variables cebades de manera que la relació amb el següent estat sigui certa. Això és fàcil de fer, però ara no posaré exemples.
Per fer una eina de treball, necessites matemàtiques formals. Com formalitzar l'especificació? Per fer-ho, necessitem un llenguatge formal, per exemple, . L'especificació de l'algorisme d'Euclides es veuria així en aquest llenguatge:
Un símbol de signe igual amb un triangle significa que el valor a l'esquerra del signe es defineix com a igual al valor de la dreta del signe. En essència, l'especificació és una definició, en el nostre cas dues definicions. A l'especificació de TLA+, cal afegir declaracions i alguna sintaxi, com a la diapositiva anterior. En ASCII es veuria així:
Com podeu veure, res complicat. L'especificació per a TLA+ es pot provar, és a dir, obviar tots els comportaments possibles en un model petit. En el nostre cas, aquest model tindrà uns valors determinats M и N. Aquest és un mètode de verificació molt eficient i senzill que és completament automàtic. També és possible escriure proves formals de veritat i comprovar-les mecànicament, però això requereix molt de temps, de manera que gairebé ningú ho fa.
El principal desavantatge de TLA+ és que són matemàtiques, i els programadors i informàtics tenen por de les matemàtiques. A primera vista, sembla una broma, però, malauradament, ho dic amb tota serietat. El meu company només m'explicava com va intentar explicar TLA+ a diversos desenvolupadors. Tan bon punt les fórmules van aparèixer a la pantalla, de seguida es van convertir en ulls de vidre. Així que si TLA+ us fa por, podeu utilitzar-lo , és una mena de llenguatge de programació de joguina. Una expressió a PlusCal pot ser qualsevol expressió TLA+, és a dir, en general, qualsevol expressió matemàtica. A més, PlusCal té una sintaxi per a algorismes no deterministes. Com que PlusCal pot escriure qualsevol expressió TLA+, PlusCal és molt més expressiu que qualsevol llenguatge de programació real. A continuació, PlusCal es compila en una especificació TLA+ de fàcil lectura. Això no vol dir, per descomptat, que la complexa especificació PlusCal es converteixi en una de simple a TLA +: només la correspondència entre elles és òbvia, no hi haurà complexitat addicional. Finalment, aquesta especificació es pot verificar mitjançant eines TLA+. Amb tot, PlusCal pot ajudar a superar la fòbia matemàtica i és fàcil d'entendre fins i tot per a programadors i informàtics. En el passat, vaig publicar algorismes durant algun temps (uns 10 anys).
Potser algú s'oposarà que TLA + i PlusCal són matemàtiques, i que les matemàtiques només funcionen amb exemples inventats. A la pràctica, cal un llenguatge real amb tipus, procediments, objectes, etc. Això està malament. Això és el que escriu Chris Newcomb, que treballava a Amazon: "Hem utilitzat TLA+ en deu projectes importants i, en cada cas, utilitzar-lo ha marcat una diferència significativa en el desenvolupament perquè vam poder detectar errors perillosos abans d'arribar a la producció i perquè ens va donar la visió i la confiança que necessitàvem per fer optimitzacions de rendiment agressives sense afectar la veritat del programa". Sovint podeu escoltar que quan utilitzeu mètodes formals, obtenim un codi ineficient; a la pràctica, tot és exactament el contrari. A més, hi ha l'opinió que els directius no poden estar convençuts de la necessitat de mètodes formals, encara que els programadors estiguin convençuts de la seva utilitat. I Newcomb escriu: "Els directius ara estan fent força per escriure especificacions per a TLA + i destinar-hi específicament temps". Així, quan els directius veuen que TLA+ funciona, estan encantats d'acceptar-ho. Chris Newcomb va escriure això fa uns sis mesos (octubre de 2014), però ara, pel que jo sé, TLA+ s'utilitza en 14 projectes, no en 10. Un altre exemple és en el disseny de l'XBox 360. Un intern va venir a Charles Thacker i va escriure l'especificació per al sistema de memòria. Gràcies a aquesta especificació, es va trobar un error que, d'altra manera, passaria desapercebut, i per la qual cosa cada XBox 360 es bloquejaria després de quatre hores d'ús. Els enginyers d'IBM van confirmar que les seves proves no haurien trobat aquest error.
Podeu llegir més sobre TLA + a Internet, però ara parlem d'especificacions informals. Poques vegades hem d'escriure programes que calculin el mínim comú divisor i similars. Molt més sovint escrivim programes com l'eina d'impressora bonica que vaig escriure per a TLA+. Després del processament més senzill, el codi TLA + es veuria així:
Però en l'exemple anterior, l'usuari probablement volia que la conjunció i els signes d'igualtat estiguessin alineats. Per tant, el format correcte seria més semblant a això:
Considerem un altre exemple:
Aquí, per contra, l'alineació dels signes d'igualtat, suma i multiplicació a la font era aleatòria, de manera que el processament més senzill és suficient. En general, no hi ha una definició matemàtica exacta del format correcte, perquè "correcte" en aquest cas significa "el que vol l'usuari", i això no es pot determinar matemàticament.
Sembla que si no tenim una definició de veritat, aleshores l'especificació és inútil. Però no ho és. El fet que no sabem què ha de fer un programa no vol dir que no hàgim de pensar en com funciona; al contrari, hem d'esforçar-hi encara més. L'especificació és especialment important aquí. És impossible determinar el programa òptim per a la impressió estructurada, però això no vol dir que no l'haguem de prendre en absolut, i escriure codi com a corrent de consciència no és bo. Al final, vaig escriure una especificació de sis regles amb definicions en forma de comentaris en un fitxer java. Aquí teniu un exemple d'una de les regles: a left-comment token is LeftComment aligned with its covering token. Aquesta regla està escrita, diguem-ne, en anglès matemàtic: LeftComment aligned, left-comment и covering token - termes amb definicions. Així és com els matemàtics descriuen les matemàtiques: escriuen definicions de termes i, a partir d'elles, regles. L'avantatge d'aquesta especificació és que sis regles són molt més fàcils d'entendre i depurar que 850 línies de codi. He de dir que escriure aquestes regles no va ser fàcil, va costar molt de temps depurar-les. Especialment per a aquest propòsit, vaig escriure un codi que informava de quina regla s'utilitzava. Gràcies al fet que vaig provar aquestes sis regles en diversos exemples, no vaig haver de depurar 850 línies de codi i els errors van resultar ser bastant fàcils de trobar. Java té grans eines per a això. Si acabés d'escriure el codi, m'hauria trigat molt més i el format hauria estat de menor qualitat.
Per què no es podria utilitzar una especificació formal? D'una banda, la correcta execució no és massa important aquí. Les impressions estructurals no agradaran a ningú, així que no vaig haver d'aconseguir que funcionés bé en totes les situacions estranyes. Encara més important és el fet que no tenia les eines adequades. El verificador de models TLA+ és inútil aquí, així que hauria d'escriure manualment els exemples.
L'especificació anterior té característiques comunes a totes les especificacions. És un nivell més alt que el codi. Es pot implementar en qualsevol idioma. Qualsevol eina o mètode no serveix per escriure'l. Cap curs de programació us ajudarà a escriure aquesta especificació. I no hi ha eines que puguin fer que aquesta especificació sigui innecessària, tret que, per descomptat, estigueu escrivint un llenguatge específicament per escriure programes d'impressió estructurada en TLA+. Finalment, aquesta especificació no diu res sobre com escriurem el codi exactament, només indica què fa aquest codi. Escrivim l'especificació per ajudar-nos a pensar en el problema abans de començar a pensar en el codi.
Però aquesta especificació també té característiques que la distingeixen d'altres especificacions. El 95% de les altres especificacions són significativament més curtes i senzilles:
A més, aquesta especificació és un conjunt de regles. Per regla general, això és un signe d'especificació deficient. Entendre les conseqüències d'un conjunt de regles és bastant difícil, per això vaig haver de dedicar molt de temps a depurar-les. Tanmateix, en aquest cas, no he pogut trobar una millor manera.
Val la pena dir algunes paraules sobre els programes que s'executen contínuament. Per regla general, funcionen en paral·lel, per exemple, sistemes operatius o sistemes distribuïts. Molt poca gent els pot entendre mentalment o sobre el paper, i jo no en sóc, encara que alguna vegada ho vaig poder fer. Per tant, necessitem eines que comprovin el nostre treball, per exemple, TLA + o PlusCal.
Per què era necessari escriure una especificació si ja sabia què havia de fer exactament el codi? De fet, només pensava que ho sabia. A més, amb una especificació, un foraster ja no necessita entrar al codi per entendre què fa exactament. Tinc una regla: no hi hauria d'haver regles generals. Hi ha una excepció a aquesta regla, és clar, és l'única regla general que segueixo: l'especificació del que fa el codi hauria de dir a la gent tot el que necessiten saber quan utilitzen el codi.
Aleshores, què necessiten saber exactament els programadors sobre el pensament? Per començar, igual que tothom: si no escrius, només et sembla que estàs pensant. A més, heu de pensar abans de codificar, el que significa que heu d'escriure abans de codificar. L'especificació és el que escrivim abans de començar a codificar. Cal una especificació per a qualsevol codi que qualsevol pugui utilitzar o modificar. I aquest "algú" pot ser el mateix autor del codi un mes després de ser escrit. Es necessita una especificació per a programes i sistemes grans, per a classes, per a mètodes i, de vegades, fins i tot per a seccions complexes d'un sol mètode. Què s'ha d'escriure exactament sobre el codi? Heu de descriure què fa, és a dir, què pot ser útil per a qualsevol persona que faci servir aquest codi. De vegades també pot ser necessari especificar com el codi aconsegueix el seu propòsit. Si vam passar per aquest mètode en el curs dels algorismes, llavors l'anomenem algorisme. Si és quelcom més especial i nou, l'anomenem disseny d'alt nivell. Aquí no hi ha cap diferència formal: tots dos són un model abstracte d'un programa.
Com s'ha d'escriure exactament una especificació de codi? El més important: hauria de ser un nivell més alt que el propi codi. Ha de descriure estats i comportaments. Ha de ser tan estricte com ho requereixi la tasca. Si esteu escrivint una especificació de com s'ha d'implementar una tasca, podeu escriure-la en pseudocodi o amb PlusCal. Heu d'aprendre a escriure especificacions sobre especificacions formals. Això us donarà les habilitats necessàries que us ajudaran també amb les informals. Com s'aprèn a escriure especificacions formals? Quan vam aprendre a programar, vam escriure programes i després els vam depurar. Aquí passa el mateix: escriviu les especificacions, comproveu-les amb el verificador de models i solucioneu els errors. És possible que TLA+ no sigui el millor llenguatge per a una especificació formal, i és probable que un altre idioma sigui millor per a les vostres necessitats específiques. L'avantatge de TLA+ és que ensenya molt bé el pensament matemàtic.
Com enllaçar especificació i codi? Amb l'ajuda de comentaris que vinculen conceptes matemàtics i la seva implementació. Si treballeu amb gràfics, a nivell de programa tindreu matrius de nodes i matrius d'enllaços. Per tant, cal escriure exactament com s'implementa el gràfic mitjançant aquestes estructures de programació.
Cal tenir en compte que cap de les anteriors s'aplica al procés real d'escriptura de codi. Quan escriviu el codi, és a dir, feu el tercer pas, també heu de pensar i pensar a través del programa. Si una subtasca resulta ser complexa o no òbvia, heu d'escriure una especificació per a ella. Però aquí no parlo del codi en si. Podeu utilitzar qualsevol llenguatge de programació, qualsevol metodologia, no es tracta d'ells. A més, cap de les anteriors elimina la necessitat de provar i depurar codi. Fins i tot si el model abstracte està escrit correctament, pot haver-hi errors en la seva implementació.
L'escriptura de les especificacions és un pas addicional en el procés de codificació. Gràcies a això, es poden detectar molts errors amb menys esforç; això ho sabem per l'experiència dels programadors d'Amazon. Amb les especificacions, la qualitat dels programes augmenta. Aleshores, per què anem tan sovint sense ells? Perquè escriure és difícil. I escriure és difícil, perquè per això cal pensar, i pensar també és difícil. Sempre és més fàcil fingir el que penses. Aquí podeu dibuixar una analogia amb córrer: com menys corre, més lent correrà. Cal entrenar els músculs i practicar l'escriptura. Necessita pràctica.
L'especificació pot ser incorrecta. És possible que hagis comès un error en algun lloc, que els requisits hagin canviat o que calgui fer una millora. Qualsevol codi que faci servir qualsevol persona s'ha de canviar, de manera que tard o d'hora l'especificació ja no coincidirà amb el programa. Idealment, en aquest cas, haureu d'escriure una nova especificació i reescriure completament el codi. Sabem molt bé que ningú ho fa. A la pràctica, peguem el codi i, possiblement, actualitzem l'especificació. Si això és obligat a passar tard o d'hora, per què escriure especificacions? En primer lloc, per a la persona que editarà el vostre codi, cada paraula addicional de l'especificació valdrà el seu pes en or, i és possible que aquesta persona siguis tu mateix. Sovint em reprendo per no obtenir prou especificacions quan edito el meu codi. I escric més especificacions que codi. Per tant, quan editeu el codi, l'especificació sempre s'ha d'actualitzar. En segon lloc, amb cada revisió, el codi empitjora, cada cop es fa més difícil de llegir i mantenir. Això és un augment de l'entropia. Però si no comenceu amb una especificació, llavors cada línia que escriu serà una edició i el codi serà difícil de manejar i difícil de llegir des del principi.
Com s'ha dit , no es va guanyar cap batalla per pla, i no es va guanyar cap batalla sense un pla. I en sabia una o dues coses sobre les batalles. Hi ha l'opinió que escriure especificacions és una pèrdua de temps. De vegades això és cert, i la tasca és tan senzilla que no hi ha res per pensar-hi. Però sempre heu de recordar que quan us diuen que no escriviu especificacions, se us diu que no penseu. I hauries de pensar-hi cada cop. Pensar en la tasca no garanteix que no cometreu errors. Com sabem, ningú va inventar la vareta màgica, i programar és una tasca difícil. Però si no penseu en el problema, segur que cometreu errors.
Podeu llegir més sobre TLA + i PlusCal en un lloc web especial, podeu anar-hi des de la meva pàgina d'inici . Això és tot per mi, gràcies per la vostra atenció.
Tingueu en compte que això és una traducció. Quan escriviu comentaris, recordeu que l'autor no els llegirà. Si realment voleu xerrar amb l'autor, aleshores serà a la conferència Hydra 2019, que se celebrarà de l'11 al 12 de juliol de 2019 a Sant Petersburg. Les entrades es poden comprar .
Font: www.habr.com