Ir al contenido

Doctorado en Tecnologías para el Desarrollo de Sistemas Software Complejos

Desarrollo Riguroso de Software mediante Tecnología Declarativa

Profesor:
Manuel Carro Liñares
Despacho:
D-2307
Teléfono:
91 336 7455
e-mail:
mcarro@fi.upm.es
Profesor:
Julio Mariño Carballo
Despacho:
D-2310
Teléfono:
91 336 7456
e-mail:
jmarino@fi.upm.es
Créditos:
6
Concentración:
Secundaria
Cuatrimestre:
Primero

Resumen:

Foreign students: Please find here the working page of this subject. It contains an English version of the core information contained in this page, plus it will give you some feeling of the topics covered throughout the course.

El software desarrollado hoy en día es cada vez más complejo y se encarga de actividades cada vez más cotidianas e importantes; por tanto, la fiabilidad y calidad (hasta puntos muchas veces no tenidos en cuenta) de este software son aspectos cada vez más relevantes, debido al uso de los computadores en nuevas actividades, disciplinas y sistemas. Las tecnologías de desarrollo de software requieren ahora primar aspectos relativos al diseño correcto (y la reutilización de diseños correctos) y que permita la comprensión fácil y única del significado de un programa. Entendiendo como "significado" de un programa lo que éste "hace", la frase anterior encierra:

Hay muchos modos de intentar alcanzar los objetivos anteriormente mencionados. El enfoque que las tecnologías declarativas utilizan pasa por disponer de métodos de especificación adecuados y lenguajes de programación de alto nivel que tienen un sólido fundamento matemático. Esto incluye lenguajges de especificación (VDM, Z, OBJ, ...), lenguajes funcionales (Haskell, Erlang, λ-calculi, ... ), lenguajes lógicos (Prolog, CLP, ...), entre otros.

Estos lenguajes, por un lado, liberan al programador de tareas monótonas y repetitivas y permitan llegar a un mayor nivel de abstracción de modo sencillo, y por otro facilitan las labores de compiladores avanzados (comprobación de terminación, uso de sistemas de tipos avanzados, comprobación de propiedades de seguridad, etc.)).

En el curso se estudiarán los fundamentos de algunos lenguajes de programación y especificación basados en tecnología declarativa. En particular, el curso aborda, a alto nivel y centrándose en sus aspectos fundamentales (que no tienen por qué ser los básicos) la programación funcional, la programación lógica y los lenguajes de especificación. Se espera que el alumno que acuda a este curso tenga un conocimiento mínimo de, al menos, programación lógica y funcional y se sienta cómodo leyendo e interpretando fórmulas de lógica formal y pruebas formales de teoremas / propiedades.

Objetivos:

Programa:

El programa que aparece a continuación no sigue, necesariamente, la sucesión cronológica de los temas del curso. Dado que el número de alumnos no suele ser muy alto y de procedencia diversa, intentamos adaptar la forma de exposición a las peculiaridades de cada año.
  1. Introducción, bibliografía ampliada, propuestas de temas de trabajo.
  2. Programación basada en la lógica. Demostración como computación. El lenguaje PROLOG como un compromiso.
  3. Programación basada en restricciones. Lenguajes lógicos con restricciones y lenguajes generales de restricciones. Un ejemplo: FD y algoritmos de resolución. Lenguajes concretos: CLP(FD), CLP(R), CLP(Q).
  4. Programación funcional. Cálculo lambda. Un lenguaje funcional moderno: Haskell. Sistemas de tipos. Temas avanzados.
  5. Métodos formales. Especificación y su papel en el desarrollo de programas. Lenguajes de especificación. Familias de lenguajes de especificación. Verificación.
  6. El lenguaje de especificación VDM. Precondiciones, postcondiciones, invariantes, especificaciones explícitas e implícitas. Sistema de tipos. Generación de código.
  7. Presentación de trabajos de clase.

Bibliografía:

Sobre métodos formales

OBJ y especificación algebraica

Referencias sobre VDM

Referencias sobre Z

Sobre programación declarativa

Lógica formal

Prerrequisitos:

Lógica; programación lógica básica; programación funcional básica; buen conocimiento de técnicas de programación generales; experiencia en proyectos software de al menos mediano tamaño (1000 a 10000 líneas).

Método de Evaluación:

Idiomas en que se imparte:

Inglés