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. |fechaacceso= requiere |url= (ayuda)
↑ 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

[CV-1] 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. |fechaacceso= requiere |url= (ayuda)

[CV2-2] Tony Hoare (marzo de 2014). «The Verifying Compiler: A Grand Challenge for Computing Research». Gresham College. Consultado el 29 de marzo de 2016.

[1]

[2]