El Estado del Arte y la Prueba de Software

En el ámbito del desarrollo de software, el estado del arte (state of the art) típicamente ha estado vinculado con la evolución de los lenguajes de computación. Uno de los primeros grandes saltos en esa dirección fue el desarrollo del primer lenguaje de alto nivel, FORTRAN. En sus inicios, el desarrollo de software en ese lenguaje era considerado “programación automática” porque requería menos conocimientos técnicos que los lenguajes ensambladores. Los detractores (gurús que programaban en lenguaje ensamblador) solían justificar su rechazo mostrando que los programas en FORTRAN eran significativamente más ineficientes comparados con los que ellos escribían. Hoy no solo tenemos lenguajes de programación de alto nivel, de “cuarta” y de “quinta generación”, funcionales u orientados a objetos; también lenguajes de documentación (Latex, HTML, etc.), de especificación (bison, flex, etc.), y otros. Sin embargo, estos lenguajes hoy representan más bien lo que suele llamarse el “state of practice”: lo que incorporan las herramientas comerciales y que utiliza la industria.

Una de las vertientes del “state of the art” tiene que ver con lo que denominamos “métodos formales” (MF).

En términos generales, los MF son técnicas mediante las cuales:

1. Se escribe la especificación del sistema a desarrollar utilizando un lenguaje formal L1 (usualmente del paradigma declarativo), que luego es verificada con intervención humana y procesada mediante un compilador C1 para así generar el código en otro lenguaje formal L2 que representa un diseño de alto nivel.
2. Este diseño escrito en el lenguaje L2 a su vez es verificado con intervención humana y procesado mediante un compilador C2 que genera el código en otro lenguaje formal L3 (usualmente del paradigma imperativo).
3. Este código en el lenguaje L3 se procesa mediante un compilador C3 para obtener finalmente el sistema ejecutable.

Las verificaciones mencionadas suelen ser demostraciones matemáticas de que el código actual Cn tiene ciertas propiedades.

En realidad, en el desarrollo de software siempre utilizamosun tipo de MF, pues finalmente se escribe el sistema en algún lenguaje Lx, que es procesado por un compilador Cx, el cual usualmente genera código ejecutable. Sin embargo, esta transformación suele realizarse solamente para la fase final de las arriba descritas (la generación del sistema ejecutable a partir del programa escrito en un lenguaje de programación, usualmente imperativo), no para todo el ciclo de desarrollo (requerimientos-diseño-programación). Los MF abordan el ciclo completo. Algunos de los métodos formales más conocidos son el “Método B” y la “Notación Z”.

Ejemplo de un método formal

Muchos de ustedes, estimados lectores, habrán llevado algún curso de construcción de compiladores durante su carrera. Recordarán que un compilador contiene 4 grandes bloques:

1. El analizador léxico, que se encarga de concatenar caracteres significativos para construir “palabras”.
2. El analizador sintáctico, que verifica que esas “palabras” formen “oraciones” con un orden que es permitido.
3. El procesador semántico, que checa que esas “oraciones” tengan significado.
4. El generador de código, que finalmente transforma el programa escrito en el lenguaje fuente en otro documento escrito en el lenguaje destino.

Probablemente también recuerden que el analizador sintáctico o “parser” suele definirse mediante una gramática, usualmente utilizando alguna nomenclatura especializada como los grafos de sintaxis (GS). Hay un tipo de gramáticas (las descendentes predictivas) para las cuales es relativamente fácil la escritura del parser que las procesen, pero tienen ciertas restricciones; en particular:

• la definición no puede tener recursión izquierda (el procesamiento se ciclaría indefinidamente),
• en una alternación de grafos, no puede ocurrir que un par de ellos comience con la misma cadena (siempre tomaría la primer alternativa).

Las reglas para construir un parser descendente predictivo son relativamente sencillas y pueden ser automatizadas para generarlos en pseudocódigo; por razones de espacio, nos ahorraremos su definición aquí. Con esa automatización tendríamos un pequeño MF:
1. Escribiríamos la especificación del parser a desarrollar utilizando el lenguaje formal de los grafos de sintaxis, que sería verificada por un compilador de GS para detectar, entre otras cosas, recursión izquierda y/o alternaciones de GS no permitidas; en caso de haberlas, la especificación sería corregida con intervención humana. Una vez corregida y verificada, el compilador de GS podría generar el “diseño” del parser en pseudocódigo, como lenguaje intermedio.
2. Este “diseño” a su vez sería procesado mediante un compilador de pseudocódigo que generaría el programa P en algún lenguaje de alto nivel, a elección del usuario (v.gr. Java, LISP).
3. El programa P sería procesado por el compilador correspondiente y generaría el código ejecutable.

Utilizando el MF para desarrollar ese componente de un compilador, nuestra actividad se centra más en el diseño de una gramática que tenga características deseables, que en la escritura de un programa que la procese. Para lograrlo fue necesario conocer el lenguaje de especificación (los GS), y las características que deben tener las gramáticas (v.gr. no recursión izquierda). Ese es el enfoque usual en los MF.

Aplicación de los métodos formales en la industria
El uso de los MF en el desarrollo de sistemas críticos no es poco común. En el artículo “Software’s Chronic Crisis” [1] pueden encontrarse algunos casos clásicos, entre ellos el uso del método formal “B” para desarrollar un sistema que solucionaba el siguiente problema del metro en París:
La cantidad de usuarios de las líneas del metro se había incrementado considerablemente, de manera que era necesario construir más vías para que circularan más trenes, o bien automatizar la sincronización de las llegadas y salidas de las líneas a cada estación, de manera que se redujera el tiempo entre la partida de un convoy y la llegada de otro. Esta automatización es un buen ejemplo de un sistema crítico: si el software fallara al sincronizar llegadas y salidas, podría ocurrir que sobre la misma vía arribara un convoy en una dirección al tiempo que llegara otro en la dirección opuesta, ocasionando una colisión en la que podría morir mucha gente. Obviamente, ante esa posibilidad no es aceptable un sistema con digamos 99.99999% de confiabilidad (que puede fallar una vez en diez millones). En lugar de ello se utilizó el MF B para “desarrollar software libre de defectos por construcción”: se escribió una especificación formal que fue verificada matemáticamente, a partir de la cual se generó un diseño que fue igualmente verificado, para de ahí generarse el código fuente del que se obtuvo luego el sistema ejecutable.

Algunos mitos sobre los MF
Uno de los mitos de los MF es que son difíciles de aprender. En realidad, la dificultad para aprenderlos solamente radica en que son un tanto “diferentes” de lo usual, pero finalmente están basados en lenguajes formales, y los podemos aprender como aprendemos los de programación (finalmente, lo aprendimos también en nuestro curso de Compiladores). Otro mito más es que poca gente los conoce, y que no son enseñados en las universidades. Este, junto con el anterior, genera un círculo vicioso que se romperá cuando uno de ellos sea descartado. En buena medida gracias a estos prejuicios (y otros más), y a que no se tienen métodos formales genéricos e integrados, esta técnica no ha proliferado en proporción a su potencial. Sin embargo, cada vez más elementos de los incluidos en ellos se han venido introduciendo en muchos ambientes de programación.

Los métodos formales y la prueba de software
Este paradigma cambia tanto la actividad de la programación de sistemas, como la de la prueba de los mismos: el desarrollo tiene que ver menos con escribir código e incluye más tareas de verificación (detección de errores “de alto nivel”), que actualmente se incluyen en las actividades de pruebas. En ese sentido, ambas actividades parecieran confluir. Sin embargo, aún en ese escenario, será necesario probar para revisar por un lado si el sistema desarrollado cumple con los requerimientos del usuario (aspecto que no puede validar el método formal), y por otro si no se cometieron errores durante las verificaciones. Además, hoy en día tenemos tecnologías que interactúan cada vez más con otras, y la integración de sistemas de sistemas es algo que también debe ser probado. Las pruebas serían pues también necesarias, aunque con variaciones significativas.

Referencias

1. W. Gibbs; “Software’s Chronic Crisis”, Scientific American, September 1994. http://bit.ly/sg30r1