# Pruebas formales de software

Las Pruebas Formales de Software (Formal Testing) son un enfoque de Prueba de Software en el que se usa extensivamente y de manera integrada una clase particular de Lenguajes Formales en actividades de pruebas. Su gestación puede situarse en trabajos sobre Métodos Formales.
Las Pruebas Formales hacen uso intensivo de la tecnología de compiladores, así como de avances en el área de los Lenguajes de Programación que han influenciado su desarrollo y el de otros Lenguajes Informáticos. Estas tecnologías posibilitan un sofisticado nivel de automatización en actividades de prueba, y con ello el incremento tanto en la productividad como en la efectividad de los Ingenieros de Prueba (Testers).

## Definición

Las Pruebas Formales de Software (Formal Testing) son un enfoque en el que se usa extensivamente y de manera integrada una clase especial de Lenguajes Formales en actividades de pruebas, los llamados Lenguajes de Computadora (o Lenguajes Informáticos), Algunos ejemplos son los siguientes:
* El uso de Lenguajes de Especificación para desarrollar modelos del producto a probar para que a partir de ellos se generen automáticamente casos de prueba (sub-enfoque conocido como Pruebas Basadas en Modelos Formales, Formal Model Based Testing, o Formal MBT).
* El uso de Lenguajes de Definición de Procesos (Process Definition Languages, o PDLs) para documentar procesos de prueba que faciliten, entre otras cosas, la adecuación de productos que implementen estos procesos y la generación de descripciones de roles que intervienen en ellos.
* El uso de componentes de compiladores (como analizadores léxicos, sintácticos o semánticos) para analizar el código del programa, de la arquitectura o de la especificación del producto a probar, para detectar errores u omisiones y obtener automáticamente métricas estructurales.

## Evolución

Los siguientes son elementos importantes en el desarrollo y la aplicación del enfoque de las Pruebas Formales.
Los primeros Lenguajes de Programación de alto nivel se desarrollaron a finales de la década de 1950. Abonaron significativamente al incremento en la productividad de los desarrolladores de software y al crecimiento de la industria, y sentaron las bases para el desarrollo de otros tipos de Lenguajes Informáticos.
Muchos de los trabajos iniciales alrededor de los Métodos Formales para desarrollar software se remontan a los años 60, y en ellos era común que utilizaran varios Lenguajes de Computadora, en particular lenguajes de especificación y de programación.
Por otro lado, se suele considerar que la Prueba de Software nace como disciplina en sí misma con trabajos como los de G. Myers a finales de los años 70.
Sobre esos fundamentos, en los años 80 aparecen trabajos del enfoque de Pruebas Basadas en Modelos Formales (Formal Model Based Testing), el cual aplica conceptos, técnicas y herramientas desarrolladas en el área de los Métodos Formales, en particular el uso de Lenguajes de Especificación. Igualmente, comienzan a usarse herramientas basadas en componentes de compiladores para hacer análisis de programas y generar información de apoyo a las actividades de prueba.
En esa década también se aplican modelos de calidad para el desarrollo de software, en particular CMM (Capability Maturity Model), y algunas organizaciones los aplican utilizando Lenguajes de Definición de Procesos.
En los años 90 proliferan las herramientas del tipo CAST (Computer Aided Software Testing).
En la década de 2000 comienzan a utilizarse modelos de calidad especializados en prueba de software como Testing Maturity Model y Test Process Improvement, y algunas organizaciones de prueba los aplican utilizando Lenguajes de Definición de Procesos.
La década de 2010 ha visto la integración de estos elementos del enfoque de las Pruebas Formales.

## Aplicación

Una manera de comenzar a aplicar rápidamente (aunque no con fundamentos muy sólidos) las Pruebas Formales en una organización es la siguiente:
* Utilizar herramientas que utilizan tecnología de compiladores para hacer análisis del código de programas, arquitecturas o especificaciones para detectar errores, omisiones y malas prácticas, así como para obtener métricas de complejidad, pues ahí donde hay mayor complejidad hay más propensión a errores.
* Usar un Lenguaje de Definición de Procesos para documentar el proceso de pruebas de manera que: a) ayude a su mejora continua y a mantenerlo actualizado, consistente y completo; b) facilite la adecuación de productos que implementen ese proceso; y c) posibilite la generación de descripciones de roles que intervienen en el proceso.
* Utilizar un Lenguaje de Especificación que permita escribir modelos del producto a probar para generar automáticamente casos de prueba, incrementando con ello la productividad y la efectividad de los ingenieros de prueba.
Una forma más sólida de comenzar a aplicar rápidamente las Pruebas Formales (porque facilita la apropiación de los fundamentos de ese enfoque) es una secuencia con los mismos pasos anteriores, pero en distinto orden, a saber: 2, 1, 3.