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 interpretação abstrata 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

Há 2 regimes da avaliação à escolha para obter aprovação nesta UC, a saber:
. Regime A) 2 testes sem consulta cuja média seja = 10, com nota máxima de 14 valores. Aos alunos com média no intervalo [8..10[ será facultada a possibilidade de fazerem uma oral.
. Regime B) 2 testes sem consulta com nota mínima 8, cuja média valerá 60% da nota final + realização de um trabalho prático de grupo de 3 alunos com nota mínima 10 (40% da nota final). O trabalho é avaliado através de um relatório e uma defesa oral.

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.