Síntesis constructiva de programas lógicos
-
Autores: Francisco José Galán Morillo
, José Miguel Toro Bonilla
- Localización: I Jornadas de informática. Actas: Puerto de la Cruz, 17-21 de julio de 1995 / José María Troya Linero (dir. congr.) , Casiano Rodríguez León (dir. congr.) , 1995, págs. 311-322
- Idioma: español
- Texto completo no disponible (Saber más ...)
-
Resumen
El problema se centra en la derivación de programas lógicos desde especificaciones en lógica de primer orden utilizando el concepto de extracción de programas desde pruebas. Sintetizar un programa desde su especificación consiste en establecer que la especificación es dedicible. Usaremos la lógica intuicionista como filosofía de razonamiento y adoptaremos como sistema de prueba el Cálculo de Secuentes de Gentzen. Ampliaremos el sistema de reglas con otras nuevas que permitan modelar de modo más adecuado aspectos relevantes en la programación: esquema de programas, transformaciones, recusión, ...etc. Los métodos constructivos aseguran de una manera más fácil la corrección de los programas sintetizados. Otro aspecto fundamental es la superación de bloqueos en la prueba de la especificación. Para ello, se propone el uso de reglas de transformación y reglas que permiten modelar razonamiento ecuacional en nuestro sistema de prueba-construcción de programas estudiando si preservan corrección parcial o total.
