UC2 - Cálculo de Sistemas de Informação
E-Learning
Docente / Horário
Alunos
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 |
Programa resumido
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.
Regime de avaliação
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.
Material disponível ou a disponibilizar
Slides das aulas teóricas:
Enunciados:
- Enunciado do mini-teste de 7 de Dezembro (com proposta de resolução).
- Enunciado do teste de 4 de Janeiro (com proposta de resolução).
Bibliografia adicional
- C.B. Jones. Systematic Software Development Using VDM. Series in Computer Science. Prentice-Hall International, 1986 (first edition). (345 pages)