Docente | Foto | Horário![]() | Sala |
---|---|---|---|
José Nuno Oliveira | ![]() | 5a-feira, 14h+17h | Sala 1.16 (antiga 1.08) |
Afonso João Borges Cabral Cerejeira da Silva | a70387 |
André Brandão de Pinho | a71841 |
André Sousa Diogo | a75505 |
Bruno Miguel Sousa Cancelinha | a75428 |
Bruno Renato Fernandes Carvalho | a67847 |
Diana Filipa Oliveira | a67652 |
Gerson Benjamim Hungulu | pg35957 |
Guilherme Vasconcelos da Silva Guerreiro | a73860 |
João Carlos Mendes Pereira | a75273 |
João Paulo Ribeiro Alves | a73542 |
Lisandra Maria Pereira da Silva | a73559 |
Marcelo António Caridade Miranda | a74817 |
Introdução aos métodos formais e seu papel na programação. Verificação e cálculo de soluções informáticas. Problemas e sistemas de informação para os resolver. Modelos e seu papel na concepção de soluções. Importância da abstracção na captação de requisitos. Limites da tipagem estática. Papel das relações binárias na modelação formal. Bases de dados seguindo o modelo 'key-value pair'. Taxonomia e álgebra das relações binárias. O lema "everything is a relation". 'Model checking' usando a ferramenta Alloy. Demonstração de corrrecção usando álgebra relacional. Noção formal de contrato. Pré-condições mais fracas. Lógica de Hoare em formato relacional.
Duas provas de avaliação (mini-teste + teste) e exame de recurso. Avaliação contínua com base em problemas dados nas aulas TP. As provas escritas são de consulta de material impresso, apenas.
Slides das aulas teóricas:
Enunciados: