Implementación de especificaciones algebraicas

Resumen

LAS ESPECIFICACIONES FORMALES PERMITEN COMPROBAR LA CORRECCION DE UNA IMPLEMENTACION RESPECRTO DE SU ESPECIFICACION, EN ESTA TESIS SE ANALIZA EL CONCEPTO DE IMPLEMENTACION DE ESPECIFICACIONES ENTENDIENDO COMO SIMULACION: UNA ESPECIFICACION, SP, SIMULA OTRA, SP, SI LOS MODELOS DE SP SE COMPORTAN COMO LOS DE SP. SINTACTICAMENTE UNA IMPLEMENTACION DE SP MEDIANTE SP ES UN PAR FORMADO POR UN CONJUNTO DE OPERACIONES, QUE DEFINEN LOS GENEROS DE LA ESPECIFICACION SP EN TERMINOS DE LOS DE SP Y UN CONJUNTO DE ECUACIONES QUE IMPLEMENTAN LAS OPERACIONES DE SP EN TERMINOS DE LAS D SP. LA SEMANTICA DE LA IMPLEMENTACION VIENE DADA POR LA COMPOSICION DE TRES FUNTORES: SINTESIS RESTRICCION E IDENTIFICACION. LA NOVEDAD DE NUESTRA DEFINICION ESTA EN EL TRATAMIENTO DE LAS OPERACIONES DE LA IMPLEMENTACION COMO OPERACIONES PARCIALES, LO CUAL PERMITE UNA CARACTERIZACION DE LA ORRECCION FACILMENTE VERIFICABLE. ADEMAS PERMITE RESOLVER LOS PROBLEMAS DE ORDEN TEORICO Y PRACTICO QUE PRESENTABA LA GNERALIZACION AL CASO PARAMETRIZADO. GENERALIZAMOS LAS IMPLEMENTACIONES AL CASO DE ESPECIFICACIONES PARCIALES TENIENDO EN CUENTA LA EQUIVALENCIA EN COMPORTAMIENTO. ABORDAMOS EL DISEÑO MODULAR DE UN SISTEMA DE SOFTWARE DESDE SU ESPECIFICACION HASTA LA CONSTRUCCION DE LOS MODULOS DE PROGRAMAS. EL RESULTADO FUNDAMENTAL PRESENTADO ESTABLECE QUE LA CORRECCION TOTAL DE LA IMPLEMENTACION DE UN SISTEMA DEPENDE DE LA CORRECCION DE LA IMPLEMENTACION CONCRETA DE CADA MODULO. ES CRUCIAL EN LA DEMOSTRACION TENER EN CUENTA PROPIEDADES DEL LENGUAJE DE PROGRAMACION QUE SOPORTA LA MODULARIDAD COMO LA ESTABILIDAD.