UNIVERSIDAD DE BUENOS AIRES

 

FACULTAD DE CIENCIAS EXACTAS Y NATURALES

 

Departamento de Computación.

 

Segundo Cuatrimestre 2004

 

 

 

Tópicos de Métodos Relacionales en Ciencias de la Computación

 

Dr.  Marcelo Frías

 

 

 

 

 

HORARIO :  T/P miercoles y viernes   10 a 13 hs.,   HORARIO FINAL A CONVENIR CON LOS ALUMNOS

                    

ASIGNATURAS CORRELATIVAS: Logica y Computabilidad

 

PUNTAJE: 4

 

FORMA DE EVALUACIÓN:

Trabajo práctico para aprobación de prácticos, monografía y coloquio para firma del final.

 

PROGRAMA

I Introducción

 

Los métodos relacionales consisten en el uso de formalismos basados en relaciones, y más precisamente,

en formalismos basados en el cálculo relacional de Tarski [T41]. En esta materia analizaremos distintas

aplicaciones de estos formalismos en Ciencias de la Computación. Entre ellas, el uso de distintas

extensiones del cálculo relacional para la especificación y verificación de software. Nos concentraremos

en el estudio de algunos temas específicos a partir de los cuales los alumnos tendrán que realizar

aportes y desarrollo de software que demuestre la utilidad de estos últimos.

 

II Fundamentos

 

En esta parte de la materia nos concentraremos en la relación entre las álgebras de relaciones

(mayormente de relaciones binarias) y el cálculo relacional. Se introducirá el formalismo de la lógica ecuacional, y se presentará al cálculo relacional como una teoría ecuacional. Se discutirá el problema

de la representabilidad de las álgebras relacionales. Se presentarán resultados que relacionan la

lógica ecuacional con propiedades algebráicas de sus modelos. Subalgebras. Productos Directos.

Álgebras simples. Imágenes homomorfas. Variedades.

 

III TOPICOS DE METODOS RELACIONALES

 

Especificación de software utilizando extensiones del cálculo relacional.

Álgebras relacionales quasi-proyectivas [TG87].

Fork álgebras [F02].

El lenguaje de especificación Alloy [J01].

Verificación de especificaciones relacionales.

Demostración semi-automática de teoremas en extensiones del cálculo relacional.

Interpretabilidad de lógicas aplicadas, a extensiones del cálculo relacional.

El proyecto ARGENTUM.

 

IV DESARROLLO

 

En esta etapa de la materia, en base al estudio realizado previamente, se estudiarán posibles

avances en los tópicos descriptos en la Sección III y se realizarán desarrollos de software

tendientes a comprobar la utilidad de los mismos.

 

BIBLIOGRAFIA

 

(Mínima para la descripción del programa de la materia, los alumnos tendrán

acceso abundante bibliografía sobre el tema).

 

[F02] Frias M., Fork Algebras in Algebra, Logic and Computer Science, World Scientific Publishing Co.,

Series Advances on Logic, 2002.

 

[J01] Jackson, D., Shlyakhter, I., and Sridharan, M., A Micromodularity Mechanism. Proc.

ACM SIGSOFT Conf. Foundations of Software Engineering/European Software Engineering

Conference (FSE/ESEC '01), Vienna, September 2001.

 

[T41] Tarski, A., On the Calculus of Relations, Journal of Symbolic Logic} (1941), vol. 6, pp. 73-89.

 

[TG87] Tarski, A.and Givant, S.,A Formalization of Set Theory without Variables}, A.M.S. Coll.

Pub., vol 41, 1987

 

Marcelo Frias