FACULTAD DE CIENCIAS EXACTAS

     Optativa 2003

     METODOS RELACIONALES PARA LA ESPECIFICACION DE SOFTWARE

    Profesor: Dr. Marcelo Frias
    Prof. Asociado, Departamento de Computacion, Facultad de Ciencias
    Exactas y Naturales, Universidad de Buenos Aires

    Contact Information:  mfrias@dc.uba.ar

El curso pretende introducir al alumno a la especificacion formal de software utilizando herramientas provenientes del calculo relacional de Tarski [Tar87]. El mismo permite especificaciones de programas ("in the small") y tambien de sistemas ("in the large"). Para la especificacion de programas se aprovecha que los mismos se pueden especificar por medio de su relacion de entrada-salida. Para la especificacion de sistemas se aprovecha la posibilidad de expresar objetos por medio de relaciones n-arias entre sus atributos. Introduccion a la logica ecuacional [Bur]. Sintaxis, semantica, deduccion.
Introduccion a la logica de primer orden [End] Sintaxis, semantica, deduccion.
Introduccion al calculo relacional [Fri02]. Sintaxis, algebras relacionales.
El lenguaje de especificacion Alloy [Jac02]. Sintaxis, semantica y ejemplos.
La herramienta de analisis de especificaciones ALCOA [Jac].
Introduccion a las Fork Algebras [Fri02], Sintaxis, representabilidad, expresividad.
El lenguage de Especificacion Ag [Fri02a]. Sintaxis, semantica y ejemplos de especificaciones.
Logica dinamica.
El proyecto ARgENTUM. [Bur81] Burris S. and Sankappanavar, H., A Course in Universal Algebra, Graduate Texts in Mathematics; Springer-Verlag, 1981.
[End01] Enderton H., A Mathematical Introduction to Logic, Academic Press, 2001.
[Fri02] Frias M.F., Fork Algebras in Algebra, Logic and Computer Science, World Scientific Publishers, Series: Advances in Logic, Vol. 2, 2002.
[Fri02a] Frias, M.F., Baum, G.A., López Pombo, C., A Comparisson of Ag with Alloy, in Abstracts of RelMiCS 2001, The Netherlands, October 2001.
[Jac02] Jackson D., Alloy: A Lightweight Object Modelling Notation, ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 11, Issue 2 (April 2002), pp. 256-290.
[Jac00] Jackson D., Schechter I. and Shlyakhter I., Alcoa: the Alloy Constraint Analyzer, Proceedings of the International Conference on
Software Engineering, Limerick, Ireland, June 2000.
[Tar87] Tarski, A. and Givant, S., A Formalization of Set Theory without Variables, A.M.S. Coll. Pub., vol. 41, 1987.

        EVALUACION DEL CURSO

        ATENCION ! - Corrección ejercicio 1 de deduccion natural, inciso (2)
        El ejercicio a resolver es el siguiente (cambia el AND por un =>)      
        (Existe x) (a(x) AND b(x)) => ((Existe x) a(x) => (Existe x) b(x))
         You will also need to install the Java Runtime Environment. Version note: 1.2 or later required.
        To run alloy, type java -jar alloy.jar in the newalloy/ directory.


Last update 24th June, 2003