2020/21
Avisos
Avisos anteriores
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
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
Classificações após correcção do teste: # = a34900, A = 5.9, B = F, NF = - ; # = a67683, A = 6.4, B = 3.6, NF = 10.0 ; # = a71407, A = 4.5, B = F, NF = - ; # = a75411, A = F, B = F, NF = - ; # = a76089, A = D, B = F, NF = - ; # = a78566, A = F, B = F, NF = - ; # = a80789, A = 9.6, B = 5.9, NF = 15.5 ; # = a80970, A = F, B = F, NF = - ; # = a81283, A = 5.0, B = 1.8, NF = 6.8 ; # = a81716, A = 4.8, B = 7.3, NF = 12.1 ; # = a82400, A = 7.0, B = 4.1, NF = 11.1 ; # = a82529, A = 4.4, B = 3.1, NF = 7.5 ; # = a83916, A = 6.9, B = 7.3, NF = 14.2 ; # = a84577, A = 8.3, B = 8.6, NF = 16.9 ; # = a84776, A = 7.0, B = 5.6, NF = 12.6 ; # = a84783, A = 9.8, B = 7.6, NF = 17.4 ; # = a85516, A = 5.4, B = F, NF = - ; # = a85573, A = 8.8, B = 4.8, NF = 13.6 ; # = a85700, A = 9.5, B = 8.6, NF = 18.1 ; # = a85731, A = 8.1, B = F, NF = - ; # = a85954, A = 8.9, B = 9.1, NF = 18.0 ; # = a86266, A = 7.8, B = 6.9, NF = 14.7 ; # = a86617, A = 6.9, B = 4.9, NF = 11.8 ; # = pg36086, A =
4.5, B = 1.9, NF = 6.4 ; # = pg41842, A = 7.4, B = 6.3, NF = 13.7 ; # = pg42839, A = 7.1, B = 2.9, NF = 10.0
Material Pedagógico
Enunciados de provas de avaliação
Slides
Casos de estudo
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
Ferramentas
Programa detalhado
