Compilador verificante es un gran reto propuesto por C. A. R. Hoare. En la actualidad es un reto realizar una correspondencia entre la teoría de la computación y las aplicaciones de software. El desarrollo de un compilador verificante es una herramienta esencial para reunir ambas áreas dado que pondría a disposición de los ingenieros de software los resultados teóricos alcanzados.
Grandes retos Un gran reto es un esfuerzo coordinado o en competencia que puede implicar logros científicos de gran envergadura y que no hubieran podido lograrse de otra forma.
Demostrar el último teorema de Fermat (cumplido) Llegar a la luna en 10 años (cumplido) Curar el cáncer en 10 años (fallido en los años 70) Crear el mapa del Genoma Humano (cumplido) Crear el mapa de Proteoma humano (demasiado difícil por el momento) Encontrar el "Bosón de Higgs" (en progreso) Encontrar las ondas gravitacionales (en progreso) Unificar las cuatro fuerzas de la física (en progreso) El Programa de Hilbert para los fundamentos de la matemática (abandonado en los años 30)
Grandes retos en computación
Probar que P es diferente de NP (abierto) La prueba de Turing (no alcanzado) El compilador verificante (abandonado en los años 70) Programa campeón en Ajedrez (completado en 1997) Programa para jugar al Go a nivel profesional (completado en 2016) Traducción automatizada entre dos idiomas (falló en los años 60, bastante avanzada en la actualidad)
Características de un gran reto
Proyecto para al menos quince años Participación mundial Criterios claros de éxito o fallo Avances fundamentales en ciencia o ingeniería
Condiciones necesarias
Suficiente madurez en el área Apoyo general de la comunidad científica Compromiso sostenido de los entes participantes Conciencia de la importancia de parte de los organismos de financiación
El compilador verificante
El compilador verifica la corrección de los programas con respecto a su especificación. La especificación viene dada como aserciones en el programa, información de tipos, etc. Las herramientas utilizadas para la verificación son herramientas de soporte al razonamiento matemático y lógico.
Este es un reto que fue formulado ya por Turing (1948), McCarthy (1962), Floyd (1967), etc.
Representa un logro ingenieril de algo que en algún momento se consideró inalcanzable o impráctico.
Medida de éxito Verificación mecánica de un conjunto de ejemplos representativos de herramientas de software mecánicamente verificadas. Cada ejemplo producido debe ser capaz de reemplazar un software existente en su uso rutinario, de manera de servir de base para futuros desarrollos. Un verificador prototipo debe estar disponible para la comunidad.
Hoare propone como mínimo la verificación de corrección y terminación de aplicaciones de al menos diez mil líneas, y con un nivel menor de seguridad hasta el tratamiento de aplicaciones de al menos un millón de líneas.
Referencias
Véase también Whiley Compilador verificante
Categoría:Compiladores