Compilador verificante
De Wikipedia, la enciclopedia libre
Compilador verificante es un gran reto propuesto por C. A. R. Hoare.
(Extracto de su presentación pública en Leiden, en 2003.)
Tabla de contenidos |
[editar] Grandes retos
- 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)
[editar] 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 (demasiado difícil)
- Traducción automatizada entre dos idiomas (falló en los años 60)
[editar] 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
[editar] 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
[editar] 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.
[editar] 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.
