ESC Java y la verificación formal de código

Recientemente recibí el encargo de preparar una clase para la Universidad sobre “ESC/Java”. La especificación que se me dio era tan sencilla como “prepara una clase de ESC/Java con contenido teórico-práctico”. Ya impartí la clase y me ha parecido interesante realizar un post acerca de la verificación formal de código y la supuesta utilidad de una herramienta como “ESC/Java” fuera del ámbito académico (es decir, si sirve para algo).

Empezaré introduciendo brevemente algún concepto de Verificación Formal, que no es si no el conjunto de técnicas que permiten demostrar matemáticamente si un programa es correcto o no. Para ello se desarrolla un proceso de inferencia cuya representación son las famosas ternas e Hoare ({P}C{Q}), donde P es la precondición, C el código y Q la poscondición. Me hinché de hacer ejercicios de estos en la carrera…

verificación formal

 

 

Si hay algo que tenía (y tengo) bastante claro es la dudosa aplicación de la verificación formal de programas como herramienta o metodología en cualquier aspecto del desarrollo de sistemas de información y esa es la forma “suave” de decir que es una disciplina de índole exclusivamente teórica o docente. ¿Os imagináis desarrollando un proceso de verificación formal sobre una aplicación de 10.000 líneas, con entorno gráfico?

ESC/Java (Extended Static Checker for Java) por su parte es la molestia que se han tomado unos señores de realizar una aplicación que realiza verificación formal de modo automático sobre código Java. El funcionamiento es sencillo, comentamos el código mediante pragmas java que componen las precondiciones, aserciones y poscondiciones, y ejecutamos ESC/Java sobre el código. Entonces en pantalla se nos muestran una serie de mensajes indicando si el código se adecua a las precondiciones, aserciones y poscondiciones indicadas.

Ejemplos de pragmas son: @requires, @ensures, @invariant, @assert.

Para poder dar la clase me estuve documentando bastante sobre el tema y llegaron a mis manos presentaciones en las que ESC/Java se proponía como “La Herramienta” que permitiría realizar buenos programas, mejorar estimaciones, servir como base para innovadoras métricas del software, etc, etc. Que cada cual saque su conclusión sobre el tema; personalmente dudo que esta herramienta, al igual que la verificación formal pueda salir del campo académico.