Este é un artigo de tradución . Pero antes hai unha pequena introdución. Como se forman os zombies? Todo o mundo atopouse nunha situación na que queren levar a un amigo ou colega ao seu nivel, pero non funciona. Ademais, "non funciona" non tanto para ti, senón para el: nun lado da escala hai un soldo normal, tarefas, etc., e por outro a necesidade de pensar. Pensar é desagradable e doloroso. Renuncia rapidamente e segue escribindo código sen usar o seu cerebro en absoluto. Te das conta do moito esforzo que fai falta para superar a barreira da impotencia aprendida, e simplemente non o fas. Así se forman os zombies, que parecen ser posibles de curar, pero parece que ninguén o fará.
Cando vin iso (si, ese mesmo amigo dos libros de texto) e non está dando un informe, senón unha sesión de preguntas e respostas, desconfiaba un pouco. Por se acaso, Leslie é un científico de renome mundial, o autor de traballos fundamentais en computación distribuída, e tamén podes coñecelo polas letras La en LaTeX - "Lamport TeX". O segundo factor alarmante é a súa esixencia: todos os que veñan deben escoitar (de xeito totalmente gratuíto) un par dos seus informes con antelación, facer polo menos unha pregunta sobre eles e só despois vir. Decidín ver o que Lamport transmitía alí, e é xenial! Isto é exactamente iso, unha pílula de enlace máxica para tratar zombies. Advírtoche: o texto pode queimar seriamente aos que aman as metodoloxías superáxiles e que non lles gusta probar o que escribiron.
Despois do habrokat, comeza realmente a tradución do seminario. Disfruta da lectura!
Sexa cal sexa a tarefa que realices, sempre debes pasar por tres pasos:
- decidir que obxectivo queres conseguir;
- decide exactamente como conseguirás o teu obxectivo;
- alcanzar o seu obxectivo.
Isto tamén se aplica á programación. Cando escribimos código, necesitamos:
- decidir o que debe facer exactamente o programa;
- determinar exactamente como debe realizar a súa tarefa;
- escribir o código axeitado.
O último paso, por suposto, é moi importante, pero hoxe non vou falar del. Pola contra, comentaremos os dous primeiros. Cada programador realízaos antes de comezar a traballar. Non te sentes a escribir a non ser que teñas decidido o que escribes: un navegador ou unha base de datos. Debe estar presente unha determinada idea do obxectivo. E definitivamente pensas sobre o que fará exactamente o programa e non o escribes ao azar coa esperanza de que o propio código se converta dalgún xeito nun navegador.
Como ocorre exactamente este pensamento previo do código? Canto esforzo debemos poñer nisto? Todo depende da complexidade do problema que esteamos a resolver. Digamos que queremos escribir un sistema distribuído tolerante a fallos. Neste caso, debemos pensar as cousas coidadosamente antes de sentarnos a codificar. E se só precisamos incrementar unha variable enteira en 1? A primeira vista, todo aquí é trivial e non fai falta pensar, pero logo lembramos que pode producirse un desbordamento. Polo tanto, mesmo para comprender se un problema é simple ou complexo, primeiro cómpre pensar.
Se pensas en posibles solucións a un problema con antelación, podes evitar erros. Pero isto require que o teu pensamento sexa claro. Para logralo, cómpre escribir os seus pensamentos. Encántame a cita de Dick Guindon: "Cando escribes, a natureza móstrache o descoidado que é o teu pensamento". Se non escribes, só pensas que estás pensando. E cómpre escribir os seus pensamentos en forma de especificacións.
As especificacións teñen moitas funcións, especialmente en proxectos grandes. Pero só falarei dun deles: axúdannos a pensar con claridade. Pensar con claridade é moi importante e bastante difícil, polo que necesitamos axuda aquí. En que idioma debemos escribir as especificacións? En xeral, esta é sempre a primeira pregunta para os programadores: en que linguaxe escribiremos? Non hai unha resposta correcta: os problemas que resolvemos son demasiado diversos. Para algunhas persoas, TLA+ é unha linguaxe de especificación que desenvolvín. Para outros, é máis cómodo usar chinés. Todo depende da situación.
A pregunta máis importante é: como podemos conseguir un pensamento máis claro? Resposta: Debemos pensar como científicos. Esta é unha forma de pensar que funcionou ben nos últimos 500 anos. Na ciencia construímos modelos matemáticos da realidade. A astronomía foi quizais a primeira ciencia no sentido estrito da palabra. No modelo matemático empregado en astronomía, os corpos celestes aparecen como puntos con masa, posición e momento, aínda que en realidade son obxectos sumamente complexos con montañas e océanos, refluxos e fluxos. Este modelo, como calquera outro, foi creado para resolver certos problemas. É xenial para determinar cara onde apuntar un telescopio se queres atopar un planeta. Pero se queres prever o tempo neste planeta, este modelo non funcionará.
As matemáticas permítennos determinar as propiedades dun modelo. E a ciencia mostra como estas propiedades se relacionan coa realidade. Falemos da nosa ciencia, da informática. A realidade coa que traballamos son sistemas informáticos de moitos tipos diferentes: procesadores, consolas de xogos, ordenadores que executan programas, etc. Vou falar de executar un programa nun ordenador, pero, en xeral, todas estas conclusións aplícanse a calquera sistema informático. Na nosa ciencia utilizamos moitos modelos diferentes: a máquina de Turing, conxuntos parcialmente ordenados de eventos e moitos outros.
Cal é o programa? Este é calquera código que se poida considerar por si só. Digamos que necesitamos escribir un navegador. Realizamos tres tarefas: deseñar a presentación do programa por parte do usuario, despois escribir o diagrama de alto nivel do programa e, finalmente, escribir o código. Mentres escribimos o código, dámonos conta de que necesitamos escribir un formateador de texto. Aquí de novo temos que resolver tres problemas: determinar que texto devolverá esta ferramenta; seleccione un algoritmo para o formato; escribir código. Esta tarefa ten a súa propia subtarefa: inserir guións en palabras correctamente. Tamén resolvemos esta subtarefa en tres pasos: como vemos, repítense en moitos niveis.
Vexamos máis de cerca o primeiro paso: que problema resolve o programa. Aquí a miúdo modelamos un programa como unha función que toma algo de entrada e dá algunha saída. En matemáticas, unha función descríbese normalmente como un conxunto ordenado de pares. Por exemplo, a función de cadrado dos números naturais descríbese como o conxunto {<0,0>, <1,1>, <2,4>, <3,9>, ...}. O dominio de definición desta función é o conxunto dos primeiros elementos de cada par, é dicir, os números naturais. Para definir unha función, necesitamos especificar o seu dominio e fórmula.
Pero as funcións en matemáticas non son o mesmo que as funcións nas linguaxes de programación. As matemáticas son moito máis sinxelas. Como non teño tempo para exemplos complexos, consideremos un simple: unha función en C ou un método estático en Java que devolve o máximo común divisor de dous números enteiros. Na especificación deste método escribiremos: calcula GCD(M,N) para argumentos M и Nonde GCD(M,N) - unha función cuxo dominio é un conxunto de pares de números enteiros e o valor de retorno é o maior enteiro que se divide por M и N. Como se compara a realidade con este modelo? O modelo opera con números enteiros, e en C ou Java temos 32 bits int. Este modelo permítenos decidir se o algoritmo é correcto GCD, pero non evitará erros de desbordamento. Isto requiriría un modelo máis complexo, para o que non hai tempo.
Falemos das limitacións da función como modelo. Algúns programas (como os sistemas operativos) non só devolven un valor específico para certos argumentos; poden executarse continuamente. Ademais, a función como modelo é pouco adecuada para o segundo paso: planificar como resolver o problema. Quicksort e Bubble sort calculan a mesma función, pero son algoritmos completamente diferentes. Polo tanto, para describir o xeito de acadar o obxectivo do programa, uso outro modelo, chamémoslle o modelo de comportamento estándar. O programa represéntase nel como un conxunto de todos os comportamentos válidos, cada un dos cales, á súa vez, é unha secuencia de estados e un estado é a asignación de valores ás variables.
Vexamos como sería o segundo paso para o algoritmo euclidiano. Necesitamos calcular GCD(M, N). Inicializamos M como xE N como y, despois restar repetidamente a menor destas variables da maior ata que sexan iguais. Por exemplo, se M = 12E N = 18, podemos describir o seguinte comportamento:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
E si M = 0 и N = 0? O cero é divisible por todos os números, polo que non hai un maior divisor neste caso. Nesta situación, debemos volver ao primeiro paso e preguntarnos: realmente necesitamos calcular o GCD para números non positivos? Se isto non é necesario, só tes que cambiar a especificación.
Fai aquí unha pequena digresión sobre a produtividade. Moitas veces mídese no número de liñas de código escritas ao día. Pero o teu traballo é moito máis útil se te libras dun certo número de liñas, porque tes menos espazo para os erros. E a forma máis sinxela de desfacerse do código é no primeiro paso. É posible que simplemente non necesites todas as campás e asubíos que estás intentando implementar. A forma máis rápida de simplificar un programa e aforrar tempo é non facer cousas que non se deberían facer. O segundo paso ten o segundo maior potencial de aforro de tempo. Se mide a produtividade en termos de liñas escritas, entón pensar en como completar unha tarefa farao menos produtivo, porque podes resolver o mesmo problema con menos código. Non podo dar aquí estatísticas exactas, porque non teño forma de contar o número de liñas que non escribín debido ao tempo que pasei na especificación, é dicir, no primeiro e segundo paso. E aquí tampouco podemos facer un experimento, porque nun experimento non temos dereito a completar o primeiro paso; a tarefa está determinada de antemán.
É fácil pasar por alto moitas dificultades nas especificacións informais. Non hai nada difícil escribir especificacións estritas para funcións; non vou falar disto. Pola contra, falaremos de escribir especificacións fortes para comportamentos estándar. Hai un teorema que afirma que se pode describir calquera conxunto de comportamentos usando a propiedade de seguridade (seguridade) e propiedades de supervivencia (vivencia). A seguridade significa que non pasará nada malo, o programa non dará a resposta incorrecta. A supervivencia significa que tarde ou cedo sucederá algo bo, é dicir, o programa tarde ou cedo dará a resposta correcta. Como regra xeral, a seguridade é un indicador máis importante; os erros a miúdo ocorren aquí. Polo tanto, para aforrar tempo, non vou falar de supervivencia, aínda que, por suposto, tamén é importante.
Conseguimos a seguridade especificando primeiro un conxunto de posibles estados iniciais. E en segundo lugar, as relacións con todos os estados seguintes posibles para cada estado. Comportémonos como científicos e definamos estados matemáticamente. O conxunto de estados iniciais descríbese coa fórmula, por exemplo, no caso do algoritmo euclidiano: (x = M) ∧ (y = N). Para determinados valores M и N só hai un estado inicial. A relación co seguinte estado descríbese mediante unha fórmula na que as variables do seguinte estado escríbense cun primo e as variables do estado actual escríbense sen primo. No caso do algoritmo euclidiano, estaremos tratando a disxunción de dúas fórmulas, nunha das cales x é o maior valor, e no segundo - y:
No primeiro caso, o novo valor de y é igual ao valor anterior de y, e obtemos o novo valor de x restando a variable máis pequena da maior. No segundo caso, facemos o contrario.
Volvamos ao algoritmo euclidiano. Supoña de novo que M = 12, N = 18. Isto define un único estado inicial, (x = 12) ∧ (y = 18). Despois conectamos estes valores á fórmula anterior e obtemos:
Aquí está a única solución posible: x' = 18 - 12 ∧ y' = 12, e obtemos o comportamento: [x = 12, y = 18]. Do mesmo xeito, podemos describir todos os estados do noso comportamento: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
En último estado [x = 6, y = 6] ambas partes da expresión serán falsas, polo que non ten un estado seguinte. Entón, temos unha especificación completa do segundo paso; como vemos, trátase dunha matemática bastante común, como a dos enxeñeiros e científicos, e non estraña, como na informática.
Estas dúas fórmulas pódense combinar nunha soa fórmula de lóxica temporal. É elegante e fácil de explicar, pero agora non hai tempo para iso. Pode que necesitemos a lóxica temporal só para a propiedade da vivacidade; para a seguridade non é necesaria. Non me gusta a lóxica temporal como tal, non son matemáticas do todo correntes, pero no caso da vivacidade é un mal necesario.
En algoritmo euclidiano para cada valor x и y hai valores únicos x' и y', que fan verdadeira a relación co seguinte estado. Noutras palabras, o algoritmo euclidiano é determinista. Para modelar un algoritmo non determinista, o estado actual debe ter varios estados futuros posibles e cada valor da variable non cebada debe ter varios valores da variable cebada de xeito que a relación co seguinte estado sexa verdadeira. Isto non é difícil de facer, pero agora non vou poñer exemplos.
Para facer unha ferramenta de traballo, necesitas matemáticas formais. Como facer unha especificación formal? Para iso necesitaremos unha linguaxe formal, p. . A especificación do algoritmo euclidiano nesta linguaxe será así:
O símbolo de signo de igual cun triángulo significa que o valor á esquerda do signo determínase que é igual ao valor á dereita do signo. En esencia, unha especificación é unha definición, no noso caso dúas definicións. Á especificación en TLA+ cómpre engadir declaracións e algunha sintaxe, como na diapositiva anterior. En ASCII quedaría así:
Como vedes, nada complicado. A especificación en TLA+ pódese verificar, é dicir, é posible evitar todos os comportamentos posibles nun modelo pequeno. No noso caso, este modelo será determinados valores M и N. Este é un método de verificación moi eficaz e sinxelo que é completamente automático. Ademais, é posible escribir probas formais de verdade e verificalas mecánicamente, pero isto leva moito tempo, polo que case ninguén o fai.
A principal desvantaxe de TLA+ é que son matemáticas, e os programadores e os informáticos teñen medo ás matemáticas. A primeira vista parece unha broma, pero, por desgraza, dígoo con toda seriedade. Un compañeiro meu só estaba a dicirme como tentou explicar TLA+ a varios desenvolvedores. Axiña que as fórmulas apareceron na pantalla, os seus ollos volvéronse inmediatamente vítreos. Entón, se TLA+ dá medo, podes usar , é unha especie de linguaxe de programación de xoguetes. Unha expresión en PlusCal pode ser calquera expresión TLA+, é dicir, basicamente calquera expresión matemática. Ademais, PlusCal ten sintaxe para algoritmos non deterministas. Debido a que PlusCal pode escribir calquera expresión TLA+, é significativamente máis expresiva que calquera linguaxe de programación real. A continuación, PlusCal compílase nunha especificación TLA+ de fácil lectura. Isto non significa, por suposto, que a complexa especificación PlusCal se converta nunha sinxela en TLA+; só que a correspondencia entre elas é obvia, non aparecerá ningunha complexidade adicional. Finalmente, esta especificación pódese verificar mediante ferramentas TLA+. En xeral, PlusCal pode axudar a superar unha fobia ás matemáticas; é fácil de entender incluso para programadores e informáticos. Publiquei algoritmos sobre el durante algún tempo (uns 10 anos) no pasado.
Quizais alguén opoña que TLA+ e PlusCal son matemáticas, e que as matemáticas só funcionan con exemplos feitos. Na práctica, necesitas unha linguaxe real con tipos, procedementos, obxectos, etc. Isto está mal. Isto é o que Chris Newcomb, que traballou en Amazon, escribe: "Utilizamos TLA+ en dez grandes proxectos e, en todos os casos, o seu uso fixo unha diferenza significativa no desenvolvemento porque puidemos detectar erros perigosos antes de que chegasen á produción e porque nos deu a visión e a confianza que necesitábamos para ser agresivos. optimizacións de rendemento sen influír na verdade do programa". Moitas veces podes escoitar que cando usamos métodos formais obtemos código ineficiente; na práctica, todo é exactamente o contrario. Ademais, existe a percepción de que os xestores non poden ser convencidos da necesidade de métodos formais, aínda que os programadores estean convencidos da súa utilidade. E Newcomb escribe: "Os xestores están agora presionando de todos os xeitos posibles para escribir especificacións en TLA+, e están destinando específicamente tempo para iso". Entón, cando os xestores ven que TLA+ funciona, acéptano. Chris Newcomb escribiu isto hai uns seis meses (outubro de 2014), pero agora, polo que sei, TLA+ úsase en 14 proxectos, non en 10. Outro exemplo refírese ao deseño da XBox 360. Un pasante chegou a Charles Thacker e escribiu especificacións para o sistema de memoria. Grazas a esta especificación, atopouse un erro que doutro xeito non se detectaría e que provocaría que todas as XBox 360 fallasen despois de catro horas de uso. Os enxeñeiros de IBM confirmaron que as súas probas non detectarían este erro.
Podes ler máis sobre TLA+ en Internet, pero agora imos falar de especificacións informais. Poucas veces temos que escribir programas que calculen o mínimo común divisor e similares. Con moita máis frecuencia escribimos programas como a ferramenta de impresora bonita que escribín para TLA+. Despois do procesamento máis sinxelo, o código TLA+ quedaría así:
Pero no exemplo anterior, o usuario probablemente quixese aliñar a conxunción e os signos de igualdade. Polo tanto, o formato correcto sería máis como o seguinte:
Considere outro exemplo:
Aquí, pola contra, o aliñamento dos signos iguais, a suma e a multiplicación na fonte foi aleatoria, polo que o procesamento máis sinxelo é suficiente. En xeral, non existe unha definición matemática exacta do formato correcto, porque "correcto" neste caso significa "o que quere o usuario", e isto non se pode determinar matematicamente.
Parece que se non temos unha definición de verdade, entón a especificación é inútil. Pero iso non é certo. O feito de que non saibamos o que debe facer un programa non significa que non teñamos que pensar en como debería funcionar; pola contra, deberíamos esforzarnos aínda máis. A especificación é especialmente importante aquí. É imposible determinar o programa óptimo para a impresión estruturada, pero isto non significa que non debamos asumilo en absoluto, e escribir código como un fluxo de conciencia non é o caso. Acabei escribindo unha especificación de seis regras con definicións en forma de comentarios nun ficheiro Java. Aquí tes un exemplo dunha das regras: a left-comment token is LeftComment aligned with its covering token. Esta regra está escrita, digamos, en inglés matemático: LeftComment aligned, left-comment и covering token - termos con definicións. Así describen as matemáticas os matemáticos: escriben definicións de termos e, a partir delas, crean regras. O beneficio desta especificación é que seis regras son moito máis fáciles de entender e depurar que 850 liñas de código. Debo dicir que escribir estas regras non foi doado; levou moito tempo depuralas. Escribín código especificamente para este fin que me indicaba que regra se estaba a usar. Debido a que probei estas seis regras con algúns exemplos, non tiven que depurar 850 liñas de código e os erros eran bastante fáciles de atopar. Java ten excelentes ferramentas para iso. Se acabase de escribir o código, tardaría moito máis tempo e o formato sería de peor calidade.
Por que non se puido utilizar unha especificación formal? Por unha banda, a correcta execución non é demasiado importante aquí. Unha impresión estruturada seguramente non será satisfactoria para algúns, polo que non tiven que facelo funcionar correctamente en todas as situacións pouco habituais. Aínda máis importante é o feito de non contar coas ferramentas adecuadas. O comprobador de modelos TLA+ é inútil aquí, polo que tería que escribir os exemplos a man.
A especificación dada ten características comúns a todas as especificacións. É de nivel superior ao código. Pódese implementar en calquera idioma. Non hai ferramentas nin métodos para escribilo. Ningún curso de programación che axudará a escribir esta especificación. E non hai ferramentas que poidan facer que esta especificación sexa innecesaria, a non ser que estea escribindo unha linguaxe específicamente para escribir programas de impresión estruturada en TLA+. Finalmente, esta especificación non di nada sobre como escribiremos exactamente o código, só indica o que fai o código. Escribimos unha especificación para axudarnos a pensar o problema antes de comezar a pensar no código.
Pero esta especificación tamén ten características que a distinguen doutras especificacións. O 95% doutras especificacións son moito máis curtas e sinxelas:
Ademais, esta especificación é un conxunto de regras. Isto xeralmente é un sinal dunha especificación deficiente. Comprender as consecuencias dun conxunto de regras é bastante difícil, polo que tiven que pasar moito tempo depurándoas. Non obstante, neste caso non puiden atopar un xeito mellor.
Paga a pena dicir algunhas palabras sobre os programas que se executan continuamente. Normalmente funcionan en paralelo, como sistemas operativos ou sistemas distribuídos. Moi poucas persoas poden entendelos na súa mente ou no papel, e eu non son un deles, aínda que noutro tempo puiden facelo. Polo tanto, necesitamos ferramentas que comprobarán o noso traballo, por exemplo, TLA+ ou PlusCal.
Por que teño que escribir unha especificación se xa sabía o que debería facer o código? De feito, só pensaba que o sabía. Ademais, cunha especificación establecida, un forasteiro xa non necesita mirar o código para comprender o que fai exactamente. Teño unha regra: non debería haber regras xerais. Hai unha excepción a esta regra, por suposto, esta é a única regra xeral que sigo: a especificación do que fai o código debería dicirlle á xente todo o que precisa saber cando usa ese código.
Entón, que precisan saber exactamente os programadores sobre o pensamento? Para comezar, o mesmo que para todos: se non escribes, só che parece que estás pensando. Ademais, debes pensar antes de codificar, o que significa que debes escribir antes de codificar. Unha especificación é o que escribimos antes de comezar a codificar. Precísase unha especificación para calquera código que poida ser usado ou modificado por calquera. E este "alguén" pode resultar ser o autor do código un mes despois de que fose escrito. Precísase unha especificación para programas e sistemas grandes, para clases, para métodos e, ás veces, incluso para seccións complexas dun só método. Que debes escribir exactamente sobre o código? Cómpre describir o que fai, é dicir, algo que pode ser útil para quen use este código. Ás veces tamén pode ser necesario especificar como o código consegue exactamente o seu obxectivo. Se pasamos por este método no curso de algoritmos, entón chamámoslle algoritmo. Se é algo máis especializado e novo, entón chamámoslle deseño de alto nivel. Non hai ningunha diferenza formal aquí: ambos son modelos abstractos do programa.
Como debería escribir exactamente unha especificación de código? O principal: debería ser un nivel máis alto que o propio código. Debe describir estados e comportamentos. Debe ser tan estrito como o requira a tarefa. Se está a escribir unha especificación de como implementar unha tarefa, pódese escribir en pseudocódigo ou usando PlusCal. Debes aprender a escribir especificacións utilizando especificacións formais. Isto darache as habilidades necesarias que tamén axudarán coas informais. Como podes aprender a escribir especificacións formais? Cando aprendemos a programar, escribimos programas e despois depurábaos. Aquí o mesmo: cómpre escribir unha especificación, comprobalo cun comprobador de modelos e corrixir os erros. Quizais TLA+ non sexa o mellor idioma para unha especificación formal, e é probable que outro idioma sexa máis adecuado para as túas necesidades específicas. O gran de TLA+ é que fai un gran traballo para ensinar o pensamento matemático.
Como vincular especificación e código? Utilizar comentarios que vinculen conceptos matemáticos e a súa implementación. Se traballas con gráficos, a nivel de programa terás matrices de nodos e matrices de ligazóns. Polo tanto, cómpre escribir como se implementa exactamente o gráfico por estas estruturas de programación.
Nótese que ningún dos anteriores se aplica ao proceso de escritura de código en si. Cando escribes código, é dicir, realizas o terceiro paso, tamén tes que pensar e pensar no programa. Se unha subtarefa resulta complexa ou non é obvia, debes escribir unha especificación para ela. Pero non estou falando do propio código aquí. Podes usar calquera linguaxe de programación, calquera metodoloxía, non se trata deles. Ademais, ningunha das anteriores elimina a necesidade de probar e depurar o seu código. Aínda que o modelo abstracto estea escrito correctamente, pode haber erros na súa implementación.
Escribir especificacións é un paso adicional no proceso de codificación. Grazas a el, pódense detectar moitos erros con menos esforzo; sámolo pola experiencia dos programadores de Amazon. Coas especificacións, a calidade dos programas faise maior. Entón, por que adoitamos ir sen eles? Porque escribir é difícil. Pero escribir é difícil, porque para iso hai que pensar, e pensar tamén é difícil. Sempre é máis fácil finxir que estás pensando. Aquí pódese facer unha analoxía con correr: canto menos corres, máis lento corres. Debes adestrar os teus músculos e practicar a escritura. Fai falta práctica.
A especificación pode ser incorrecta. É posible que cometeches un erro nalgún lugar, que os requisitos cambiaron ou que haxa que facer unha mellora. Calquera código que use alguén ten que ser cambiado, polo que tarde ou cedo a especificación xa non coincidirá co programa. Idealmente, neste caso, cómpre escribir unha nova especificación e reescribir completamente o código. Sabemos moi ben que ninguén fai isto. Na práctica, parcheamos o código e quizais actualizamos a especificación. Se isto ocorrerá tarde ou cedo, entón por que escribir especificacións? En primeiro lugar, para a persoa que editará o teu código, cada palabra extra na especificación valerá o seu peso en ouro, e esta persoa pode ser ti. Moitas veces me pateo por non ser o suficientemente específico cando edito o meu código. E escribo máis especificacións que código. Polo tanto, cando editas o código, sempre hai que actualizar a especificación. En segundo lugar, con cada edición o código empeora, faise máis difícil de ler e manter. Este é un aumento da entropía. Pero se non comeza cunha especificación, cada liña que escriba será unha edición e o código será voluminoso e difícil de ler desde o principio.
Como dixo , non se gañou ningunha batalla segundo un plan, e non se gañou ningunha batalla sen un plan. E sabía algo das batallas. Hai unha opinión de que escribir especificacións é unha perda de tempo. Ás veces isto é certo, e a tarefa é tan sinxela que non ten sentido pensalo ben. Pero sempre debes lembrar que cando se lle aconsella non escribir especificacións, significa que se lle aconsella non pensar. E deberías pensar nisto cada vez. Pensar nunha tarefa non garante que non cometerás erros. Como sabemos, ninguén inventou unha variña máxica, e a programación é unha tarefa difícil. Pero se non pensas na tarefa, tes a garantía de cometer erros.
Podes ler máis sobre TLA+ e PlusCal nun sitio web especial, podes ir alí desde a miña páxina de inicio . Iso é todo para min, grazas pola túa atención.
Lembra que esta é unha tradución. Cando escribas comentarios, lembra que o autor non os lerá. Se realmente queres conversar co autor, estará na conferencia Hydra 2019, que se celebrará do 11 ao 12 de xullo de 2019 en San Petersburgo. As entradas pódense mercar .
Fonte: www.habr.com