Este artículo es una traducción. . Pero antes de ella una pequeña introducción. ¿Cómo se forman los zombis? Todos se metieron en una situación en la que quieren llevar a un amigo o colega a su nivel, pero no funciona. Y no es tanto contigo como con él que “no sale”: de un lado de la balanza está el salario normal, tareas, etcétera, y del otro, la necesidad de pensar. Pensar es desagradable y doloroso. Rápidamente se da por vencido y continúa escribiendo código sin encender su cerebro en absoluto. Te imaginas cuánto esfuerzo se necesita para superar la barrera de la indefensión aprendida, y simplemente no lo haces. Así se forman los zombis que, al parecer, se pueden curar, pero parece que nadie lo hará.
cuando vi eso (sí, el mismo camarada de los libros de texto) y no hace un informe, sino una sesión de preguntas y respuestas, estaba un poco cauteloso. Por si acaso, Leslie es un científico de fama mundial, autor de trabajos fundamentales en computación distribuida, y también puede conocerlo por las letras La en la palabra LaTeX - "Lamport TeX". El segundo factor alarmante es su requisito: todos los que vienen deben (absolutamente gratis) escuchar un par de sus informes por adelantado, formular al menos una pregunta sobre ellos y solo entonces venir. Decidí ver lo que Lamport estaba transmitiendo allí, ¡y es genial! Es exactamente eso, la píldora mágica para curar zombis. Os advierto: del texto, los amantes de las metodologías superflexibles y aquellos a los que no les gusta poner a prueba lo escrito pueden quemarse notablemente.
Después de habrokat, de hecho, comienza la traducción del seminario. ¡Disfruta leyendo!
Cualquiera que sea la tarea que asuma, siempre debe seguir tres pasos:
- decide qué objetivo quieres lograr;
- decidir cómo logrará su objetivo;
- ven a tu meta.
Esto también se aplica a la programación. Cuando escribimos código, necesitamos:
- decidir qué debe hacer el programa;
- determinar cómo debe realizar su tarea;
- escribir el código correspondiente.
El último paso, por supuesto, es muy importante, pero no hablaré de eso hoy. En cambio, discutiremos los dos primeros. Todo programador las realiza antes de empezar a trabajar. No te sientas a escribir a menos que hayas decidido si estás escribiendo un navegador o una base de datos. Una cierta idea de la meta debe estar presente. Y definitivamente piensa en qué hará exactamente el programa, y no escribe de alguna manera con la esperanza de que el código se convierta de alguna manera en un navegador.
¿Cómo sucede exactamente este pensamiento previo del código? ¿Cuánto esfuerzo debemos poner en esto? Todo depende de cuán complejo sea el problema que estemos resolviendo. Supongamos que queremos escribir un sistema distribuido tolerante a fallas. En este caso, debemos pensar las cosas detenidamente antes de sentarnos a codificar. ¿Qué pasa si solo necesitamos incrementar una variable entera en 1? A primera vista, aquí todo es trivial y no se necesita pensar, pero luego recordamos que puede ocurrir un desbordamiento. Por lo tanto, incluso para comprender si un problema es simple o complejo, primero debe pensar.
Si piensa de antemano en posibles soluciones al problema, puede evitar errores. Pero esto requiere que tu pensamiento sea claro. Para lograr esto, necesitas escribir tus pensamientos. Me gusta mucho la cita de Dick Guindon: “Cuando escribes, la naturaleza te muestra cuán descuidado es tu pensamiento”. Si no escribes, sólo piensas que estás pensando. Y necesita escribir sus pensamientos en forma de especificaciones.
Las especificaciones realizan muchas funciones, especialmente en proyectos grandes. Pero solo hablaré de uno de ellos: nos ayudan a pensar con claridad. Pensar con claridad es muy importante y bastante difícil, por lo que aquí necesitamos ayuda. ¿En qué idioma debemos escribir las especificaciones? En general, esta es siempre la primera pregunta para los programadores: en qué lenguaje escribiremos. No hay una respuesta correcta: los problemas que estamos resolviendo son demasiado diversos. Para algunos, TLA+ es un lenguaje de especificación que desarrollé. Para otros, es más conveniente usar chino. Todo depende de la situación.
Más importante es otra pregunta: ¿cómo lograr un pensamiento más claro? Respuesta: Debemos pensar como científicos. Esta es una forma de pensar que ha demostrado su eficacia durante los últimos 500 años. En ciencia, construimos modelos matemáticos de la realidad. La astronomía fue quizás la primera ciencia en el sentido estricto de la palabra. En el modelo matemático utilizado en astronomía, los cuerpos celestes aparecen como puntos con masa, posición y momento, aunque en realidad son objetos extremadamente complejos con montañas y océanos, mareas y mareas. Este modelo, como cualquier otro, fue creado para resolver ciertos problemas. Es excelente para determinar hacia dónde apuntar el telescopio si necesita encontrar un planeta. Pero si quieres predecir el tiempo en este planeta, este modelo no funcionará.
Las matemáticas nos permiten determinar las propiedades de un modelo. Y la ciencia muestra cómo estas propiedades se relacionan con la realidad. Hablemos de nuestra ciencia, la informática. La realidad con la que trabajamos son sistemas informáticos de diversa índole: procesadores, videoconsolas, ordenadores, programas de ejecución, etc. Hablaré sobre ejecutar un programa en una computadora, pero en general, todas estas conclusiones se aplican a cualquier sistema informático. En nuestra ciencia, usamos muchos modelos diferentes: la máquina de Turing, conjuntos de eventos parcialmente ordenados y muchos otros.
¿Qué es un programa? Este es cualquier código que se puede considerar de forma independiente. Supongamos que necesitamos escribir un navegador. Realizamos tres tareas: diseñamos la vista del usuario del programa, luego escribimos el diagrama de alto nivel del programa y finalmente escribimos el código. A medida que escribimos el código, nos damos cuenta de que necesitamos escribir un formateador de texto. Aquí nuevamente necesitamos resolver tres problemas: determinar qué texto devolverá esta herramienta; seleccione un algoritmo para formatear; escribir código. Esta tarea tiene su propia subtarea: insertar correctamente un guión en las palabras. También resolvemos esta subtarea en tres pasos; como puede ver, se repiten en muchos niveles.
Consideremos con más detalle el primer paso: qué problema resuelve el programa. Aquí, generalmente modelamos un programa como una función que toma alguna entrada y produce alguna salida. En matemáticas, una función suele describirse como un conjunto ordenado de pares. Por ejemplo, la función de elevar al cuadrado los números naturales se describe como el conjunto {<0,0>, <1,1>, <2,4>, <3,9>, …}. El dominio de tal función es el conjunto de los primeros elementos de cada par, es decir, los números naturales. Para definir una función, necesitamos especificar su alcance y fórmula.
Pero las funciones en matemáticas no son lo mismo que las funciones en los lenguajes de programación. Las matemáticas son mucho más fáciles. Como no tengo tiempo para ejemplos complejos, consideremos uno simple: una función en C o un método estático en Java que devuelva el máximo común divisor de dos enteros. En la especificación de este método, escribiremos: calcula GCD(M,N) para argumentos M и NDonde GCD(M,N) - una función cuyo dominio es el conjunto de pares de enteros, y el valor de retorno es el entero más grande que es divisible por M и N. ¿Cómo se relaciona este modelo con la realidad? El modelo opera en números enteros, mientras que en C o Java tenemos un modelo de 32 bits. int. Este modelo nos permite decidir si el algoritmo es correcto GCD, pero no evitará errores de desbordamiento. Esto requeriría un modelo más complejo, para el que no hay tiempo.
Hablemos de las limitaciones de una función como modelo. Algunos programas (como los sistemas operativos) no solo devuelven un cierto valor para ciertos argumentos, sino que pueden ejecutarse continuamente. Además, la función como modelo no es adecuada para el segundo paso: planificar cómo resolver el problema. La ordenación rápida y la ordenación de burbujas calculan la misma función, pero son algoritmos completamente diferentes. Por lo tanto, para describir cómo se logra el objetivo del programa, utilizo un modelo diferente, llamémoslo modelo de comportamiento estándar. El programa en él se representa como un conjunto de todos los comportamientos permitidos, cada uno de los cuales, a su vez, es una secuencia de estados, y el estado es la asignación de valores a las variables.
Veamos cómo sería el segundo paso del algoritmo de Euclides. tenemos que calcular GCD(M, N). Inicializamos M cómo xY N cómo y, luego reste repetidamente la menor de estas variables de la mayor hasta que sean iguales. Por ejemplo, si M = 12Y N = 18, podemos describir el siguiente comportamiento:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Y si M = 0 и N = 0? El cero es divisible por todos los números, por lo que en este caso no existe el mayor divisor. En esta situación, debemos volver al primer paso y preguntarnos: ¿realmente necesitamos calcular el GCD para números no positivos? Si esto no es necesario, solo necesita cambiar la especificación.
Aquí deberíamos hacer una pequeña digresión sobre la productividad. A menudo se mide en la cantidad de líneas de código escritas por día. Pero su trabajo es mucho más útil si se deshace de un cierto número de líneas, porque tiene menos espacio para errores. Y la forma más fácil de deshacerse del código es en el primer paso. Es muy posible que simplemente no necesite todas las campanas y silbatos que está tratando de implementar. La forma más rápida de simplificar un programa y ahorrar tiempo es no hacer cosas que no se deben hacer. El segundo paso es el segundo potencial de mayor ahorro de tiempo. Si mide la productividad en términos de líneas escritas, pensar en cómo realizar una tarea le hará menos productivo, porque puedes resolver el mismo problema con menos código. No puedo dar estadísticas exactas aquí, porque no tengo forma de contar la cantidad de líneas que no escribí debido al hecho de que dediqué tiempo a la especificación, es decir, al primer y segundo paso. Y el experimento tampoco se puede configurar aquí, porque en el experimento no tenemos derecho a completar el primer paso, la tarea está predeterminada.
Es fácil pasar por alto muchas dificultades en las especificaciones informales. No hay nada difícil en escribir especificaciones estrictas para funciones, no discutiré esto. En cambio, hablaremos sobre escribir especificaciones sólidas para comportamientos estándar. Hay un teorema que dice que cualquier conjunto de comportamientos puede describirse usando la propiedad de seguridad (la seguridad) y propiedades de supervivencia (vida). La seguridad significa que no pasará nada malo, el programa no dará una respuesta incorrecta. Supervivencia significa que tarde o temprano sucederá algo bueno, es decir, el programa dará la respuesta correcta tarde o temprano. Como regla general, la seguridad es un indicador más importante, los errores ocurren con mayor frecuencia aquí. Por lo tanto, para ahorrar tiempo, no hablaré sobre la capacidad de supervivencia, aunque, por supuesto, también es importante.
Alcanzamos la seguridad prescribiendo, primero, el conjunto de posibles estados iniciales. Y segundo, las relaciones con todos los próximos estados posibles para cada estado. Actuemos como científicos y definamos estados matemáticamente. El conjunto de estados iniciales se describe mediante una fórmula, por ejemplo, en el caso del algoritmo de Euclides: (x = M) ∧ (y = N). Para ciertos valores M и N sólo hay un estado inicial. La relación con el siguiente estado se describe mediante una fórmula en la que las variables del siguiente estado se escriben con un primo y las variables del estado actual se escriben sin un primo. En el caso del algoritmo de Euclides, nos ocuparemos de la disyunción de dos fórmulas, en una de las cuales x es el valor más grande, y en el segundo - y:
En el primer caso, el nuevo valor de y es igual al valor anterior de y, y obtenemos el nuevo valor de x restando la variable más pequeña de la variable más grande. En el segundo caso, hacemos lo contrario.
Volvamos al algoritmo de Euclides. Supongamos de nuevo que M = 12, N = 18. Esto define un único estado inicial, (x = 12) ∧ (y = 18). Luego conectamos esos valores en la fórmula anterior y obtenemos:
Aquí está la única solución posible: x' = 18 - 12 ∧ y' = 12y obtenemos el comportamiento: [x = 12, y = 18]. Del mismo modo, podemos describir todos los estados de nuestro comportamiento: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
En último estado [x = 6, y = 6] ambas partes de la expresión serán falsas, por lo que no tiene siguiente estado. Entonces, tenemos una especificación completa del segundo paso: como puede ver, se trata de matemáticas bastante ordinarias, como en ingenieros y científicos, y no extrañas, como en informática.
Estas dos fórmulas se pueden combinar en una fórmula de lógica temporal. Es elegante y fácil de explicar, pero ahora no hay tiempo para ella. Es posible que necesitemos lógica temporal solo para la propiedad de vivacidad, no es necesaria para la seguridad. No me gusta la lógica temporal como tal, no es una matemática ordinaria, pero en el caso de la vivacidad es un mal necesario.
En el algoritmo de Euclides, para cada valor x и y tener valores únicos x' и y', que hacen verdadera la relación con el siguiente estado. En otras palabras, el algoritmo de Euclides es determinista. Para modelar un algoritmo no determinista, el estado actual debe tener múltiples estados futuros posibles, y que cada valor de variable sin prima tenga múltiples valores de variable con prima de modo que la relación con el siguiente estado sea verdadera. Esto es fácil de hacer, pero no daré ejemplos ahora.
Para hacer una herramienta de trabajo, necesitas matemáticas formales. ¿Cómo hacer que la especificación sea formal? Para hacer esto, necesitamos un lenguaje formal, por ejemplo, . La especificación del algoritmo de Euclides se vería así en este lenguaje:
Un símbolo de signo igual con un triángulo significa que el valor a la izquierda del signo se define como igual al valor a la derecha del signo. En esencia, la especificación es una definición, en nuestro caso dos definiciones. A la especificación en TLA+, debe agregar declaraciones y algo de sintaxis, como en la diapositiva anterior. En ASCII se vería así:
Como puedes ver, nada complicado. La especificación para TLA+ se puede probar, es decir, omitir todos los comportamientos posibles en un modelo pequeño. En nuestro caso, este modelo tendrá ciertos valores. M и N. Este es un método de verificación muy eficiente y simple que es completamente automático. También es posible escribir pruebas de verdad formales y verificarlas mecánicamente, pero esto lleva mucho tiempo, por lo que casi nadie lo hace.
La principal desventaja de TLA+ es que es matemática, y los programadores e informáticos tienen miedo de las matemáticas. A primera vista, esto suena como una broma, pero, desafortunadamente, lo digo en serio. Mi colega me estaba contando cómo trató de explicar TLA+ a varios desarrolladores. Tan pronto como aparecieron las fórmulas en la pantalla, inmediatamente se convirtieron en ojos vidriosos. Entonces, si TLA+ te asusta, puedes usar , es una especie de lenguaje de programación de juguete. Una expresión en PlusCal puede ser cualquier expresión TLA+, es decir, en general, cualquier expresión matemática. Además, PlusCal tiene una sintaxis para algoritmos no deterministas. Como PlusCal puede escribir cualquier expresión TLA+, PlusCal es mucho más expresivo que cualquier lenguaje de programación real. A continuación, PlusCal se compila en una especificación TLA+ de fácil lectura. Esto no significa, por supuesto, que la especificación PlusCal compleja se convertirá en una simple en TLA +; solo la correspondencia entre ellos es obvia, no habrá complejidad adicional. Finalmente, esta especificación puede ser verificada por las herramientas TLA+. Con todo, PlusCal puede ayudar a superar la fobia a las matemáticas y es fácil de entender incluso para programadores e informáticos. En el pasado, publiqué algoritmos durante algún tiempo (alrededor de 10 años).
Quizás alguien objete que TLA+ y PlusCal son matemáticas, y las matemáticas solo funcionan con ejemplos inventados. En la práctica, necesita un lenguaje real con tipos, procedimientos, objetos, etc. Esto está mal. Esto es lo que escribe Chris Newcomb, que trabajó en Amazon: “Utilizamos TLA+ en diez proyectos importantes y, en cada caso, su uso marcó una diferencia significativa en el desarrollo porque pudimos detectar errores peligrosos antes de comenzar la producción y porque nos dio la perspectiva y la confianza que necesitábamos para realizar optimizaciones de rendimiento agresivas sin afectar la verdad del programa". A menudo puede escuchar que cuando usamos métodos formales, obtenemos un código ineficiente; en la práctica, todo es exactamente lo contrario. Además, existe la opinión de que los gerentes no pueden estar convencidos de la necesidad de métodos formales, incluso si los programadores están convencidos de su utilidad. Y Newcomb escribe: “Los gerentes ahora están presionando para escribir especificaciones para TLA + y específicamente asignar tiempo para esto”. Entonces, cuando los gerentes ven que TLA+ está funcionando, lo aceptan con gusto. Chris Newcomb escribió esto hace unos seis meses (octubre de 2014), pero ahora, que yo sepa, TLA+ se usa en 14 proyectos, no en 10. Otro ejemplo se relaciona con el diseño de XBox 360. Un pasante acudió a Charles Thacker y escribió la especificación para el sistema de memoria. Gracias a esta especificación, se encontró un error que de otro modo pasaría desapercibido y por el cual cada XBox 360 fallaría después de cuatro horas de uso. Los ingenieros de IBM confirmaron que sus pruebas no habrían encontrado este error.
Puede leer más sobre TLA+ en Internet, pero ahora hablemos de especificaciones informales. Rara vez tenemos que escribir programas que calculen el mínimo común divisor y cosas por el estilo. Con mucha más frecuencia escribimos programas como la herramienta pretty-printer que escribí para TLA+. Después del procesamiento más simple, el código TLA+ se vería así:
Pero en el ejemplo anterior, lo más probable es que el usuario quisiera alinear la conjunción y los signos iguales. Entonces, el formato correcto se vería más así:
Considere otro ejemplo:
Aquí, por el contrario, la alineación de los signos de igual, suma y multiplicación en la fuente fue aleatoria, por lo que el procesamiento más simple es suficiente. En general, no existe una definición matemática exacta de formato correcto, porque "correcto" en este caso significa "lo que el usuario quiere", y esto no se puede determinar matemáticamente.
Parecería que si no tenemos una definición de verdad, entonces la especificación es inútil. Pero no lo es. El hecho de que no sepamos lo que se supone que debe hacer un programa no significa que no necesitemos pensar en cómo funciona; al contrario, tenemos que poner aún más esfuerzo en él. La especificación es especialmente importante aquí. Es imposible determinar el programa óptimo para la impresión estructurada, pero esto no significa que no debamos tomarlo en absoluto, y escribir código como una corriente de conciencia no es algo bueno. Al final, escribí una especificación de seis reglas con definiciones en forma de comentarios en un archivo java. Aquí hay un ejemplo de una de las reglas: a left-comment token is LeftComment aligned with its covering token. Esta regla está escrita, digamos, en inglés matemático: LeftComment aligned, left-comment и covering token - términos con definiciones. Así es como los matemáticos describen las matemáticas: escriben definiciones de términos y, en base a ellos, reglas. El beneficio de tal especificación es que seis reglas son mucho más fáciles de entender y depurar que 850 líneas de código. Debo decir que escribir estas reglas no fue fácil, llevó bastante tiempo depurarlas. Especialmente para este propósito, escribí un código que informaba qué regla se usaba. Gracias al hecho de que probé estas seis reglas en varios ejemplos, no tuve que depurar 850 líneas de código y los errores resultaron ser bastante fáciles de encontrar. Java tiene grandes herramientas para esto. Si solo hubiera escrito el código, me habría llevado mucho más tiempo y el formato habría sido de peor calidad.
¿Por qué no se puede utilizar una especificación formal? Por un lado, la correcta ejecución aquí no es demasiado importante. Las impresiones estructurales seguramente no complacerán a nadie, por lo que no tuve que hacer que funcionara bien en todas las situaciones extrañas. Aún más importante es el hecho de que no tenía las herramientas adecuadas. El verificador de modelos TLA+ es inútil aquí, por lo que tendría que escribir manualmente los ejemplos.
La especificación anterior tiene características comunes a todas las especificaciones. Es un nivel más alto que el código. Se puede implementar en cualquier idioma. Cualquier herramienta o método es inútil para escribirlo. Ningún curso de programación le ayudará a escribir esta especificación. Y no existen herramientas que puedan hacer innecesaria esta especificación, a menos, por supuesto, que esté escribiendo un lenguaje específicamente para escribir programas de impresión estructurada en TLA+. Finalmente, esta especificación no dice nada sobre exactamente cómo escribiremos el código, solo establece lo que hace el código. Escribimos la especificación para ayudarnos a pensar en el problema antes de comenzar a pensar en el código.
Pero esta especificación también tiene características que la distinguen de otras especificaciones. El 95% de otras especificaciones son significativamente más cortas y simples:
Además, esta especificación es un conjunto de reglas. Como regla general, esto es un signo de mala especificación. Comprender las consecuencias de un conjunto de reglas es bastante difícil, por lo que tuve que dedicar mucho tiempo a depurarlas. Sin embargo, en este caso, no pude encontrar una mejor manera.
Vale la pena decir algunas palabras sobre los programas que se ejecutan continuamente. Por regla general, funcionan en paralelo, por ejemplo, sistemas operativos o sistemas distribuidos. Muy pocas personas pueden entenderlos mentalmente o en papel, y yo no soy uno de ellos, aunque alguna vez pude hacerlo. Por lo tanto, necesitamos herramientas que verifiquen nuestro trabajo, por ejemplo, TLA + o PlusCal.
¿Por qué era necesario escribir una especificación si ya sabía qué debía hacer exactamente el código? De hecho, pensé que lo sabía. Además, con una especificación, una persona ajena ya no necesita ingresar al código para comprender qué es exactamente lo que hace. Tengo una regla: no debería haber reglas generales. Hay una excepción a esta regla, por supuesto, es la única regla general que sigo: la especificación de lo que hace el código debe decirle a la gente todo lo que necesitan saber al usar el código.
Entonces, ¿qué necesitan saber exactamente los programadores sobre el pensamiento? Para empezar, lo mismo que todos los demás: si no escribes, entonces solo te parece que estás pensando. Además, debe pensar antes de codificar, lo que significa que debe escribir antes de codificar. La especificación es lo que escribimos antes de comenzar a codificar. Se necesita una especificación para cualquier código que cualquiera pueda usar o modificar. Y este "alguien" puede ser el propio autor del código un mes después de haberlo escrito. Se necesita una especificación para programas y sistemas grandes, para clases, para métodos y, a veces, incluso para secciones complejas de un solo método. ¿Qué debería escribirse exactamente sobre el código? Debe describir lo que hace, es decir, lo que puede ser útil para cualquier persona que use este código. A veces también puede ser necesario especificar cómo el código logra su propósito. Si pasamos por este método en el curso de algoritmos, entonces lo llamamos algoritmo. Si es algo más especial y nuevo, lo llamamos diseño de alto nivel. No hay diferencia formal aquí: ambos son un modelo abstracto de un programa.
¿Cómo se debe escribir exactamente una especificación de código? Lo principal: debe ser un nivel más alto que el código en sí. Debe describir estados y comportamientos. Debe ser tan estricto como lo requiera la tarea. Si está escribiendo una especificación sobre cómo se implementará una tarea, puede escribirla en pseudocódigo o con PlusCal. Debe aprender a escribir especificaciones sobre especificaciones formales. Esto te dará las habilidades necesarias que también te ayudarán con las informales. ¿Cómo se aprende a escribir especificaciones formales? Cuando aprendimos a programar, escribimos programas y luego los depuramos. Es lo mismo aquí: escriba la especificación, verifíquela con el verificador de modelos y corrija los errores. Es posible que TLA+ no sea el mejor lenguaje para una especificación formal y es probable que otro lenguaje sea mejor para sus necesidades específicas. La ventaja de TLA+ es que enseña muy bien el pensamiento matemático.
¿Cómo vincular la especificación y el código? Con la ayuda de comentarios que vinculan conceptos matemáticos y su implementación. Si trabaja con gráficos, a nivel de programa tendrá matrices de nodos y matrices de enlaces. Por lo tanto, debe escribir exactamente cómo se implementa el gráfico mediante estas estructuras de programación.
Cabe señalar que nada de lo anterior se aplica al proceso real de escribir código. Cuando escribe el código, es decir, realiza el tercer paso, también necesita pensar y pensar en el programa. Si una subtarea resulta ser compleja o no obvia, debe escribir una especificación para ella. Pero no estoy hablando del código en sí aquí. Puedes usar cualquier lenguaje de programación, cualquier metodología, no se trata de ellos. Además, nada de lo anterior elimina la necesidad de probar y depurar el código. Incluso si el modelo abstracto está escrito correctamente, puede haber errores en su implementación.
Escribir especificaciones es un paso adicional en el proceso de codificación. Gracias a él, se pueden detectar muchos errores con menos esfuerzo; lo sabemos por la experiencia de los programadores de Amazon. Con las especificaciones, la calidad de los programas aumenta. Entonces, ¿por qué, entonces, pasamos tan a menudo sin ellos? Porque escribir es difícil. Y escribir es difícil, porque para eso hay que pensar, y pensar también es difícil. Siempre es más fácil fingir lo que piensas. Aquí puedes hacer una analogía con correr: cuanto menos corres, más lento corres. Necesitas entrenar tus músculos y practicar la escritura. Necesita práctica.
La especificación puede ser incorrecta. Es posible que haya cometido un error en alguna parte, que los requisitos hayan cambiado o que sea necesario realizar una mejora. Cualquier código que alguien use debe cambiarse, por lo que tarde o temprano la especificación ya no coincidirá con el programa. Idealmente, en este caso, debe escribir una nueva especificación y reescribir completamente el código. Sabemos muy bien que nadie hace eso. En la práctica, parcheamos el código y posiblemente actualizamos la especificación. Si esto va a suceder tarde o temprano, ¿por qué escribir especificaciones? En primer lugar, para la persona que editará su código, cada palabra adicional en la especificación valdrá su peso en oro, y esta persona bien puede ser usted mismo. A menudo me regaño a mí mismo por no obtener suficientes especificaciones cuando estoy editando mi código. Y escribo más especificaciones que código. Por lo tanto, cuando edita el código, la especificación siempre debe actualizarse. En segundo lugar, con cada revisión, el código empeora, se vuelve cada vez más difícil de leer y mantener. Esto es un aumento en la entropía. Pero si no comienza con una especificación, entonces cada línea que escriba será una edición, y el código será difícil de manejar y difícil de leer desde el principio.
Como se dijo , ninguna batalla se ganó con un plan, y ninguna batalla se ganó sin un plan. Y sabía un par de cosas sobre batallas. Existe la opinión de que escribir especificaciones es una pérdida de tiempo. A veces esto es cierto, y la tarea es tan simple que no hay nada que pensar. Pero siempre debe recordar que cuando se le dice que no escriba especificaciones, se le dice que no piense. Y deberías pensar en ello cada vez. Pensar en la tarea no garantiza que no cometerá errores. Como sabemos, nadie inventó la varita mágica y la programación es una tarea difícil. Pero si no piensa en el problema, está garantizado que cometerá errores.
Puede leer más sobre TLA + y PlusCal en un sitio web especial, puede ir allí desde mi página de inicio . Eso es todo para mí, gracias por su atención.
Tenga en cuenta que esto es una traducción. Cuando escriba comentarios, recuerde que el autor no los leerá. Si realmente desea conversar con el autor, estará en la conferencia Hydra 2019, que se llevará a cabo del 11 al 12 de julio de 2019 en San Petersburgo. Los boletos se pueden comprar .
Fuente: habr.com