Compilador verificante
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 editar
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 editar
- 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 editar
- 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 editar
- 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 editar
- 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 editar
- 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 editar
- ↑ Tony Hoare (enero de 2003). «The Verifying Compiler: A Grand Challenge for Computing Research». Journal of the ACM (JACM) 50 (1): 63-69. doi:10.1145/602382.602403.
- ↑ Tony Hoare (marzo de 2014). «The Verifying Compiler: A Grand Challenge for Computing Research». Gresham College. Consultado el 29 de marzo de 2016.
Véase también editar
- Whiley Compilador verificante
Datos: Q5779850
