TEORIA DE LA PROGRAMACION

Autor: JORGE CASTRO JOSE SANTIAGO.
Año: 2004.
Universidad: A CORUÑA.
Centro de lectura: FACULTAD DE INFORMATICA.
Centro de realización: FACULTAD DE INFORMATICA.

Resumen: El principal objetivo de esta tesis es la investigación de una metodología para producir software certificado, desde pruebas manuales hasta el uso de asistentes que supervisan y colaboran en el proceso de prueba. Estudiaremos el desarrollo de algoritmos probados formalmente para la computación, explicando cómo demostrar que una implementación de un algoritmo cumple las propiedades esperadas, realizando este examen en base al estudio de distintos ejemplos en orden creciente de complejidad, teniendo en cuenta no sólo la certificación de los programas sino tambien de su eficiencia. Para cada uno de estos programas, presentamos en primer lugar, todas las definiciones y demostraciones de propiedades con pruebas hechas a mano en un estilo riguroso, donde cada paso está justificado por razonamiento matemático, y a continuación presentamos una transformación de la formalización de estas definiciones y pruebas a otras equivalentes en el sistema de pruebas Coq. Como otros probadores de teoremas, este sistema proporciona control y asistencia durante los procesos de especificación y prueba; por tanto evita errores que podrían introducirse en una prueba a mano. El asistente de pruebas Coq es una implementación del cálculo de construcciones inductivas que es una teoría de tipos resultante de la combinación de la teoría intuicionista de tipos de Martin Lof y el cálculo polimórfico de Girard, Fw. La teoría constructiva de tipos guarda similitudes con los lenguajes de programación. La prueba de un teorema es una función que a partir de las pruebas de las hipótesis del teorema, calcula la prueba del enunciado. Así, las formalizaciones de los algoritmos en Coq son compilables eficientemente usándose para la computación. Las técnicas propuestas quedarán ejemplificadas sobre programas no triviales, donde se describen formalmente los principios básico que hacen a estos algoritmos funcionar, quedando manifiesta la posibilidad de que las pruebas y la computación vayan de la mano.

Autor: GALLEGOS SALINER ANNA.
Año: 2003.
Universidad: GIRONA.
Centro de lectura: UNIVERSITAT DE GIRONA.
Centro de realización: INSTITUTO DE QUIMICA COMPUTACIONAL.

Resumen: La presente tesis está centrada en el uso de la teoría de la semejanza cuántica para calcular descriptores moleculares. Dichos descriptores se usan como parámetros estructurales para derivar correlaciones entre la estructura y la función o actividad experimental para un grupo de compuestos. Los estudios de Relaciones Cuantitativas Estructura-Actividad son de gran importancia para el diseño de moléculas asistido por ordenador y, en particular, para el diseño de fármacos. La memoria consta de cuartro paretes diferenciadas. En los dos primeros bloques, los fundamentos de la teoría de semejanza cuántica, así como la aproximación topológica, son revisados. Ambas teorias se usan para calcular los descriptores moleculares. En el segundo bloque, debe remarcarse la programación e implementación de programario para calcular los llamados indices topológicos de semejaza cuántica. la tercera sección revisa los fundamentos de las Relaciones Cuantitativas Estructura-Actividad y, finalmente, el último apartado recoge los resultados de aplicación obtenidos para distintos sistemas biológicos.

Autor: CABALLERO ROLDÁN RAFAEL.
Año: 2003.
Universidad: COMPLUTENSE DE MADRID.
Centro de lectura: MATEMÁTICAS.
Centro de realización: FACULTAD DE CC. MATEMÁTICAS.

Resumen: La falta de herramientas auxiliares tales como depuradores o entornos gráficos ha sido señalada como una posible limitacion para el éxito, fuerade ámbitos puramente académicos, de los lenguajes funcionales tipo Haskell. Este mismo razonamiento es aplicable al caso de los lenguajes lógicos, lógico-funcionales, en general a todos los llamados lenguajes declarativos. Sin embargo, la incorporación de estas herramientas, y en particular de depuradores, no es siempre sencilla, ya que a menudo las ideas empleadas para su desarrollo en otros paradigmas no son aplicables a los lenguajes declarativos. La progrmación lógico-funcional recoge ideas tanto de la programación lógica como funcional perezosa para dar lugar a lenguajes como Toy y Curry, que tratan de aunar las ventajas de ambos pradigmas. El problema de la construcción de depuradores para estos lenguajes plantea los inconvenientes ya señalados, y ello motiva la investigación de técnicas alternativas a las tradicionales también para estos lenguajes. La presente tesis desarrolla un marco teórico para la depuración declarativa de respuestas incorrectas en lenguajes lógico-funcionales y se ocupa así mismo de su implementación. Para ello se define un cálculo semántico, basado en la lógica CRWL propuesta como marco semántico para programas lógico-funcionales, que permite la definición formal de árboles de cómputo adecuados para la depuración de respuestas incorrectas en el marco lógico-funcional. Con objeto de poder llevar estas ideas teóricas a la práctica se define además una transformación de programas capaz de producir programas que generen árboles de cómputo como parte de sus resultados, y se prueba la corrección de esta transformación con respecto al cálculo semántico. Entre los objetivos de la tesis también está comprobar la viabilidad de la implementación de estas ideas. Para ello se han incorporado depuradores deeclarativos de respuestas incorrectas tanto al sistema Toy como al sistema Curry desarrollado por la Universidad de Münster, desarrollando técnicas destinadas a mejorar la utilización de estos depuradores. Como tanto la programación lógica como funcional tienen cabida en el marco teórico considerado, las pruebas de correción sirven a la vez para probar la corrección de los depuradores basados en estas mismas ideas para la programación lógica y para la programación funcional. Aunque en programación lógica sí es habitual encontrar pruebas de corrección de los depuradores declarativos, no ocurre lo mismo en programación funcional, por lo que el enfoque resulta novedoso en este sentido.

Autor: HIDALGO HERRERO MERCEDES.
Año: 2003.
Universidad: COMPLUTENSE DE MADRID.
Centro de lectura: MATEMÁTICAS.
Centro de realización: FACULTAD DE CIENCIAS MATEMÁTICAS.

Resumen: El objetivo del trabajo es definir semánticas formales para un lenguaje que contiene las principales características del lenguaje funcional paralelo Eden, extensión del lenguaje funcional perezoso por excelencia, Haskell, pues Eden permite definir esquemás genéricos de proceso y crear dinámicamente ejemplares a partir de los mismos. Así como Eden presenta paralelismo explícito, la comunicación es, en cambio, implícita. En cuanto a la introducción del no-determinismo, es explícita y se limita a la invocación de un proceso predefinido. Estas características las hemos incluido en un lenguaje más simple, Jauja, y hemos precedido a definir semánticas formales para este último. La primera semántica tratada es la operacional, con un nivel de abstracción separado de las particularidades de cualquier máquina virtual. Nos dirigimos hacia enfoques basados en la semántica natural de Launchbury, como la semántica operacional que Baker-Finch y otros defnieron para el lenguaje funcional paralelo GpH (Glasgow Parallel Haskell), también definido sobre Haskell pero empleando paralelismo semi-explícito. Para Jauja extendemos este modelo operacional para poder representar proceso. A partir de la semántica operacional construida, se definen medidas para estudiar la eficiencia de los programas, sobre si la introducción del paralelismo ha sido fructífera o no. Pensando en un usuario del lenguaje, hemos definido una semántica denotacional que refleja los resultados de la evaluación sin bajar tanto el nivel de abstracción. No obstante, el modelo denotacional elegido no es una semántica denotacional directa, sino un modelo denotacional de continuaciones para poder expresar la pereza de Jauja y los posibles efectos laterales producidos como resultado de la evaluación de una expresión: creación de procesos y comunicaciones subyacentes. La consideración de estos efectos laterales estará implícita en una continuación. El trabajo también empleamos el formalismo denotacional de continuaciones para definir el significado de pH (Parallel Haskell) y de GpH. Para ambos lenguajes ya se habían definido semánticas operacionales, pero las diferencias de base de estas semánticas no permitían una comparación fácil entre los algoritmos escritos en pH, los implementados en GpH y los programados en Jauja. Por esta parte, estos lenguajes son representantes de los tres enfoques fundamentales de introducción de paralelismo en un lenguaje funcional, en el caso que nos ocupa Haskell: pH de paralelismo implícito, GpH de paralelismo semi-explícito y Jauja de paralelismo explícito. De modo que un mismo marco semántico (de continuaciones) nos permite comparar también estos tres paradigmas.

Autor: SÁNCHEZ HERNÁNDEZ JAIME.
Año: 2003.
Universidad: COMPLUTENSE DE MADRID.
Centro de lectura: MATEMÁTICAS.
Centro de realización: FACULTAD DE CC. MATEMÁTICAS.

Resumen: La negación en programación lógica es un tema ampliamente investigado desde los inicios de este estilo de programación. En este trabajo se estudia un recurso similar para la programación lógico-funcional. La contrapartida natural a la negación en el contexto lógico-funcional es el fallo en la reducción, que es donde se centra la tesis. Se toma como referencia la negación constructiva de la programación lógica, que es capaz de encontrar valores para las variables de los objetivos, y en ese mismo sentido, se hace una propuesta de fallo constructivo. En el marco lógico-funcional, el fallo tiene además otros usos interesantes, como las reglas por defecto o la recolección de valores. La investigación toma como punto de partida la lógica de reescritura del marco CRWL, un formalismo bien establecido y estudiado para el paradigma lógico-funcional. El fallo se incorpora a través de una lógica orientada a la reducción conjuntista, elaborando las nociones y propiedades se tiene que una prueba de fallo en esta lógica corresponde a una prueba de fallo en esta lógica corresponde a una prueba de indemostrabilidad con respecto a la lógica de CRWL, con lo que el fallo adquiere una caracterización semántica precisa. Como mecanismo operacional se construye una relación de estrechamiento que también se apoya en la visión conjuntista. Para facilitar la presentación, esta construcción se lleva a cabo en dos etapas: en la primera se descarta la igualdad, que después se analiza como relación aislada y se funde con el mecanismo global de estrechamiento. Por último, se estudia la implementación efectiva del fallo en programación lógico-funcional. Es sencillo extender un lenguaje como TOY o Curry con fallo no constructivo plantea serias dificultades debido al mecanismo de reducción que utilizan estos sistemas. Por ello, se diseña el prototipo experimental OOPS con un mecanismo de reducción basado en la semántica conjuntista estudiada y que es capaz de manipular el fallo constructivo. Este prototipo ha supuesto una valiosa herramienta de investigación con la que experimentar los distintos usos del fallo.

Autor: MARROQUÍN ALONSO OLGA.
Año: 2003.
Universidad: COMPLUTENSE DE MADRID.
Centro de lectura: MATEMÁTICAS.
Centro de realización: FACULTAD DE CIENCIAS MATEMÁTICAS.

Resumen: En el trabajo se realiza un estudio exhaustivo de una extensión con tiempo de PBC (Petri Box Calculus), que es un modelo formal de especificación de sistemas concurrentes en el que se da especial importancia a la sincronización y el paralelismo, y cuya semántica denotacional utiliza como soporte redes de Petri. La Tesis comienza con la exposición detallada de un modelo básico para el que se define una semántica operacional, formada por un conjunto de relgas de transición al estilo Plotkin, y una semántica denotacional, que genera un álgebra de redes de Petri temporizadas. A continuación se introducen los elementos necesarios para incorporar la urgencia en la ejecución de dichas acciones, y al estudio de un nuevo operador, denominado time-out con excepción, que permite el establecimiento de ocmportamientos alternativos. La urgencia de los procesos, característica imprescindible en la modelización de sistemas temporizados reales, se refuerza con una tercera modificación en la que se incorpora el máximo paralelismo, que facilita la ejecución más rápida posible de las acciones de una expresión de proceso. El resultado técnico fundamental del trabajo es la equivalencia entre las semánticas operacional y denontacional del modelo definido, en el sentido de que ambas definen comportamientos equivalentes para cada expresión. Durante todo el análisis, el dominio de tiempo considerado es discreto, pues de esta forma se consiguen importantes simplifaciones, que nos conducen a un modelo más tratable pero suficientemente expresivo. La Tesis se completa con los resultados obtenidos sobre una segunda extensión de PBC que incorpora al Cálculo de Cajas el concepto de ambiente de Cardelli, tratando satisfactoriamente los aspectos relativos a la movilidad. Ello representa una vía de ampliación del modelo básico que incorpora a su semátncia operacional reglas equivalentes a las que definen el Cálculo de Ambientes, y cuya semántica denotacional se realiza por medio de redes anidadas que generalizan el modelo de los Sistemas de Objetos Elementales de Valk. En definitiva, el trabajo contiene una teoría completa para la extensión temporizada y una propuesta de una extensión ambiental de PBC.

Autor: IBRAHIM RASHED ABU DALHOUM ABDEL LATIF.
Año: 2003.
Universidad: AUTONOMA DE MADRID.
Centro de lectura: ESCUELA POLITÉCNICA SUPERIOR.
Centro de realización: ESCUELA POLITÉCNICA SUPERIOR.

Resumen: La informática teórica es una disciplina básica en informática ya que la mayoría de los avances en esta ciencia se sustentan en un sólido resultado de esa materia. En su origen se situaron los desarrollos casi simultáneos de la lógica formal, la electrónica digital y de la lingüística que condujeron a la aparición de la teoría de lenguajes formales y autómatas, rama principal en la formación de todo informático. El objetivo de la tesis es doble: * Profundizar en el estudio teórico de las propiedades formales de los autómatas celulares y los sistemas de Lindenmayer y sus relaciones, en particular, en el diseño de autómatas celulares que simulen la generación de lenguajes de los sistemas de Lindenmayer para continuar trabajos anteriores en esta línea. * Estudio de posibles herramientas para el diseño de sistemas de Liondenmayer y autómatas celulares que resuelvan un problema concreto. Se estudiará la aplicación de las técnicas de los algoritmos genéticos en la solución de este problema y también de la evolución gramatical.

Autor: MEDEROS MARTÍN JORGE.
Año: 2003.
Universidad: POLITECNICA DE MADRID.
Centro de lectura: INFORMÁTICA.
Centro de realización: FACULTAD DE INFORMÁTICA.

Resumen: El presente trabajo estudia las limitaciones en las técnicas actuales de subdivisión de sistemas informáticos y de su emsablado. Este análisis pone en relieve deficiencias -muchas veces conocidas pero aceptadas sin más- en las técnicas usadas. Carencias que aumentan la complejidad percibida de los programas construidos y limitan las posibilidades de creación de componentes. Los modelos de componentes actuales ofrecen únicamente una abstracción parcialmente opaca a los lenguajes de programación con los que se manipulan. La implementación eficiente de componentes demanda además características de programación de sistemas y de bajo nivel en los lenguajes que lo implementan.. A su vez, la programación con los se manipulan. La implementación eficiente de componentes demanda además características de programación de sistemas y de bajo nivel en los lenguajes que los implementan. A su vez, la programación de sistemas se puede beneficiar del uso de componentes para mantener las barreras de abstracción apropiadas y limitar la complejidad. Este trabajo analiza y justifica mejoras en los procesos de construcción de programas, donde se pone mayor énfasis en las propiedades de los productos resultantes -programas que faciliten la construcción de componentes- que en el proceso que los genera. Se describe la definición e implementación de un prototipo de un nuevo lenguaje de programación, llamado XC, usado como ejemplo de implementación de las guías de diseño estudiadas. Se trata de un lenguaje orientado a la programación con componentes que soporta también la programación orientada a objetos y la programación de sistemas, aportando las abstracciones necesarias: Estructura jerárquica de módulos, Interfaces e implementación independientes, herencia múltiple de interfaces y herencia simple de implementación, novedoso modelo de objetos interno modular y extensible pensado para la construcción de componentes, comprobación estricta de tipos, tipos covariantes y tipso genéricos (usando una nueva técnica llamada sustitución de tipos explícita que fomenta la modularidad), optimizaciones de tipos básicos, funciones en línea, funciones y objetos nativos, código no seguro, compilación final a C y sintaxis expresiva.

Autor: MACIA SOLER HERMENEGILDA.
Año: 2003.
Universidad: CASTILLA-LA MANCHA.
Centro de lectura: ESCUELA POLITÉCNICA SUPERIOR.
Centro de realización: ESCUELA POLITECNICA SUPERIOR. ALBACETE (U.C.L.M.).

Autor: MANTAS RUIZ JOSÉ MIGUEL.
Año: 2002.
Universidad: GRANADA.
Centro de lectura: INFORMÁTICA .
Centro de realización: E.T.S. INGENIERÍA INFORMÁTICA.

Resumen: Se aplican los conceptos de software basado en componentes al campo de la integración numérica paralela de Ecuaciones Diferenciales Ordinarias (EDOs), abordando la definición de algoritmos numéricos paralelos útiles y facilitando el diseño e implementación paralela de métodos numéricos de resolución de Ecuaciones Diferenciales. Se integra dentro de un marco metodológico existente para la derivación de programas paralelos de métodos numéricos un enfoque formal para separar la definición y la implementación de los procedimientos paralelos, así como de un mecanismo de especialización de componentes, que habilita la adaptación de las descripciones obtenidas a las características estructurales de los problemas a resolver. El nuevo enfoque obtenido contempla una serie de pasos de transformación que permita adaptar de forma sistemática una descripción del paralelismo funcional de un método numérico a un problema y una arquitectura concretos. El enfoque supone una estructuración y formalización del proceso de derivación de resolutores paralelos de EDOs a partir de módulos de bibliotecas paralelas de álgebra lineal numérica y constituye una base para la automatización parcial o total del proceso de derivación. Esto se consigue tratando de forma separada los aspectos fundamentales en la derivación de resolutores paralelos de EDOs: 1,- Funcionalidad y paralelismo funcional. 2,- Estructura del problema. 3,- Aspectos de diseño paralelo dependientes de la máquina (distribuciones de datos, implementaciones paralelas de las operaciones, planificación de tareas, etc.). Esta separación permite que las especificaciones de los métodos numéricos sean altamente reutilizables, para su adaptación a diferentes aplicaciones y a diferentes máquinas paralelas. Se propone también la optimización de un esquema numérico paralelo existente basado en un método de Rung-Kutta Implícito con 4 etapas y una técnica general para obtener versiones paralelas de métodos de Rung-Kutta Implícitos-Explícitos. Siguiendo la metodología propuesta, se obtienen de forma sistemática, implementaciones paralelas de los esquemas numéricos adaptados a problemas realistas de considerable costo computacional que modelan diversos fenómenos (Evolución de manchas de vorticidad en un fluido incompresible, choques de gases poco densos, etc.).

Autor: VERDEJO LÓPEZ JOSÉ ALBERTO.
Año: 2002.
Universidad: COMPLUTENSE DE MADRID .
Centro de lectura: INFORMÁTICA.
Centro de realización: FACULTAD DE INFORMÁTICA.

Resumen: La lógica de resscritura, propuesta por José Meseguer en 1990 como marco de unificación de modelos de computación concurrente, es una lógica para razonar sobre sistemas concurrentes con estado que evolucionan por medio de transiciones. Desde su definición, se ha propuesto a la lógica de reescritura como marco lógico y semántico en el cual poder expresar de forma natural otras muchas lógicas, lenguajes y modelos de computación. Además, la lógica de reescritura es ejecutable utilizando el lenguaje multiparadigma Maude cuyos módulos son teorías en la lógica de reescritura. El objetivo principal de esta tesis es extender la idea de la lógica de reescritura y Maude como marco semántico a la idea de marco semántico ejecutable. Este objetivo se ha abordado desde diferentes puntos de vista. En primer lugar, presentamos representaciones ejecutables de semántica operacionales estructurales. En concreto, hemos estudiado dos implementaciones diferentes de la semántica de CCS y su utilización para implementar la lógica modal de Hennessy-Milner; hemos realizado una implementación de una semántica simbólica para LOTOS incluyendo especificaciones de tipos de datos en ACT ONE que son traducidos a módulos Maude y de una herramienta que permite al usuario ejecutar directamente sus especificaciones LOTOS; y hemos utilizado las mismas técnicas para implementar otros tipos de semánticas operacionales de lenguajes funcionales e imperativos sencillos, incluyendo tanto semánticas de evaluación (o paso largo) como semánticas de computación (o paso corto). En segundo lugar, hemos querido contribuir al desarrollo de una metodología propuesta recientemente por Denker, Meseguer y Talcott para la especificación y análisis de sistemas basada en una jerarquía de métodos incrementalmente más fuertes, especificando y analizando tres descripciones ejecutables del protocolo de elección de líder dentro de la especificación del bus multimedia en serie IEEE 1394 (conocido como "FireWire"). En dos de estas descripciones hacemos especial énfasis en los aspectos relacionados con el tiempo, esenciales para este protocolo. Por último, hemos abordado la dotación de semántica formal a lenguajes de la web semántica, mediante la traducción del lenguaje de descripción de recursos web RDF (Resource Description Framework) a Maude y su integración con Mobile Maude, una extensión de Maude para permitir cómputos móviles.

Autor: PITA ANDREU M. ISABEL.
Año: 2002.
Universidad: COMPLUTENSE DE MADRID.
Centro de lectura: MATEMÁTICAS.
Centro de realización: FACULTAD DE MATEMÁTICAS.

Resumen: Las técnicas de especificación formal de sistemas concurrentes pueden agruparse en general en dos niveles; en el primero se incluyen las técnicas consistentes en el desarrollo de modelos formales del sistema y en el segundo las técnicas que realizan la especificación del sistema mediante la definición de propiedades abstractas del mismo. El objetivo de esta tesis es proponer una metodología de especificación de sistemas que cubra ambos niveles de especificación mediante el uso de un marco matemático uniforme, proporcionado por la lógica de reescritura y su implementación vía el metalenguaje Maude. La especificación en el primer nivel se realizará directamente en el propio lenguaje Maude, mientras que para realizar la especificación de segundo nivel definiremos una lógica modal para probar propiedades de sistemas especificados en Maude, en la cual las transiciones definidas por las reglas de reescritura se capturan como acciones en la lógica. La lógica definida puede utilizarse además mediante la definición de la interfaz apropiada para probar propiedades específicas en otras lógicas temporales o modales. En la tesis se estudian en primer lugar las especificaciones en el lenguaje Maude. Mediante el desarrollo de una especificación de un modelo orientado a objetos para redes de telecomunicación de banda ancha se muestra el poder del lenguaje para especificar este tipo de sistemas y en particular la relación de herencia, la relación del contenido y las relaciones explícitas de grupo (ser-miembro-de, cliente-servidor, ..). Se estudia el uso de la reflexión en el control de un proceso de modificación de características de la red. En este sentido se combinan ideas del campo de la reflexión lógica con ideas provenientes del campo de la reflexión orientada a objetos mediante el uso de un mediador, un metaobjeto que vive en el metanivel y que tiene acceso a la configuración de la red para su gestión. En segundo lugar se procede a la definición de la lógica modal Verificación Logic for Rewriting Logic (VLRL). La principal característica de esta lógica es que proporciona dos modalidades, una de ellas una modalidad de acción que permite capturar las reglas de reescritura como acciones de la lógica, y la otra modalidad espacial que permite definir propiedades sobre partes del sistema y relacionarlas con propiedades del sistema completo así como definir propiedades sobre acciones realizadas en partes del sistema. La lógica VLRL permite además probar propiedades definidas en otras lógicas modales o temporales mediante la definición de la interfaz apropiada. Se muestra el uso de la lógica en la prueba de propiedades de seguridad de varios sistemas orientados a objetos: un protocolo de exclusión mutua, el sistema del mundo de los bloques y el sistema Mobile Maude como modelo de movilidad de objetos entre procesos. Por último se muestra otro medio de probar propiedades de sistemas especificados en lógica de reescritura mediante un ejemplo en el que se realiza una prueba semi-formal por inducción de propiedades de seguridad y vivacidad del protocolo para la elección de líder del bus en serie multimedia IEEE 1394.

Autor: GARCÍA ARENAS M. ISABEL.
Año: 2002.
Universidad: GRANADA.
Centro de lectura: INFORMÁTICA.

Resumen: Este trabajo está motivado por la necesidad de herramientas de Computación Evolutiva que faciliten la creación de experimentos para aprovechar la potencia disponible en máquinas no locales conectadas a una red como puede ser internet. Esta herramienta, denominada JEO (Objetos Evolutivos en Java), es los suficientemente flexible, potente y fácil y usar como para construir cualquier experimento de forma distribuida. Otra de las característícas más destacables es que permite la creación de experimentos escalables posibilitando así centrar la investigación en el propio experimento y despreocuparse de otros aspectos que pueden no estar tan ligados a los algoritmos. La escalabilidad que adquieren los experimentos construidos con JEO está avalada por un soporte software que permite la construcción de una red punto a punto que implementa un modelo de computación paralela basado en el paso de mensajes. JEO da soporte a la creación de experimentos de los paradigmas tradicionales como son los algoritmos genéticos, las estrategias evolutivas, la programación evolutiva o la programación genética. También proponen un nuevo modelo general de computación evolutiva basado en una economía virtual que ayuda a la evolución de soluciones. JEO está totalmente integrada en un proyecto denominado DREAM (Máquina Distribuida de Recursos para Algoritmos Evolutivos) que permite crear redes punto a punto de nodos de ejecución para los experimentos que se desarrollan. Por último se presentan las características de JEO de forma más detallada. Para probar la utilidad de la herramienta se presentan varios problemas clásicos en Computación Evolutiva y algunos problemas que introducen innovaciones en este campo, dotando a JEO de una potencia que otras herramientas no poseen.

Autor: CUESTA QUINTERO CARLOS ENRIQUE.
Año: 2002.
Universidad: VALLADOLID.
Centro de lectura: INFORMÁTICA.
Centro de realización: FACULTAD DE CIENCIAS/E.T.S. DE INGENIERÍA INFORMÁTICA.

Resumen: Esta tesis se centra en el campo de la Arquitectura de Software, una rama de la Ingeniería de Software dedicada al estudio de la estructura de los sistemas sowftware complejos. Se trata y estudia concretamente uno de los problemas pendientes del campo: la especificación y descripción de arquitecturas de software dinámicas, es decir, aquéllas cuya estructura puede variar. Se parte de un estudio general del estado del arte en este campo, identificando los esquemas básicos propuestos en las literatura. En esta tesis se propone el uso del concepto de Reflexión Computacional, referente a los sistemas software que tratan y actúan sobre sí mismo, como noción unificadora de las distintas propuestas y modelos básicos mencionados, que ha de servir como base para un enfoque más general del problema de la descripción de las arquitecturas de software dinámicas. Para ello se recopilan los principales aspectos vinculados al concepto de Reflexión, y se seleccionan aquéllos que se consideran relevantes en el contexto de Arquitectura de Software. Con éstos se elabora de manera informal un modelo reflexivo de descripción arquitectónica de Software. Con éstos se elabora de manera informal un modelo reflexivo de descripción arquitectónica, capaz de expresar los esquemas básicos de dinamismo identificados. A continuación se plantea una descripción formal de este modo reflexivo. El modelo se desarrolla en tres etapas: en la primera se establecen los conceptos habituales de Arquitectura de Software en términos de teoría de conjuntos y relaicones, dando lugar a un marco de definición formal para las nociones fundamentales de la descripción arquitectónica. En la segunda etapa, se amplía este marco mediante la inclusión de los conceptos reflexivos seleccionados en el punto anterior, dando lugar a una descripción formal del modelo reflexivo allí propuesto, según el cual un esquema se estructura en múltiples estratos descriptivos, denominados meta-niveles. En la tercera etapa, se elabora una versión restringida de este modelo, que permite expresar con mayor simplicidad algunas de las estructuras reflexivas habituales, y que resultan particularmente apropiadas en este contexto. Utilizando como base este modelo, se elabora a continuación un Lenguaje de Descripción de Arquitectura, denominado Pilar. El lenguaje se divide implícitamente en dos fragmentos: El denominado Lenguaje Estructural, que se centra en los aspectos estáticos de la descripción, y el Lenguaje Dinámico, que se encarga de la especificación del comportamiento dinámico asociado a esa estructura. Entre ambos lenguajes, se incorpora la relación de reificación como única noción adicional, que resulta suficiente para el establecimiento de un esquema relfexivo. Lingüísticamente, el Lenguaje Estructural es comparable a cualquier Lenguaje de Descripción de Arquitecturas convencional, incluso del tipo estático, mientras que el Lenguaje Dinámico se enmarca dentro de la familia de los lenguajes, utilizando como base el cálculo-pi, un álgebra de procesos con movilidad, que la desarrolla como una estructura de procesos. Se concluye la tesis mostrando la aplicabilidad del lenguaje para la descripción de diversos sistemas concretos.

Autor: VILLANUEVA GARCÍA ALICIA.
Año: 2002.
Universidad: POLITECNICA DE VALENCIA.
Centro de lectura: INFORMÁTICA.
Centro de realización: DPTO. DE SISTEMAS INFORMÁTICOS Y COMPUTACIÓN.

Resumen: En muchas aplicaciones reales la verificación formal de propiedades temporales es imprescindible. En la bibliografía podemos encontrar muchos casos de estudio en los que parecían cómo las técnicas de verificación formal han permitido detectar errores en sistemas que parecían correctos. El model cheching es una técnica de verificación autonómica que, dado un modelo del sistema y una fórmula temporal, comprueba si el modelo satisface la fórmula. El problema principal del model checking es la explosión de estados. En esta tesis se usa el paradigma Concurrent Constraint (cc) para especificar sistemas reactivos y sistemas híbridos. Se consideran tres lenguajes temporales que han sido definidos a partir del paradigma cc: el lenguaje tcc, el lenguaje tccp y el lenguaje hcc. Los dos primeros pueden modelar sistemas reactivos gracias a que han definidos sobre una noción de tiempo discreto, mientras que el tercer lenguaje es capaz de modelar sistemas híbridos ya que usa una noción de tiempo continuo. Sabemos que una adecuada semántica denotacional permite realizar análisis muy interesantes de lenguajes. Cuando fue introducido el lenguaje tcc se definió su semántica operacional y su semántica denotacional, sin embargo estas dos semántcias a veces no coinciden. En esta tesis se ha definido una semátncia denotacional fully abstract (con respecto a la semántica operacional) para el modelo de programación tcc. Además mostramos un ejemplo de cómo se puede usar esta nueva semántica denotacional para analizar la expresividad del operador de tcc que modela los conceptos de timeout y preemption. Se ha demostrado que la introducción de dicho constructor hace el lenguaje tcc más potente que el paradigma cc. El resultado más importante de esta tesis es la definición de un algoritmo de model checking para el lenguaje tccp. La idea es la de explortar las características del paradigma cc para resolver (en parte) el problema de la explosión de estados. Se ha usado la noción de constraint (restricción) para redefinir dos de las tres fases principales del model checking. Por un lado se ha definido un estado del modelo en base al concepto de restricción. De un modo intuitivo un estado de nuestro modelo representa un conjunto de estados de una estructura de Kripke tradicional. Por otro lado, la lógica que se usa para especificar la propiedad está definida con respecto al concepto de restricción directamente. Esto nos permite no tener que transformar nuestro modelo de un modelo tradicional. Por último, se define un método para verificar programas especificados en el lenguaje hcc. Con hcc se pueden modelar sistemas híbridos en general e híbridos lineales en particular. En esta tesis se introduce un método que construye un autómata híbrido lineal a partir de la especificación, el cual puede ser dado como entrada a uno de los más famosos model chekers del sector.

Autor: FREIRE BRAÑAS JOSÉ ENRIQUE.
Año: 2002.
Universidad: A CORUÑA.
Centro de lectura: INFORMÁTICA.
Centro de realización: FACULTAD DE INFORMÁTICA.

Resumen: Identificación de las estructuras subyacentes a las categorías de Eilenberg-Moore y de Kleisli asociadas a las mónadas usadas en algunos lenguajes funcionales puros para modelizar aspectos imperativos. Dar una adecuada definición de la noción de tipo que permita abarcar estructuras abstractas. Definición de morfismos genéricos sobre esos tipos de forma que, aplicados a parámetros adecuados, posibiliten la construcción de programas funcionales verificables. Generalización de los teoremas de optimización (fusión y deforestación) aplicables a los morfismos previamente declarados. Implementación y optimización en CAML, usando los teoremas descritos en el apartado anterior, de los siguientes problemas: resolución, por medio de un algoritmo de búsqueda ciega, del problema PS de McCarthy, cálculo del número cromático y del spanning-tree de un grafo. Construcción de morfismos sobre tipos anidados con la posibilidad de ser singularizados analizando qué requerimientos son precisos para poder definir tales funciones. Caracterización de las funciones tail-recursive sobre los tipos regulares. Implementación y demostración en Coq de las propiedades previamente reseñadas. Definición en Coq de las funciones primitivo recursivas y de la noción de catamorfismo generalizado. Demostración en Coq del carácter catamórfico de la función de Ackermann. Demostración en Coq de la imposibilidad de declarar la función de Ackermann como catamorfismo generalizado. Caracterización de los cotipos según su carácter coninductivo analizando la equivalencia con su definición en Coq.

Autor: GARCÍA PÉREZ-SCHOFIELD JOSE BALTASAR.
Año: 2002.
Universidad: VIGO.
Centro de lectura: INFORMÁTICA.
Centro de realización: DEPARTAMENTO DE INFORMÁTICA - F. CIENCIAS.

Resumen: Los sistemas persistentes se configuran como uno de los grandes campos de investigación desde 1970, con la venida de las bases de datos orientadas a objetos. Varias razones (rendimiento, filosofía de trabajo, …) han impedido que estos sistemas sustituyan a los actuales. En esta tesis se presenta en primer lugar un estudio sobre los modelos de persistencia y los sistemas persistentes ya existentes. Se desarrolla un nuevo modelo de persistencia, basado en los anteriores, llamado modelo de persistencia basado en contenedores. Este modelo se contrastará con el modelo de persistencia ortogonal (el imperante actualmente) y se demuestra como el primero conlleva significativas mejoras en el rendimiento sobre el segundo. El modelo basado en contenedores se aplica al prototipo barbados, un sistema de programación persistente basado en C++, del que se obtendrá una evaluación del rendimiento real, comprobando si las asunciones son válidas y correctas. Finalmente, la evolución del esquema presenta una de las subáreas más importantes en este campo. Se incluirá una completa definición del diseño de la evolución del esquema aplicable al modelo de contenedores, y por lo tanto, aplicable directamente al prototipo.

Autor: SEGURA DIAZ CLARA M..
Año: 2001.
Universidad: COMPLUTENSE DE MADRID.
Centro de lectura: MATEMATICAS.
Centro de realización: FACULTAD DE CIENCIAS MATEMATICAS.

Resumen: Las tecnicas de analisis de programas se han demostrado útiles en todo tipo de lenguajes de programación para determinar de forma estática aproximaciones a las propiedades dinámicas de los programas. Sus aplicaciones incluyen la optimización y transformación de los programas, asi como la demostración o verificacion de propiedades de los mismos. El desarrollo y la aplicación de las tecnicas de análisis a los lenguajes funcionales ha sido muy amplio en estas dos ultimas décadas. Esta tesis se enmarca en el área de análisis estáticos de programas aplicados a los lenguajes funcionales paralelos. La programación funcional paralela es un área de investigación intensa en la actualidad que proporciona nuevos problemas en el campo de los analisis de programas, pero es aun un area poco trabajada donde queda mucho por hacer. En esta tesis se definen tres análisis aplicados al lenguaje funcional paralelo Eden: -Analisis de conexión directa: tiene como objetivo optimizar los programas Eden reduciedo sobrecargas debidas a la creación de procesos y a la comunicación entre ellos. -Analisis de no determinismo: pretende delimitar aquellas partes de los programas Edén donde es posible mantener el razonamiento ecuacional caracteristico de los lenguajes funcionales. -Analisis de terminación y productividad: es un sistema de demostración de propiedades de terminacion y productividad de los programas Edén que garantiza la ausencia de bloqueos en ellos. Para definir estos análisis se han utilizado algunas de las tecnicas usadas en el análisis de los lenguajes funcionales: la interpretación abstracta y los sistemas de tipos anotados.

Autor: VIZCAINO BARCELO AURORA.
Año: 2001.
Universidad: CASTILLA-LA MANCHA.
Centro de lectura: INFORMATICA.
Centro de realización: ESCUELA SUPERIOR DE INFORMATICA.

Autor: GIRONÉS TORRENT XAVIER.
Año: 2001.
Universidad: GIRONA.
Centro de lectura: CIENCIAS.
Centro de realización: INSTITUTO DE QUIMICA COMPUTACIONAL.

Resumen: La Tesis se divide en tres partes claramente diferenciadas. En la primera se repasa el concepto del uso de funciones densidad electrónicas de primer orden ajustadas en cálculos de semejanza molecular quántica. Así como su utilización posterior en la representación gráfica de isocontornos de densidad electrónica. El uso de estas funciones densidad ajustada permite una representación, aunque simplificada de la densidad real obtenible a partir de complejos cálculos ab initio, resultando en un ahorro considerable de tiempo de cálculo al realizar medidas de semejanza molecular quántica o la representación de los mencionados contornos de densidad. El sengudo bloque de la tesis englobal el concepto de alineamiento molecular, abordado desde el punto de vista introductivo y cubriendo un amplio rango de aplicaciones. Asimismo, se trata la estrecha relación existente entre el alineamiento molecular y las medidas de semejanza molecular quántica, ya que la magnitud de la misma depende de la orientación relativa de los objetos, normalmente estructuras moleculares, en el espacio tridimensional. Finalmente, se expone una nueva propuesta de algoritmo de alineamiento molecular, desarrollada en el departamento y bautizada como "Topo-Geometrical Superposition Algorithm (TGSA), la cual se ha implementado en un programa informático, TGSA99. La última parte está dedicada a la teoría de la semejanza quántica, con especial devoción a su aplicación práctica en el campo de la Relaciones Cuantitativas Estructura-Propiedad, comúnmente denominadas por su acrónimo QSAR. En primera instancia se aborda el trasfondo teórico de las medidas de semejanza, con especial antención a su derivación conceptual y aplicaciones prácticas. Finalmente, se exponen ejemplos de aplicación dentro de tres derivaciones diferentes: 1,- Utilizando matrices de semejanza. 2,- Energía de interacción electrón-electrón asimilada en el contexto de la semejanza como una medidad de autosemejanza. 3,- Uso de densidades de agujero de Fermi como densidad alternativa, y intermedia, entre el uso de densidades electrónicas completas y densidades de fragmentos en el estudio de los efectos de la substitución sobre la respuesta molecular.