Este es un artículo de traducción . Pero antes, una breve introducción. ¿Cómo se forman los zombis? Todos hemos estado en la situación en que queremos elevar a un amigo o colega a nuestro nivel, pero no podemos. Y el 'no poder' no es tanto por ti, sino por él: en un lado está un salario normal, tareas, etc., y en el otro – la necesidad de pensar. Pensar es desagradable y doloroso. Él se rinde rápidamente y sigue escribiendo código sin usar la cabeza. Te imaginas cuánta energía se necesita para superar la barrera de la impotencia aprendida y simplemente no lo haces. Así se forman los zombis, que aparentemente se pueden curar, pero a la vez parece que nadie se ocupará de ello.
Cuando vi que (sí, sí, el mismo amigo de los libros de texto) y no daba una conferencia, sino una sesión de preguntas y respuestas, me sentí un poco inquieto. Por si acaso, Leslie es un científico de renombre mundial, autor de trabajos fundamentales en computación distribuida, y también puede que lo conozcan por las letras La en la palabra LaTeX – 'Lamport TeX'. El segundo factor inquietante es su requisito: cada persona que venga debe (totalmente gratis) escuchar un par de sus conferencias de antemano, formular al menos una pregunta sobre ellas y solo entonces asistir. Decidí ver qué decía Lamport, ¡y es magnífico! ¡Es exactamente eso, el enlace mágico que es una pastilla para curar la zombificación! Advierto: el texto puede causar gran malestar a los amantes de las metodologías extremadamente flexibles y a los que no les gusta probar lo que han escrito.
Después del artículo en sí, comienza la traducción del seminario. ¡Feliz lectura!
Cualquiera sea la tarea que emprendas, siempre debes seguir tres pasos:
- definir qué objetivo quieres alcanzar;
- decidir cómo vas a lograr tu objetivo;
- alcanzar tu objetivo.
Esto también se aplica a la programación. Cuando escribimos código, necesitamos:
- determinar qué debe hacer el programa;
- definir cómo debe realizar su tarea;
- escribir el código correspondiente.
El último paso, por supuesto, es muy importante, pero hoy no hablaré de él. En su lugar, discutiremos los dos primeros. Cada programador los realiza antes de comenzar a trabajar. No te sientas a escribir si no has decidido qué exactamente estás escribiendo: un navegador o una base de datos. Debe haber una idea clara del objetivo. Y definitivamente piensas en lo que hará el programa, en lugar de escribir de cualquier manera con la esperanza de que el código se convierta en un navegador por sí mismo.
¿Cómo ocurre exactamente esta planificación preliminar del código? ¿Cuánto esfuerzo deberíamos dedicarle? Todo depende de cuán compleja sea la problemática que estamos resolviendo. Supongamos que queremos escribir un sistema distribuido tolerante a fallos. En este caso, deberíamos pensar en todo detenidamente antes de sentarnos a codificar. ¿Y si solo necesitamos incrementar una variable entera en 1? A primera vista, parece trivial y no requiere reflexión, pero luego recordamos que puede ocurrir un desbordamiento. Por lo tanto, incluso para entender si una pregunta es simple o compleja, primero se debe pensar.
Si se planifican previamente las posibles soluciones a un problema, se pueden evitar errores. Pero para ello es necesario que tu pensamiento sea claro. Para lograr esto, es importante anotar tus pensamientos. Me gusta mucho la cita de Dick Geddes: "Cuando escribes, la naturaleza te muestra cuán desordenado es tu pensamiento". Si no escribes, solo te parece que estás pensando. Y es necesario registrar tus pensamientos en forma de especificaciones.
Las especificaciones cumplen muchas funciones, especialmente en proyectos grandes. Pero solo hablaré de una de ellas: nos ayudan a pensar con claridad. Pensar con claridad es muy importante y bastante difícil, por lo que aquí necesitamos toda la ayuda posible. ¿En qué idioma deberíamos escribir las especificaciones? Esta siempre es la primera pregunta para los programadores: ¿en qué lenguaje vamos a escribir? No hay una respuesta correcta única: los problemas que estamos resolviendo son demasiado diversos. Para algunos, TLA+ es útil: es un lenguaje de especificaciones que yo desarrollé. Para otros, puede ser más cómodo usar chino. Todo depende de la situación.
Hay otra pregunta más importante: ¿cómo lograr un pensamiento más claro? Respuesta: debemos pensar como científicos. Este es un modo de pensar que ha demostrado ser excelente en los últimos 500 años. En la 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 se presentan como puntos con masa, posición y momento, aunque en realidad son objetos extremadamente complejos con montañas y océanos, mareas y flujos. Este modelo, como cualquier otro, fue creado para resolver tareas específicas. Es muy eficaz para determinar hacia dónde debe dirigirse un telescopio si necesitamos encontrar un planeta. Pero si quieres predecir el clima en ese planeta, este modelo no será útil.
Las matemáticas nos permiten definir las propiedades del 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 computacionales de diversos tipos: procesadores, consolas de videojuegos, computadoras que ejecutan programas, y así sucesivamente. Hablaré sobre la ejecución de un programa en una computadora, pero, en términos generales, todas estas conclusiones son aplicables a cualquier sistema computacional. En nuestra ciencia usamos muchos modelos diferentes: la máquina de Turing, conjuntos de eventos parcialmente ordenados, y muchos otros.
¿Qué es un programa? Es cualquier código que se puede considerar de manera independiente. Supongamos que necesitamos escribir un navegador. Realizamos tres tareas: diseñamos la presentación del programa para el usuario, luego escribimos un esquema de alto nivel del programa y, finalmente, escribimos el código. Mientras escribimos el código, nos damos cuenta de que necesitamos crear una herramienta para formatear texto. Aquí nuevamente debemos resolver tres tareas: definir qué texto devolverá esa herramienta; elegir un algoritmo para el formateo; escribir el código. Esta tarea tiene su propia subtarea: insertar correctamente guiones en las palabras. También resolvemos esta subtarea en tres pasos; como podemos ver, se repiten en muchos niveles.
Analicemos más a fondo el primer paso: qué tarea resuelve el programa. Aquí, a menudo modelamos el programa como una función que recibe ciertos datos de entrada y devuelve algunos datos como salida. En matemáticas, una función generalmente se describe como un conjunto ordenado de pares. Por ejemplo, la función que eleva al cuadrado para los números naturales se describe como el conjunto {, , , , ...}. El dominio de esta 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 dominio y su 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 simples. Dado que no tengo tiempo para ejemplos complejos, consideremos uno sencillo: una función en C o un método estático en Java que devuelve el máximo común divisor de dos números enteros. En la especificación de este método, nosotros escribiremos: calcula GCD(M,N) para los argumentos M y N, donde GCD(M,N) — es una función cuyo dominio es el conjunto de pares de números enteros, y el valor devuelto es el mayor número entero que divide M y N. ¿Cómo se relaciona esta modelo con la realidad? El modelo opera con números enteros, mientras que en C o Java tenemos un intde 32 bits. Este modelo nos permite determinar si el algoritmo es correcto GCD, pero no evitará errores de desbordamiento. Para eso se requeriría un modelo más complicado, para el cual no hay tiempo.
Hablemos de las limitaciones de la función como modelo. El funcionamiento de algunos programas (por ejemplo, sistemas operativos) no se reduce a devolver un valor determinado para argumentos específicos; pueden ejecutarse de manera continua. Además, la función como modelo no es adecuada para el segundo paso: planificar la forma de resolver el problema. La ordenación rápida y la ordenación burbuja calculan la misma función, pero son algoritmos completamente diferentes. Por lo tanto, para describir la forma de alcanzar el objetivo del programa, utilizo otro modelo, que llamaremos el modelo de comportamiento estándar. En este, el programa se presenta como un conjunto de todos los comportamientos permitidos, cada uno de los cuales es a su vez una secuencia de estados, y un estado es la asignación de valores a las variables.
Veamos cómo se verá el segundo paso del algoritmo de Euclides. Necesitamos calcular MCD(M, N). Inicializamos M cómo x, y N cómo y, luego restamos repetidamente la menor de estas variables de la mayor hasta que sean iguales. Por ejemplo, si M = 12, y N = 18, podemos describir el siguiente comportamiento:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Y si M = 0 y N = 0? Ноль делится на все числа, поэтому наибольшего делителя в этом случае нет. В этой ситуации нам нужно вернуться к первому шагу и спросить: действительно ли нам нужно вычислять НОД для неположительных чисел? Если в этом нет необходимости, то нужно просто изменить спецификацию.
Aquí es conveniente hacer un pequeño paréntesis sobre la productividad. A menudo se mide por la cantidad de líneas de código escritas en un día. Pero tu trabajo es mucho más valioso si te has deshecho de ciertas líneas, porque hay menos espacio para errores. Y es más fácil deshacerse del código precisamente en el primer paso. Es muy posible que simplemente no necesites todas esas complejidades que intentas implementar. La manera más rápida de simplificar un programa y ahorrar tiempo es no hacer cosas que no valen la pena. El segundo paso ocupa el segundo lugar en potencial para ahorrar tiempo. Si mides la productividad por la cantidad de líneas escritas, pensar en una manera de resolver la tarea te hará menos productivo, ya que podrás resolver la misma tarea con menos código. No puedo proporcionar estadísticas exactas aquí, ya que no tengo forma de contar cuántas líneas no escribí porque perdí tiempo en la especificación, es decir, en los primeros dos pasos. Y tampoco se puede realizar un experimento al respecto, porque en un experimento no tenemos derecho a ejecutar el primer paso, la tarea está definida de antemano.
En las especificaciones informales, a menudo es fácil pasar por alto muchas dificultades. No hay nada complicado en escribir especificaciones estrictas para funciones, no discutiré esto. En su lugar, hablaremos sobre cómo escribir especificaciones estrictas para modelos de comportamiento estándar. Hay un teorema que dice que cualquier conjunto de comportamientos se puede describir mediante la propiedad de seguridad (safety) y la propiedad de vivacidad (liveness). La seguridad significa que no sucederá nada malo, el programa no dará una respuesta incorrecta. La resiliencia significa que tarde o temprano sucederá algo bueno, es decir, el programa dará una respuesta correcta tarde o temprano. Por lo general, la seguridad es un indicador más importante, los errores suelen ocurrir aquí. Por lo tanto, para ahorrar tiempo no hablaré sobre la resiliencia, aunque, por supuesto, también es importante.
Logramos la seguridad describiendo, en primer lugar, una multitud de posibles estados iniciales. Y, en segundo lugar, las relaciones con todos los posibles estados siguientes para cada estado. Nos comportaremos como científicos y definiremos los estados matemáticamente. Un conjunto de estados iniciales se describe con una fórmula, por ejemplo, en el caso del algoritmo de Euclides: (x = M) ∧ (y = N). Para ciertos valores M y N solo existe un estado inicial. La relación con el estado siguiente se describe con una fórmula donde las variables del próximo estado se anotan con una línea, y las del estado actual sin línea. En el caso del algoritmo de Euclides, trataremos con la disyunción de dos fórmulas, en una de las cuales x es el valor máximo, y en la otra, y:
En el primer caso, el nuevo valor de y es igual al valor anterior de y, y el nuevo valor de x lo obtenemos restando la menor variable de la mayor. En el segundo caso, hacemos lo contrario.
Volvamos al algoritmo de Euclides. Supongamos nuevamente que M = 12, N = 18. Esto define un único estado inicial, (x = 12) ∧ (y = 18). Luego sustituimos estos valores en la fórmula anterior y obtenemos:
Aquí la única solución posible es: x' = 18 - 12 ∧ y' = 12, y obtenemos el comportamiento: [x = 12, y = 18]. De la misma manera, podemos describir todos los estados en nuestro comportamiento: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
En el último estado [x = 6, y = 6] ambas partes de la expresión serán falsas, por lo tanto, no tiene un estado siguiente. Así que tenemos una especificación completa del segundo paso: como podemos ver, es matemáticas completamente normales, como en la ingeniería y la ciencia, y no extrañas, como en la informática.
Estas dos fórmulas se pueden combinar en una única fórmula de lógica temporal. Es elegante y no es difícil de explicar, pero no hay tiempo para ello en este momento. La lógica temporal puede ser necesaria solo para la propiedad de vivacidad; no es necesaria para la seguridad. A la lógica temporal en sí no le agrada, ya que no es del todo matemática común, pero en el caso de la vivacidad, es un mal necesario.
En el algoritmo de Euclides para cada valor x y y hay valores únicos x' y y', que hacen que la relación con el siguiente estado sea verdadera. En otras palabras, el algoritmo de Euclides es determinista. Para modelar un algoritmo no determinista, es necesario que el estado actual tenga varios estados futuros posibles, y que cada valor de la variable sin línea tenga varios valores de la variable con línea, en los cuales la relación con el siguiente estado es verdadera. No es difícil de hacer, pero no daré ejemplos ahora.
Para crear una herramienta funcional, se necesita matemáticas formales. ¿Cómo hacer una especificación formal? Para ello, necesitaremos un lenguaje formal, por ejemplo, . La especificación del algoritmo de Euclides se verá de la siguiente manera en este lenguaje:
El símbolo del signo igual con un triángulo significa que el valor a la izquierda del signo está definido como igual al valor a la derecha del signo. Esencialmente, la especificación es una definición, en nuestro caso, dos definiciones. A la especificación en TLA+ hay que añadir declaraciones y cierta sintaxis, como se mostró en la diapositiva anterior. En ASCII se verá así:
Como podemos ver, no hay nada complicado. La especificación en TLA+ se puede verificar, es decir, explorar todos los posibles comportamientos en un pequeño modelo. En nuestro caso, este modelo serán ciertos valores M y N. Este es un método muy eficiente y simple de verificación que se realiza completamente de manera automática. Además, se pueden redactar pruebas formales de veracidad 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 a los programadores y los científicos de la computación les asusta la matemática. A primera vista, esto suena a broma, pero, desafortunadamente, hablo muy en serio. Un colega mío me contaba cómo intentó explicar TLA+ a varios desarrolladores. Tan pronto como aparecieron fórmulas en la pantalla, se les pusieron los ojos en blanco. Así que si TLA+ asusta, se puede usar , es una especie de lenguaje de programación de juguete. Una expresión en PlusCal puede ser cualquier expresión de TLA+, es decir, en términos generales, cualquier expresión matemática. Además, PlusCal tiene una sintaxis para algoritmos no deterministas. Debido a que en PlusCal se puede escribir cualquier expresión de TLA+, es significativamente más expresivo que cualquier lenguaje de programación real. Además, PlusCal se compila en una especificación de TLA+ fácilmente legible. Esto no significa, por supuesto, que una especificación compleja en PlusCal se convierta en una simple en TLA+; simplemente la correspondencia entre ambas es obvia, no habrá complejidad adicional. Finalmente, esta especificación se podrá verificar con herramientas de TLA+. En general, PlusCal puede ayudar a superar la fobia a la matemática, es fácil de entender incluso para programadores y científicos de la computación. En el pasado, publiqué durante un tiempo (alrededor de 10 años) algoritmos en él.
Puede que alguien objete que TLA+ y PlusCal son matemáticas, y que la matemática solo funciona con ejemplos inventados. Sin embargo, en la práctica se necesita un lenguaje real con tipos, procedimientos, objetos, etc. Eso no es cierto. Esto es lo que dice Chris Newcomb, quien trabajó en Amazon: «Usamos TLA+ en diez proyectos importantes, y en cada caso su uso contribuyó significativamente al desarrollo, porque pudimos identificar errores críticos antes de que llegaran a producción, y porque nos dio la comprensión y confianza necesarias para realizar optimizaciones de rendimiento agresivas sin afectar la corrección del programa». A menudo se escucha que al usar métodos formales obtenemos código ineficiente; en la práctica, todo es exactamente lo contrario. Además, se suele decir que es imposible convencer a los gerentes de la necesidad de métodos formales, incluso si los programadores están convencidos de su utilidad. Y Newcomb escribe: «Los gerentes ahora fomentan activamente la redacción de especificaciones en TLA+, y dedican tiempo específicamente para ello». Así que cuando los gerentes ven que TLA+ funciona, lo aceptan con gusto. Chris Newcomb escribió esto hace unos seis meses (en octubre de 2014), y ahora, hasta donde sé, TLA+ se utiliza en 14 proyectos, no en 10. Otro ejemplo se refiere al diseño de Xbox 360. Un pasante se acercó a Charles Takeur y escribió una especificación para el sistema de memoria. Gracias a esta especificación, se encontró un error que de otro modo no se habría detectado, y que habría provocado que cada Xbox 360 se bloqueara después de cuatro horas de uso. Ingenieros de IBM confirmaron que sus pruebas no habrían detectado este error.
Puede leer más sobre TLA+ en Internet, y ahora hablemos de especificaciones informales. Rara vez tenemos que escribir programas que calculen el máximo común divisor y cosas por el estilo. Con mayor frecuencia, escribimos programas como la herramienta de formateo estructurado (pretty-printer) que escribí para TLA+. Después del procesamiento más simple, el código en TLA+ se vería de la siguiente manera:
Pero en el ejemplo dado, el usuario probablemente quería que los signos de conjunción y igualdad estuvieran alineados. Así que el formato correcto se vería más bien así:
Consideremos otro ejemplo:
Aquí, por el contrario, la alineación de los signos de igualdad, suma y multiplicación en el origen era aleatoria, por lo que el procesamiento más simple es totalmente suficiente. En general, no hay una definición matemática precisa del formato correcto, porque 'correcto' en este caso significa 'lo que desea el usuario', y eso no se puede definir matemáticamente.
Aparentemente, si no tenemos una definición de veracidad, entonces la especificación es inútil. Pero no es así. Si no sabemos exactamente lo que debe hacer el programa, eso no significa que no debamos considerar su funcionamiento; por el contrario, debemos dedicar aún más esfuerzo a ello. La especificación aquí es particularmente importante. No es posible determinar el programa óptimo para el formateo estructurado, pero eso no significa que no debamos intentarlo; escribir código como un flujo de conciencia no es lo correcto. Al final, escribí una especificación de seis reglas con definiciones en forma de comentarios en el archivo Java. Aquí hay un ejemplo de una de las reglas: un token de comentario izquierdo es LeftComment alineado con su token correspondiente. Esta regla está escrita en un, por así decirlo, inglés matemático: LeftComment alineado, comentario izquierdo y token correspondiente — términos con definiciones. Así es como los matemáticos describen las matemáticas: escriben definiciones de términos y, sobre la base de ellas, reglas. La ventaja de tal especificación es que es mucho más fácil entender y depurar seis reglas que 850 líneas de código. Cabe mencionar que escribir estas reglas no fue sencillo, se tardó bastante tiempo en depurarlas. Especialmente para este propósito, escribí un código que informaba qué regla se estaba utilizando. Gracias a que probé estas seis reglas con varios ejemplos, no necesitaba depurar 850 líneas de código, y los errores resultaron ser bastante fáciles de encontrar. En Java hay excelentes herramientas para esto. Si simplemente hubiera escrito el código, me habría llevado mucho más tiempo y el formateo habría sido de peor calidad.
¿Por qué no se podía utilizar una especificación formal? Por un lado, la corrección en este caso no es demasiado importante. La impresión estructural seguramente no agradará a alguien, así que no necesitaba lograr que funcionara correctamente en todas las situaciones inusuales. Más importante aún es el hecho de que no tenía herramientas adecuadas. La herramienta para verificar modelos TLA+ aquí es inútil, por lo que tendría que escribir ejemplos manualmente.
La especificación dada tiene características comunes a todas las especificaciones. Está a un nivel más alto que el código. Se puede implementar en cualquier lenguaje. Para escribirla, no son útiles herramientas o métodos. Ningún curso de programación puede ayudarle a escribir esta especificación. Y no existen herramientas que puedan hacer que esta especificación sea innecesaria, a menos que esté escribiendo un lenguaje específicamente para escribir programas de impresión estructural en TLA+. Finalmente, esta especificación no dice nada sobre cómo vamos a escribir el código, solo indica qué hace este 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 particularidades que la distinguen de otras especificaciones. El 95% de las otras especificaciones son significativamente más cortas y simples:
A continuación, esta especificación es un conjunto de reglas. Por lo general, esto es un signo de una mala especificación. Comprender las consecuencias de un conjunto de reglas es bastante difícil, y por eso tuve que dedicar mucho tiempo a depurarlas. Sin embargo, en este caso no encontré mejor manera.
Vale la pena decir unas palabras sobre los programas que funcionan continuamente. Por lo general, operan en paralelo, como los sistemas operativos o los sistemas distribuidos. Muy pocas personas pueden entenderlos en la mente o en papel, y yo no me cuento entre ellas, a pesar de que alguna vez fui capaz de hacerlo. Por lo tanto, se necesitan herramientas que verifiquen nuestro trabajo, como TLA+ o PlusCal.
¿Por qué era necesario escribir una especificación si ya sabía lo que el código debía hacer? En realidad, solo me parecía que lo sabía. Además, con la especificación, una persona externa ya no necesita meterse en el código para entender qué es lo que hace. Tengo una regla: no debe haber reglas generales. Esta regla, por supuesto, tiene una excepción, que es la única regla general que sigo: la especificación de lo que hace el código debe informar a las personas todo lo que necesitan saber al utilizar ese código.
Entonces, ¿qué necesitan saber los programadores sobre el pensamiento? Para empezar, lo mismo que todos: si no escribes, solo te parece que piensas. Además, hay que pensar antes de codificar, lo que significa que hay que 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 pueda ser utilizado o modificado por alguien. Y ese 'alguien' puede ser el mismo autor del código un mes después de haberlo escrito. La especificación es necesaria para grandes programas y sistemas, para clases, para métodos y a veces incluso para secciones complejas de un solo método. ¿Qué se debe escribir sobre el código? Hay que 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 indicar cómo exactamente el código alcanza su objetivo. Si este método lo vimos en el curso de algoritmos, lo llamamos algoritmo. Si es algo más especial y nuevo, lo denominamos diseño de alto nivel. No hay diferencia formal aquí: ambos son modelos abstractos del programa.
¿Cómo se debe escribir la especificación del código? Lo principal: debe estar un nivel por encima del código mismo. Debe describir estados y comportamientos. Tiene que ser tan rigurosa como lo exija la tarea. Si estás escribiendo la especificación de un método de implementación de una tarea, se puede escribir en pseudocódigo o utilizando PlusCal. Debes aprender a escribir especificaciones a partir de especificaciones formales. Esto te dará las habilidades necesarias que también ayudarán con las no formales. ¿Y cómo se aprende a escribir especificaciones formales? Cuando estudiamos programación, escribimos programas y luego los depuramos. Lo mismo aquí: necesitas escribir una especificación, probarla con una herramienta de verificación de modelos y corregir errores. TLA+ puede no ser el mejor lenguaje para la especificación formal, y para tus necesidades específicas, es probable que un lenguaje diferente sea más adecuado. La ventaja de TLA+ es que enseña muy bien el pensamiento matemático.
¿Cómo vincular la especificación y el código? A través de comentarios que conectan conceptos matemáticos con su implementación. Si trabajas con grafos, a nivel de programa tendrás matrices de nodos y matrices de conexiones. Por lo tanto, debes escribir cómo se implementa exactamente el grafo con estas estructuras de programación.
Es importante señalar que nada de lo anterior se relaciona con el propio proceso de escritura de código. Cuando escribes código, es decir, cuando realizas el tercer paso, también necesitas pensar y planificar el programa. Si una subtarea resulta ser complicada o poco clara, es necesario elaborar una especificación para ella. Pero aquí no hablo del código en sí. Puedes utilizar cualquier lenguaje de programación, cualquier metodología, no se trata de eso. 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 una etapa adicional en el proceso de escribir código. A través de esto, muchos errores se pueden detectar con menos esfuerzo, como lo sabemos por la experiencia de programadores en Amazon. Con especificaciones, la calidad de los programas mejora. ¿Entonces, por qué a menudo prescindimos de ellas? Porque escribir es difícil. Y escribir es difícil porque requiere pensar, y pensar también es complicado. Siempre es más fácil fingir que piensas. Aquí se puede hacer una analogía con correr: cuanto menos corres, más lento corres. Necesitas entrenar tus músculos y practicar la escritura. Se necesita práctica.
La especificación puede ser incorrecta. Es posible que hayas cometido un error en algún lugar, que los requisitos hayan cambiado o que haya sido necesario hacer una mejora. Cualquier código que alguien utilice necesita ser modificado, por lo que tarde o temprano la especificación dejará de coincidir con el programa. Idealmente, en este caso, se debería escribir una nueva especificación y reescribir completamente el código. Sabemos que eso rara vez se hace. En la práctica, parcheamos el código y, posiblemente, actualizamos la especificación. Si esto debe suceder tarde o temprano, ¿por qué escribir especificaciones en primer lugar? Primero, para la persona que va a modificar tu código, cada palabra extra en la especificación será invaluable, y esa persona podrías ser tú mismo. A menudo me recrimino por no tener especificaciones adecuadas cuando modifico mi código. Yo escribo más especificaciones que código. Por lo tanto, cuando modifiques el código, siempre debes actualizar la especificación. En segundo lugar, con cada modificación, el código se vuelve peor, se hace cada vez más difícil de leer y mantener. Esto es un aumento de la entropía. Pero si no comienzas con una especificación, cada línea escrita será una modificación, y el código desde el principio será engorroso y difícil de leer.
Como dijo , , ninguna batalla se ganó siguiendo un plan, y ninguna batalla se ganó sin un plan. Y él sabía algo sobre batallas. Existe la opinión de que escribir especificaciones es una pérdida de tiempo. A veces realmente lo es, y la tarea es tan simple que no hay nada que planear. Pero siempre debes recordar que, cuando te aconsejan no escribir especificaciones, te están aconsejando no pensar. Y sobre esto vale la pena reflexionar cada vez. Pensar en la tarea no garantiza que no cometerás errores. Como sabemos, no se ha inventado la varita mágica, y la programación es una tarea compleja. Pero si no piensas en la tarea, seguro que cometerás errores.
Puedes leer más sobre TLA+ y PlusCal en un sitio web especial; se puede acceder desde mi página de inicio. Eso es todo de mi parte, gracias por su atención.
Recuerdo que esta es una traducción. Cuando escriban comentarios, tengan en cuenta que el autor no los leerá. Si realmente desean comunicarse 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. Las entradas se pueden adquirir. .
Fuente: habr.com
