MFES
Índice
Cálculo de Sistemas de Informação
2020/21
Atendimento electrónico
Programa
- Métodos formais e qualidade de software
- Conceitos básicos: modelo, especificação, verificação e prova.
- Cálculo relacional básico
- As relações binárias polimórficas como linguagem de especificação formal universal
- Taxonomia relacional
- Combinadores relacionais e suas propriedades.
- Cálculo relacional avançado
- Conexões de Galois e igualdade indirecta
- Catamorfismos e hilomorfismos relacionais.
- Aplicações
- Polimorfismo paramétrico: cálculo de teoremas grátis
- Lógica de Hoare em formato relacional
- Modelos de dados relacionais
- Tipos relacionais e cálculo de invariantes
- ‘Design by contract’ por cálculo
- Interpretação abstracta.
Docente e Horário
| Docente | Foto | Horário | Sala |
|---|---|---|---|
| José Nuno Oliveira |  |
5a-feira, 13h-16h | CP1 1.21 |
Alunos
| # | Nome | Curso |
|---|---|---|
| a83916 | Ana João Dias de Almeida | MiEI |
| a85516 | António Manuel Carvalho Gonçalves | MiEI |
| a82529 | Carlos Manuel Marques Afonso | MiEI |
| a34900 | Cecília da Conceição de Oliveira Soares | MiEI |
| a67683 | César Eduardo da Silva Magalhães | MiEI |
| pg41842 | César Hugo Moreira da Silva | MEI |
| a80970 | Davide da Silva Matos | MiEI |
| a76089 | Etienne da Silva Filipe Amado da Costa | MiEI |
| a85731 | Gonçalo José Azevedo Esteves | MiEI |
| a86617 | Gonçalo Pinto Nogueira | MiEI |
| a81283 | Hugo Filipe Oliveira de Sousa Faria | MiEI |
| a85573 | Jorge Gabriel Alves Cerqueira | MiEI |
| a84776 | José Emanuel Silva Rodrigues | MiEI |
| pg42839 | José Gonçalo Macedo Costa | MEI |
| a84577 | José Pedro Oliveira Silva | MiEI |
| a85954 | Luís Mário Macedo Ribeiro | MiEI |
| a78566 | Marcos Daniel Teixeira da Silva | MiEI |
| a71407 | Maurício Zulueta Lima Salgado | MiEI |
| a82400 | Márcio Alexandre Mota Sousa | MiEI |
| a85700 | Pedro Miguel Araújo Costa | MiEI |
| a84783 | Pedro Miguel Borges Rodrigues | MiEI |
| a86266 | Rafael Inácio Lourenço | MiEI |
| a75411 | Ricardo Guerra Leal | MiEI |
| a81716 | Rodolfo António Vieira da Silva | MiEI |
| a80789 | Rui Filipe Brito Azevedo | MiEI |
| pg36086 | Vítor Hugo Gonçalves Silva | MMC |
Método de avaliação
- Duas provas escritas de avaliação (mini-teste + teste) e exame de recurso. / 2 written exams
- As provas escritas são de consulta de material impresso. / The exams are open-book
- O mini-teste é eliminatório de matéria para o teste e vale 50%. / The first exam amounts to 50% of the final mark
Classificações
Retiradas para cumprimento do GDPR.
Material Pedagógico
Enunciados de provas de avaliação
Slides
- Slides da aula de 7-Jan
Casos de estudo
- Mercearia da D. Acácia - queries são paths em diagramas relacionais. (Alloy)
- Liga de futebol - quocientes de funções. (Alloy)
- Sinalização ferroviária - diferença relacional. (Alloy)
- Plano de estudos do MiEI - pré-condições mais fracas; redundância de invariantes.
Código
- Módulo Alloy: RelCalc.als - Cálculo relacional básico em Alloy.
- Módulo Alloy: kerimg.als - o que é o núcleo (kernel) e a imagem (image) de uma relação? Experimentem e observem variando a cláusula run.
- Módulo Alloy: prod.als - produtos cartesianos em Alloy.
- Script básica alloy.sed para converter instâncias geradas pelo Alloy para Haskell - em Alloy, visualizar instância em modo Txt e copiar para ficheiro, eg. i.txt; de seguida correr, numa shell, sed -f alloy.sed i.txt
Bibliografia
- J.N. Oliveira. Program Design by Calculation, Departamento de Informática, Universidade do Minho. Textbook in preparation. Chapters relevant for this course: 5, 6, 7 (and possibly 8, time permitting).
Outras leituras recomendadas
- 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 (first edition). (345 pages)