Análisis de datos de periódicos digitales

En este proyecto se ha desarrollado una aplicación Web cuya finalidad es ofrecer al usuario datos provenientes del análisis de texto de las noticias que se encuentran en periódicos online. La aplicación permite al usuario realizar búsquedas personalizadas sobre temáticas específicas y configurar algunos tipos de análisis sobre la información recuperada. Entre los análisis que son llevados a cabo destaca el análisis del sentimiento. Para ello se ofrece la posibilidad de que el usuario utilice sus propios diccionarios de pares palabra-valor, utilizados para realizar este tipo de análisis. Para la codificación de la herramienta, se ha utilizado el lenguaje de programación Python y la framework web Django. El almacenamiento de la información de la aplicación se ha realizado sobre una base de datos NoSQL de tipo MongoDB.

Verificación de algoritmos y estructuras de datos en Dafny

La verificación formal de un programa es la demostración de que este funciona de acuerdo a una descripción del comportamiento esperado en toda posible ejecución. La especificación de lo deseado puede utilizar técnicas diversas y entrar en mayor o menor detalle, pero para ganarse el título de formal esta ha de ser matemáticamente rigurosa. El estudio y ejercicio manual de alguna de esas técnicas forma parte del currículo común a los estudios de grado de la Facultad de Informática y del itinerario de Ciencias de la Computación de la Facultad de Ciencias Matemáticas de la Universidad Complutense de Madrid, como es el caso de la verificación con pre- y postcondiciones o lógica de Hoare. En el presente trabajo se explora la automatización de estos métodos mediante el lenguaje y verificador Dafny, con el que se especifican y verifican algoritmos y estructuras de datos de diversa complejidad. Dafny es un lenguaje de programación diseñado para integrar la especificación y permitir la verificación automática de sus programas, con la ayuda del programador y de un demostrador de teoremas en la sombra. Dafny es un proyecto en desarrollo activo aunque suficientemente maduro, que genera programas ejecutables.

Extensiones de bases de datos relacionales y deductivas: fundamentos teóricos e implementación

En esta memoria hacemos contribuciones dentro del campo de los lenguajes de bases de datos. Nos hemos propuesto tres objetivos fundamentales: 1. Mejorar la expresividad de los lenguajes de bases de datos actuales. 2. Desarrollar semánticas formales para nuestras propuestas de lenguajes de bases de datos extendidos. 3. Llevar a cabo la implementación de las semánticas anteriores en sistemas de bases de datos prácticos. Hemos conseguido estos tres objetivos en distintas áreas dentro de las bases de datos. Por un lado, en el campo de las bases de datos deductivas, proponemos HH:(C). Este lenguaje extiende las capacidades de los lenguajes de bases de datos deductivos con restricciones dado que permite consultas hipotéticas y cuanti cación universal. Por otro lado, utilizamos el estudio dentro de las bases de datos deductivas y lo aplicamos a las bases de datos relacionales. En concreto proponemos HR-SQL que incorpora consultas hipotéticas y de niciones recursivas no lineales y mutuamente recursivas. La idea tras esta propuesta es superar algunas limitaciones expresivas del lenguaje estándar de de nición de bases de datos SQL. A continuación introducimos ambas aproximaciones. Las fórmulas de Harrop hereditarias con restricciones, HH(C), se han usado como base para lenguajes de programación lógica con restricciones. Al igual que la programación lógica da soporte a lenguajes de bases de datos deductivas como Datalog (con restricciones), este marco se usa como base para un sistema de bases de datos deductivas que mejora la expresividad de los sistemas aparecidos hasta el momento. En el segundo capítulo de esta memoria se muestran los resultados teóricos que fundamentan el lenguaje HH:(C) y una implementación concreta de este esquema que demuestra la viabilidad y expresividad del esquema. Las principales aportaciones con respecto a Datalog son la incorporación de la implicación intuicionista, que permite formular hipótesis, y el uso de cuanti cadores incluso en el lenguaje de restricciones. El sistema está diseñado de forma que soporta diferentes sistemas de restricciones. La implementación incluye varios dominios concretos y también funciones de agregación y restricciones de integridad que son habituales en otros lenguajes de bases de datos relacionales. El signi cado del lenguaje se de ne mediante una semántica de pruebas y el mecanismo operacional se de ne mediante una sem ánica de punto jo que es correcta y completa con respecto a la primera. Para el cómputo de las consultas hipotéticas y de las funciones de agregación se hace uso de una noción de estrati cación más compleja que la que usa Datalog. La semántica de punto jo desarrollada constituye un marco apropiado que lleva a la implementación de un sistema concreto...