Técnicas de reescritura para especificaciones condicionales

Laburpena

LA REESCRITURA ES UN CONCEPTO Y UNA HERRAMIENTA BASICA HOY EN DIA PARA LA REALIZACION DE DISTINTAS TAREAS LIGADAS A LAS ESPECIFICACIONES ALGEBRAICAS DE TIPOS ABSTRACTOS DE DATOS, SU INTERES SE CENTRA ESENCIALMENTE EN LA EJECUCION DE ESPECIFICACIONES Y EN LA DEMOSTRACION DE TEOREMAS. EL USO DE ESPECIFICACIONES CONDICIONALES NECESARIO PARA TRATAR ALGUNAS CLASES DE PROBLEMAS DA LUGAR A DIVERSOS ENFOQUES DE REESCRITURA CONDICIONAL EN LOS QUE EL MANEJO DE CONDICIONES APORTA NUEVOS PROBLEMAS. EN ESTA TESIS SE REALIZA UN ESTUDIO DE DISTINTAS TECNICAS DE REESCRITURA CONDICIONAL. LOS PUNTOS MAS SEÑALADOS SON LOS SIGUIENTES: 1- DEFINICION GENERAL Y CONDICIONES DE COMPLETITUD DE DIVERSOS METODOS JERARQUICOS EN CONEXION CON LA REESCRITURA CONDICIONAL RECURSIVA. 2- ESTUDIO DE LAS LOG-ESPECIFICACIONES CONDICIONALES ESPECIFICACIONES CUYOS MODELOS TIENEN COMO SOPORTE BOOLEANO EXACTAMENTE A LOS BOOLEANOS . PARA ESTE TIPO DE ESPECIFICACIONES SE DEFINE UN SISTEMA DE DEDUCCION COMPLETO Y SE DA UNA CARACTERIZACION SINTACTICA DE LA CORRECCION DE LAS LOG-ESPECIFICACIONES PARAMETRIZADAS. 3- SE PRESENTA LA REESCRITURA CONTEXTUAL COMO METODO DE DEDUCCION COMPLETO ASOCIADO A LAS LOG-ESPECIFICACIONES. TAMBIEN SE DA UNA CONDICION QUE GARANTIZA LA COMPLETITUD DEL METODO JERARQUICO EN ESTE AMBITO.