MATERIA: Semántica y verificación

CLAVE: COMP-820

SEMESTRE DE UBICACION: Octavo

AREA: Ciencias de la computación

OBJETIVOS: El énfasis en este curso es la representación y manipulación, así como la aplicación de sistemas formales en la computación. Se discutirán temas de lógica, conjuntos, álgebra, complejidad y computabilidad y se verán sus posibles aplicaciones, una de ellas la formalización de la semántica de los lenguajes de programación y la verificación de programas

TEMARIO:

  1. Introducción

    • Un ejemplo

    • Sintaxis Abstracta

    • Ejecución secuencial

    • Expresiones

    • Comandos de control de flujo

  2. Notación-l

    • Dominios. Funciones

    • Cálculo-l sin tipos. Conversión. Evaluación. Constantes. Funciones de orden superior

    • Recursión. Operador Y de punto fijo

    • Cálculo-l con tipos. Constructores de tipos

    • Cálculo-l polinórfico

  3. Latices

    • Cardinalidad. El problema de Términacion (Halting Problem)

    • Estructura de las latices. Órdenes parciales. Operaciones entre latices. Latices de funciones. Puntos fijos minimales

    • Dominios recursivos. Listas y secuencias. Contrucción del límite inverso. Los tipos como ideales

  4. Un lenguaje simple

    • Definición completa de un lenguaje simple

    • Ejemplos

  5. Semántica directa

    • Efectos laterales

    • Errores y significados "erróneos"

    • Salida

    • Una traducción de Pascal

  6. Control

    • Comandos de control

    • Continuaciones

    • Salidas y respuestas

    • Efectos laterales y secuencias

    • Continuación de declaraciones

    • Funciones y parámetros

    • Semántica Estándar

    • Una traducción de Algol-68

  7. Estructuras de datos y tipos en los datos

    • Semántica dinámica de las estructuras de datos

    • Chequeo estático de tipos. Tipos identificados. Tipos recursivos. Tipos parametrizados

    • Interpretaciones no estándar

  8. Semántica de Prolog

    • Prolog. Ejecución. Ejemplo: append. Difernciador

    • Una definición formal. Sintaxis. Dominios semánticos. Ecuaciones semánticas. Unificación. Funciones auxiliares

    • Una traducción de Algol-68

  9. Colofón

    • Intérpretes y compiladores de compiladores

    • Concurrencia

BIBLIOGRAFIA:

  • Allison, L., A practical introduction to denotational semantics, Cambridge University Press, 1986

  • Gries, D.; Editor, Programming In The 1990s, An Introduction To The Calculation Of Programs, Springer Verlag, 1990

BIBLIOGRAFIA COMPLEMENTARIA:

  • Winblad, A. L.; Edwards, S. D. ; King, D. R., Object-Orifented Software, Addison-Wesley Publishing Company, 1990

  • Dijkstra, E. W., Formal Development Of Programs And Proofs, Addison-Wesley Publishing Company, 1990

  • Janicki, R. ; Koczdodaj, W. W.; Editores, Computing And Information, North-Holland, 1989

  • Manna, Z.; Waldinger, R., The Logical Bases For Computing Programming, Volume 1: Deductive Reasoning, Volume 2: Dedictive Systems, Addison-Weslesy Publishing Company, 1990

  • Marin, J., Systems Design From Provably Correct Constructs, Prentice Hall, Inc., 1985

  • Sperschneider, V.; Antoniou, A., Logic: A Foundation For Computer Science, Addison-Wesley Publishing Company, 1991