Trata de averiguar manualmente la correctitud de software resulta en una prueba formal más larga y propensa a errores que el código mismo. Las herramientas automatizadas son preferibles, pero no siempre posibles. Lo siguiente describe una ruta intermedia: razonamiento semi-formal sobre la dicha correctitud.
El planteamiento de fondo es dividir todo el código en cuestión de secciones cortas –desde una sola línea, como invocar a una función, hasta bloques de menos de 10 líneas– y discutir acerca de su exactitud. Los argumentos sólo necesitan ser suficientemente fuertes para convencer al compañero del diablo como tu pareja de programación.
Una sección debería ser elegida de modo que en cada terminal el estado del programa (léase: el conteo del programa y los valores de todos los objetos “vivos”) satisface una propiedad fácilmente descrita y que la funcionalidad de esa sección (transformación de estado) sea fácil de describir como una sola tarea –estos harán el razonamiento más sencillo–. Tales propiedades terminales generalizan conceptos como precondinción y poscondición de funciones, e invariantes para ciclos y clases (con respecto a sus instancias). La lucha para que las secciones sean independientes de las otras tanto como sea posible simplifica el razonamiento y es indispensable cuando estas secciones son modificadas.
Muchas de las prácticas de codificación que son bien conocidas (aunque quizás menos seguidas) y consideradas “buenas” hacen el razonamiento más fácil. Por lo tanto, sólo con la intención de razonar sobre tu código ya estás comenzando a pensar acerca de un mejor estilo y estructura. Como era de esperarse, la mayoría de estas prácticas pueden ser revisadas por analizadores de código estático:
goto
, ya que hacen las secciones remotas
altamente interdependientesConforme se razone sobre la correctitud, argumentar sobre tu código te ofrece entendimiento sobre él. Comunica sus descubrimientos para el beneficio de todos.
Traducción: Espartaco Palma