Departamento de Informática (UM)

Cálculo de Sistemas de Informação

9397 [ME78ME7800006081]

Mestrado em Engenharia Informática [MEINF]

S2

José Nuno Fonseca Oliveira

Objetivos

Recurso uniforme à álgebra das relações binárias como linguagem universal para abordar problemas em geral e o desenho de software em particular sob uma perspectiva científica (cf. lema “relational thinking”). O método permite abordar, de forma unificada, tópicos aparentemente díspares como a tipificação polimórfica, o modelo de dados key-value-pair e a lógica de Hoare, como “exercícios” de cálculo na mesma álgebra.

Programa

1. Breve Introdução aos métodos formais e seu papel na programação.
2. Uso de relações binárias na modelação abstracta de problemas ('relational thinking'). Taxonomia e álgebra das relações binárias.
3. O lema "everything is a relation". 'Model checking' usando a ferramenta Alloy.
4. Uso de interpetação abstracta na modelação de problemas complexos.
5. Cálculo relacional de propriedades grátis de funções com tipos polimórficos.
6. Demonstração de correcção por cálculo, usando álgebra relacional.
7. Formalização relacional do modelo de dados 'key-value pair'.
8. Limites da tipificação estática. Noção formal de contrato de software. Cálculo de pré-condições mais fracas.
9. Lógica de Hoare em formato relacional.

Bibliografia

J.N. Oliveira. Program Design by Calculation, 2008. Draft of textbook in preparation, current version: October 2019. Chapters 5 to 7. Available from http://www.di.uminho.pt/~jno/ps/pdbc.pdf. Informatics Department, University of Minho.

D. Jackson. Software abstractions: logic, language, and analysis. Revised edition, MIT Press, 2012.

C.B. Jones. Systematic Software Development Using VDM. Series in Computer Science. Prentice-Hall International, 1986.

Resultados da aprendizagem

- Abordar problemas através de modelos abstractos
- Verificar sistemas de software por cálculo
- Adoptar o método "Relational Thinking" fazendo 'model checking' com a ferramenta Alloy
- Abordar com rigor o modelo de bases de dados 'key-value pair'
- Demonstrar a correcção de programas usando álgebra relacional
- Conhecer a noção formal de contrato de software e sua validação por cálculo.

Método de avaliação

1. Duas provas de avaliação individual (testes) e exame de recurso.
2. Avaliação contínua com base em problemas dados nas aulas TP.
3. As provas escritas são de consulta de material impresso (apenas).

NB: está previsto um novo regime de avaliação em que um dos testes será substituído por um trabalho de grupo a valer 40% da nota final.

Funcionamento

Turno: T 1; Docente: José Nuno Fonseca Oliveira; Dep.: DI; Horas: 30.
Turno: TP 1; Docente: José Nuno Fonseca Oliveira; Dep.: DI; Horas: 15.