Diseño y verificación de algoritmos para el tratamiento difuso de imágenes digitales en teledetección y seguridad

Resumen

En esta memoria se analizan procesos de especificación, diseño, implementación y corrección de algoritmos nítidos y difusos, así como el proceso de derivación de algoritmos correctos a partir de especificaciones formales, Partiendo de la lógica proposicional y la lógica de primer orden clásicas, se aborda el problema de la expresión y valoración de especificaciones formales de algoritmos en el contexto difuso, lo que nos obliga a realizar un estudio del tratamiento de predicados borrosos en el análisis de objetivos. De este modo, se aborda el problema de la especificación formal mostrando la utilidad del rigor lógico-matemático para expresar las propiedades que ofrecen los datos de entrada en la resolución de problemas que se plantean libres de ambigüedades mediante predicados lógicos. En este trabajo se muestran las técnicas de diseño de algoritmos. En el paradigma imperativo se estudia el diseño desde la intuición y desde la especificación mediante la construcción de asertos invariantes que conducen a la implementación de algoritmos correctos (derivación algorítmica). También se estudia la vericación de algoritmos surgidos de las ideas e intuición del programador cuando el código no se relaciona mediante transformaciones directas con la especificación planteada. En ambos casos se muestra una gran colección de ejemplos que constituyen una base para el programador que podrá utilizar a modo de 'plantillas' en otros desarrollos. En cuanto al paradigma funcional, en primer lugar se estudian técnicas de inmersión, que conducen a algoritmos depurados mediante transformaciones relacionadas con los asertos que constituyen la especificación de los algoritmos. Se distinguen tipos de recursión en función del número de llamadas recursivas (lineal o múltiple) y también en función del modo de la ejecución de las operaciones en cada etapa del proceso (algoritmos recursivos finales y no finales). Se est