Combining static analysis and automatic testing

La verificación estática y el testing son técnicas muy útiles que pueden ayudar a los programadores a producir software de calidad que cumple unos requisitos dados. La verificación consiste en usar métodos formales para probar de forma automática o interactiva alguna especificación del código, mientras que el testing consiste en ejecutar el código para entradas concretas, también llamadas casos de prueba, y comprobar que la salida del programa y su comportamiento en general cumple con lo especificado. La depuración de código representa una gran parte del coste del proceso de desarrollo software y del mantenimiento (entre 25% y el 70% para software crítico), por lo que el uso de estas herramientas durante las fases de programación, pruebas y mantenimiento del ciclo de desarrollo ayuda a reducir el esfuerzo en términos de tiempo y coste, ya que contribuyen a la detección temprana de errores. El punto de partida de este trabajo es el enfoque general de combinar testing (aleatorio) basado en aserciones con análisis y verificación estática automática presentes en Ciao, un lenguaje de programación modular, multiparadigma y de propósito general de la familia Prolog. Con las herramientas de Ciao: el analizador estático por interpretación abstracta, el módulo de generación automática de tests basados en aserciones, la infraestructura de comprobación en tiempo de ejecución, y con el lenguaje unificado de aserciones de Ciao como enlace común, exploramos un proceso concreto de verificación de aserciones que combina de manera secuencial el análisis estático con el testing a través de casos de prueba unitarios definidos por el usuario y generación de tests aleatorios, e ilustramos sus funcionalidades con un ejemplo práctico. Está combinación explota los puntos fuertes de cada uno de estos métodos de verificación, obteniendo mejores resultados en validación de código. Nuestro objetivo a medio plazo es implementar, experimentar y evaluar las diferentes combinaciones de generación de casos de prueba aleatorios, testing en tiempo de ejecución y verificación estática qué son posibles con la infraestructura de Ciao. A más largo plazo planeamos elevar nuestra exploración al nivel abstracto, por ejemplo a través de la experimentación con diferentes formas de testing abstracto aleatorio, basado en la partición de dominios abstractos.---ABSTRACT---Static verification and testing are useful techniques that can help programmers produce quality software that meets certain requirements. Verification consists in using formal methods to prove automatically or interactively some specification of the code, whereas testing consists in executing the code for concrete inputs, also known as test cases, and checking that the program’s output and behaviour in general meets the specifications of the code. Software debugging represents a large proportion of the software development and maintenance cost (from 25% up to 70% for safety critical software), so the usage of these tools during the coding, testing, and maintenance phases of the software development cycle helps reduce efforts in terms of time and cost, as they contribute to the early detection of bugs. The starting point of this work is the general approach for combining assertionbased (random) testing with automatic abstract static analysis and verification present in Ciao, a general-purpose, modular, multiparadigm programming language in the Prolog family. With the tools provided by Ciao: The static analyser via abstract interpretation, the automatic assertion-based test generation module, the run-time checking framework, and Ciao’s unified assertion language as the common link, we explore a concrete assertion checking pipeline that sequentially combines static analysis and testing via user-defined unit tests and randomised test case generation, and we illustrate its features with a practical example. This combination exploits the strengths of each one of these verification methods achieving even better results in code validation. Our medium term objective is to implement, experiment with, and benchmark several of the different combinations of randomised test case generation, run-time testing, and static verification which are possible within the Ciao framework. Longerterm, we plan to lift our exploration to the abstract level, for example by experimenting with different forms of randomised abstract testing, based on abstract domain partitioning