Derivacion deductiva de programas funcionales con patrones

Résumé

LA TESIS DESARROLLA UN METODO DEDUCTIVO PARA LA DERIVACION DE PROGRAMAS FUNCIONALES CON PATRONES, ESCRITOS EN UN LENGUAJE SIMILAR A HOPE, EL METODO UTILIZA UNA LOGICA MULTIGENERO, CUYA RELACION CON EL LENGUAJE DE PROGRAMACION ES ESTUDIADA. TAMBIEN SE IDENTIFICAN LOS ESQUEMAS DE DEMOSTRACION NECESARIOS PARA LA DERIVACION DE FUNCIONES CON PATRONES, BASADOS EN LA DEMOSTRACION INDEPENDIENTE DE VARIAS SUBSENTENCIAS. CADA SUBSENTENCIA PROPORCIONA UNA ESPECIFICACION DE UNA ECUACION DEL FUTURO PROGRAMA A DERIVAR. EL METODO DEDUCTIVO DESARROLLADO ESTA BASADO EN UNO PREVIO DE MANNA Y WALDINGER, CONOCIDO COMO EL CUADRO DEDUCTIVO, QUE DERIVA PROGRAMAS EN UN LENGUAJE SIMILAR A LISP. EL NUEVO METODO ES UNA MODIFICACION DEL CUADRO DE ESTOS AUTORES, QUE INCORPORA TIPOS Y PERMITE DEMOSTRAR UNA ESPECIFICACION MEDIANTE VARIOS CUADROS. CADA CUADRO DEMUESTRA UNA SUBESPECIFICACION Y POR TANTO DERIVA UNA ECUACION DEL PROGRAMA. LA TESIS SE COMPLETA CON MECANISMOS PARA QUE LOS PROGRAMAS DERIVADOS PUEDAN CONTENER DEFINICIONES LOCALES CON PATRONES Y VARIABLES SINONIMAS Y ANONIMAS, CON VARIOS EJEMPLOS DE APLICACION Y UN ANALISIS FUNCIONAL DE UN ENTORNO INTERACTIVO DE DERIVACION DEDUCTIVA.