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.[1][2]
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
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
