Teoria da Programação II
Fundamentos Lógicos
Elementos Lógicos da Programação I

Disciplina da Secção de Ciência da Computação.

Cursos:
LEIC (Licenciatura em Engenharia Informática e de Computadores). Ano: 3. Semestre: 1.
LMAC (Licenciatura em Matemática e Computação). Ano: 3. Semestre: 1.

Professora Responsável: Paula Gouveia.

Semestre corrente: Avisos e outras informações.

Objectivos

Introdução aos fundamentos lógicos da engenharia da programação: lógica temporal para especificação e verificação de sistemas concorrentes e reactivos. Experimentação com a ferramenta STeP: descrição de sistemas concorrentes na linguagem SPL; especificação e verificação de propriedades de sistemas concorrentes.

Programa mínimo

Sistemas de transições. Linguagem SPL (Simple Programming Language): sintaxe e semântica sobre sistemas de transições justos. Exemplos incluindo diversos casos típicos no contexto dos sistemas distribuídos (eg protocolos). Lógica temporal linear: sintaxe e semântica. Especificação temporal de sistemas concorrentes e reactivos: propriedades de segurança, garantia, resposta e persistência. Verificação de programas: sistema dedutivo; verificação algorítmica em sistemas de transições finitos. Especificação e verificação de sistemas com a ferramenta STeP (Stanford Temporal Prover).

Bibliografia

• N.  Bjorner, A. Browne, E. Chang, M. Colon, B. Finkbeiner, A. Kapur, Z. Manna, H. Sipma, T. Uribe. STeP: The Stanford Temporal Prover
  (Educational Release), User's Manual. Technical  report, U. Stanford, 1997.
• R. Goldblat. Logics of Time and Computation.
  CSLI, 1992.
• P. Gouveia e H. Lourenço. Folhas de apoio para a disciplina de Teoria da Programação II.
  DMIST, 1999.
• N. Lynch. Distributed Algorithms.
  Morgan Kaufmann Publishers, 1996.
• Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems - Safety.
  Springer-Verlag, 1995.
• G. Tel. Introduction to Distributed Algorithms.
  Cambridge University Press, 1994.

Última actualização: 28 de Setembro de 1999.