Compilador verificante

Compilador verificante es un gran reto propuesto por C. A. R. Hoare.

(Extracto de su presentación pública en Leiden, en 2003.)

Contenido

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)

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)

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.


Wikimedia foundation. 2010.

Mira otros diccionarios:

  • Compilador verificante — Gran reto propuesto por C. A. R. Hoare. (Extracto de su presentación pública en Leiden, en 2003.) …   Enciclopedia Universal

  • Comandos Guardados — Saltar a navegación, búsqueda Comandos guardados (GCL) órdenes guardadas es un modelo de lenguaje definido por Edsger Dijkstra para semántica de transformación de predicados (una extensión lógica diseñada para proporcionar una metodología para… …   Wikipedia Español

  • Lenguaje de Comandos Guardados — El Lenguaje de Comandos Guardados (GCL, Guarded Command Language), o de Órdenes Guardadas, es un modelo de lenguaje definido por Edsger Dijkstra para semántica de transformación de predicados (una extensión lógica diseñada para proporcionar una… …   Wikipedia Español

  • GaCeLa — (Del ár. gazala.) ► sustantivo femenino ZOOLOGÍA Pequeño mamífero rumiante del grupo de los antílopes, muy estilizado y de cuello largo, pelo corto de color canela, orejas largas, muy veloz, que habita en las estepas africanas y asiáticas.… …   Enciclopedia Universal


Compartir el artículo y extractos

Link directo
Do a right-click on the link above
and select “Copy Link”

We are using cookies for the best presentation of our site. Continuing to use this site, you agree with this.