Tesis doctoral de David Robert Son
Esta tesis trata de nuevas formas de usar métodos de síntesis estructural para especificaciones cláusulas de horn ejecutables como programas lógicos. estos métodos son aplicables al diseño y refinamiento iniciales de estas especificaciones, estadio considerado crucial para el uso de las especificaciones formales en aplicaciones prácticas. dos métodos de diseño automático son descritos. El primero es una forma distribuida de diseño que utiliza un conjunto de herramientas independientes para construir las diferentes partes de una especificación. Estas herramientas solamente comparten información de diseño através del lenguaje com partido por todas ellas. La evalución empírica de este sistema revela un conjunto de dificultades nacidas de la insuficiente integración entre las diferentes herramientas mencionadas y también la falta de un marco para el refinamiento incremental de especificaciones. El segundo sistema da respuesta a algunos de estos problemas proponiendo un sistema de refinamiento aplicable a problemas que pueden ser vistos como transformaciones sobre conjuntos de axiomas. en este sistema, todas las cláusulas de horn expresan relaciones entre conjuntos de axionas (donde estos también son cláusulas de horn). Esto permite que las especificaciones iniciales sean definifas restringiendo estos conjuntos. Inicialmente, estas especificaciones son refinadas por un sistema de reglas de reescritura aplicadas sobre desigualdades entre esos conjuntos. Inmediatamente después las espcificaciones son detalladas progresivamente introduciendo esqueletos de definiciones específicas de la tarea, que describen la manera de relacionar los elementos de los conjuntos de axiomas mencionados y también añadiendo nuevos argumentos a los predicados que permitan llevar nueva información entre las especificaciones. los métodos descritos en la tesis son implementados por los sistemas lss y hansel. Estos han sido aplicados y comprob
Datos académicos de la tesis doctoral «Pragmatica de la sintesis de programas lógicos«
- Título de la tesis: Pragmatica de la sintesis de programas lógicos
- Autor: David Robert Son
- Universidad: Autónoma de barcelona
- Fecha de lectura de la tesis: 01/10/1999
Dirección y tribunal
- Director de la tesis
- Jaume Agustí Cullell
- Tribunal
- Presidente del tribunal: Juan jose Villanueva pipaón
- Manuel Hermenegildo salinas (vocal)
- ramón López de mántaras badía (vocal)
- norbert Fuchs (vocal)