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

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
  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.
  2. 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
Este artículo ha sido escrito por Wikipedia. El texto está disponible bajo la licencia Creative Commons - Atribución - CompartirIgual. Pueden aplicarse cláusulas adicionales a los archivos multimedia.