En informática , la corrección del compilador es la rama de la ciencia informática que trata de intentar demostrar que un compilador se comporta de acuerdo con su especificación de lenguaje . [ cita requerida ] Las técnicas incluyen el desarrollo del compilador utilizando métodos formales y el uso de pruebas rigurosas (a menudo llamadas validación del compilador) en un compilador existente.
Los dos principales enfoques de verificación formal para establecer la corrección de la compilación son demostrar la corrección del compilador para todas las entradas y demostrar la corrección de una compilación de un programa particular (validación de la traducción).
La validación de compiladores con métodos formales implica una larga cadena de lógica formal y deductiva . [1] Sin embargo, dado que la herramienta para encontrar la prueba ( demostrador de teoremas ) está implementada en software y es compleja, existe una alta probabilidad de que contenga errores. Un enfoque ha sido utilizar una herramienta que verifica la prueba (un verificador de pruebas ) que, debido a que es mucho más simple que un buscador de pruebas, es menos probable que contenga errores.
Un ejemplo destacado de este enfoque es CompCert , que es un compilador optimizador verificado formalmente de un gran subconjunto de C99 . [2] [3] [4]
Otro compilador verificado fue desarrollado en el proyecto CakeML, [5] que establece la corrección de un subconjunto sustancial del lenguaje de programación ML estándar utilizando HOL (asistente de prueba) .
Otro enfoque para obtener un compilador formalmente correcto es utilizar la generación de compiladores dirigida por semántica. [6]
A diferencia de intentar demostrar que un compilador es correcto para todos los programas de entrada válidos, la validación de la traducción [7] tiene como objetivo establecer automáticamente que un programa de entrada dado se compila correctamente. Probar la compilación correcta de un programa dado es potencialmente más fácil que probar que un compilador es correcto para todos los programas, pero aún requiere razonamiento simbólico, porque un programa fijo puede seguir funcionando con entradas arbitrariamente grandes y ejecutarse durante un período de tiempo arbitrario. La validación de la traducción puede reutilizar una implementación de compilador existente al generar, para una compilación dada, una prueba de que la compilación fue correcta. La validación de la traducción se puede utilizar incluso con un compilador que a veces genera código incorrecto, siempre que este error no se manifieste para un programa dado. Dependiendo del programa de entrada, la validación de la traducción puede fallar (porque el código generado es incorrecto o la técnica de validación de la traducción es demasiado débil para mostrar la corrección). Sin embargo, si la validación de la traducción tiene éxito, entonces se garantiza que el programa compilado es correcto para todas las entradas.
Las pruebas representan una parte importante del esfuerzo que supone lanzar un compilador, pero reciben una cobertura comparativamente escasa en la literatura estándar. La edición de 1986 de Aho, Sethi y Ullman tiene una sección de una sola página sobre pruebas de compiladores, sin ejemplos nombrados. [8] La edición de 2006 omite la sección sobre pruebas, pero sí enfatiza su importancia: “Los compiladores optimizadores son tan difíciles de hacer bien que nos atrevemos a decir que ningún compilador optimizador está completamente libre de errores. Por lo tanto, el objetivo más importante al escribir un compilador es que sea correcto”. [9] Fraser y Hanson 1995 tienen una breve sección sobre pruebas de regresión ; el código fuente está disponible. [10] Bailey y Davidson 2003 cubren las pruebas de llamadas a procedimientos . [11] Varios artículos confirman que muchos compiladores lanzados tienen errores significativos de corrección de código. [12] Sheridan 2007 es probablemente el artículo de revista más reciente sobre pruebas generales de compiladores. [13] Para la mayoría de los propósitos, la mayor cantidad de información disponible sobre pruebas de compiladores son las suites de validación Fortran [14] y Cobol [15] .
Otras técnicas comunes al probar compiladores son el fuzzing [16] (que genera programas aleatorios para intentar encontrar errores en un compilador) y la reducción de casos de prueba (que intenta minimizar un caso de prueba encontrado para que sea más fácil de entender). [17]