| Métodos Formais de Programação I - 2002/03 |
|---|---|
| [ DI/UM ] |
| Aula Teórica de 02.09.26 [Ref:1]: |
Sumário: Apresentação da disciplina. Equipa docente. Programa da disciplina e seu enquadramento no plano de estudos. Regime de avaliação. Informação electrónica sobre a disciplina: URL: http://www.di.uminho.pt/~jno/html/mi.html. Bibliografia.
| Aula Teórica de 02.09.26 [Ref:2]: |
Sumário: Introdução à especificação formal como método de controlo de qualidade em `software' . Motivação: especificação formal -- porquê e para quê? Introdução ao binómio especificação /implementação. Antevisão do programa da disciplina:
(a) Adopção do `standard' ISO/IEC 13817-1 (VDM-SL);
(b) Propriedades, invariantes e obrigações de prova ;
(c) Tipos colectivos de dados
| Aula Prática de 02.09.26 [Ref:3]: |
Sumário: Inscrições.
| Aula Prática de 02.09.26 [Ref:4]: |
Sumário: Inscrições.
Aula Teórica de 02.10.03 [Ref:1]:
Sumário: Ciclo de vida do desenvolvimento formal de `software' . Especificação formal construtiva. Modelação de um problema. Prototipagem e animação. Validação por teste. Importância da verificação formal das propriedades de um modelo. Técnicas de prova.
| Aula Teórica de 02.10.03 [Ref:2]: |
Sumário: Introdução aos tipos colectivos de dados. Tipos não indutivos. Invertibilidade à esquerda e à direita. Inequações T <= F T e tipos quasi-indutivos. Conjuntos: introdução ao tipo quasi-indutivo PA (set of A em VDM-SL). [Ol00, pp.79-81] Parcialidade e não-determinismo e parcialidade: relações versus funções.
| Aula Prática de 02.10.03 [Ref:3]: |
Sumário: Introdução às VDMTOOLS®. Exemplo de utilização: modelação de um sensor de temperatura.
Aula Laboratorial: Ficha 1 (especificação vs implementação de funções)
| Aula Prática de 02.10.04 [Ref:4]: |
Sumário: Introdução às VDMTOOLS®. Exemplo de utilização: modelação de um sensor de temperatura.
Aula Laboratorial: Ficha 1 (especificação vs implementação de funções)
| Aula Teórica de 02.10.10 [Ref:1]: |
Sumário: Operações sobre o tipo set of A. Definição do morfismo (partes finitas de) como um hilomorfismo. Compreensão de conjuntos.
| Aula Teórica de 02.10.10 [Ref:2]: |
Sumário: Introdução à especificação formal por pares pré/pós-condições. Necessidade de estender funções a relações: não-determinismo e parcialidade. Sub-especificação.
| Aula Prática de 02.10.10 [Ref:3]: |
Sumário: Aula Laboratorial: problema 2 (modelação com sequências); problema 3 (modelação com conjuntos).
| Aula Prática de 02.10.11 [Ref:4]: |
Sumário: Aula Laboratorial: problema 2 (modelação com sequências); problema 3 (modelação com conjuntos).
| Aula Teórica de 02.10.17 [Ref:1]: |
Sumário: Não houve aula (dispensa de aulas devida aos festejos académicos).
| Aula Teórica de 02.10.17 [Ref:2]: |
Sumário: Não houve aula (dispensa de aulas devida aos festejos académicos).
| Aula Prática de 02.10.17 [Ref:3]: |
Sumário: Aula Laboratorial: Ficha 4 (invariantes); Ficha 5 (tipos indutivos).
| Aula Prática de 02.10.18 [Ref:4]: |
Sumário: Aula Laboratorial: Ficha 4 (invariantes); Ficha 5 (tipos indutivos).
| Aula Teórica de 02.10.24 [Ref:1]: |
Sumário: Introdução ao cálculo de relações. Inclusão de relações. Composição e intersecção de relações. Conversa de uma relação. Propriedades.
| Aula Teórica de 02.10.24 [Ref:2]: |
Sumário: Provas de igualdade relacional. Ordens e sua taxonomia. As ordens coreflexivas e a modelação de predicados.
| Aula Prática de 02.10.24 [Ref:3]: |
Sumário: Exercícios teorico-práticos.
| Aula Prática de 02.10.25 [Ref:4]: |
Sumário: Exercícios teorico-práticos.
| Aula Teórica de 02.10.31 [Ref:1]: |
Sumário: Os operadores ker e img. Sua utilização em especificação. Exemplo: isPermutation.
| Aula Teórica de 02.10.31 [Ref:2]: |
Sumário: Taxonomia de relações binárias. Relações inteiras (totais), sobrejectivas e simples (funcionais) Significado de uma especificação constituída por pares-pre/post.
| Aula Prática de 02.10.31 [Ref:3]: |
Sumário: Exercícios teorico-práticos.
| Aula Prática de 02.11.01 [Ref:4]: |
Sumário: Não houve aula (feriado).
| Aula Teórica de 02.11.07 [Ref:1]: |
Sumário: As relações finitas como estruturas de dados: set of (A * B). Notação e operadores. Notação em compreensão. Relações binárias finitas com uma dependência funcional.
| Aula Teórica de 02.11.07 [Ref:2]: |
Sumário: O tipo de dados função parcial finita map A to B e seus operadores básicos. Notação em compreensão.
| Aula Prática de 02.11.07 [Ref:3]: |
Sumário: Exercícios teorico-práticos.
| Aula Prática de 02.11.07 [Ref:4]: |
Sumário: Exercícios teorico-práticos.
| Aula Teórica de 02.11.14 [Ref:1]: |
Sumário: Conclusão da aula anterior.
| Aula Teórica de 02.11.14 [Ref:2]: |
Sumário: Diagramas ERA (`Entity-Relationship-Attribute') e sua conversão para modelos formais de dados baseados em funções parciais finitas e respectivos invariantes ([Ol95d], pág. 328).
| Aula Prática de 02.11.14 [Ref:3]: |
Sumário: Exercícios teorico-práticos.
| Aula Prática de 02.11.14 [Ref:4]: |
Sumário: Exercícios teorico-práticos.
| Aula Teórica de 02.11.21 [Ref:1]: |
Sumário: Conclusão da aula anterior.
| Aula Teórica de 02.11.21 [Ref:2]: |
Sumário: Início do estudo de formalização dos morfismos associados aos tipos quasi-indutivos PA e (set of A em VDM-SL).
| Aula Prática de 02.11.21 [Ref:3]: |
Sumário: Exercícios teorico-práticos.
| Aula Prática de 02.11.21 [Ref:4]: |
Sumário: Exercícios teorico-práticos.
| Aula Teórica de 02.11.28 [Ref:1]: |
Sumário: Noção de hilomorfismo relacional. Relacionadores versus functores. Factorização de um hilomorfismo relacional através do tipo indutivo associado (ponto-fixo do respectivo relacionador de base).
| Aula Teórica de 02.11.28 [Ref:2]: |
Sumário: Introdução ao cálculo de pontos-fixos : Funções monótonas, pré/pós-pontos-fixos. Teorema de Tarski. Notação µ.
| Aula Prática de 02.11.28 [Ref:3]: |
Sumário: Exercícios teorico-práticos.
| Aula Prática de 02.11.28 [Ref:4]: |
Sumário: Exercícios teorico-práticos.
| Aula Teórica de 02.12.05 [Ref:1]: |
Sumário: Cálculo de pontos-fixos : Aplicação à definição indutiva de um tipos de dados com ponto fixo µF de um functor polinomial F. Unicidade do catamorfismo associado.
| Aula Teórica de 02.12.05 [Ref:2]: |
Sumário: Hilomorfismos como pontos fixos de equações relacionais. Teorema da factorização-hilo. Aplicação aos morfismos de conjuntos e funções finitas. Terminação versus indução. Ordens bem-fundadas.
| Aula Prática de 02.12.05 [Ref:3]: |
Sumário: Exercícios teorico-práticos.
| Aula Prática de 02.12.05 [Ref:4]: |
Sumário: Exercícios teorico-práticos.
| Aula Teórica de 02.12.12 [Ref:1]: |
Sumário: Cálculo de catamorfismos : Propriedades de reflexão-cata e fusão-cata e sua utilidade na prova construtiva de propriedades. Exemplo: verificação da propriedade involutiva da inversão de listas finitas, invl ·invl = id . Propriedade de absorção-cata. Exemplo: prova da igualdade length = sum ·(1)*.
| Aula Teórica de 02.12.12 [Ref:2]: |
Sumário: Hilomorfismos como pontos fixos de equações relacionais. Teorema da factorização-hilo. Aplicação aos morfismos de conjuntos e funções finitas. Terminação versus indução.
| Aula Prática de 02.12.12 [Ref:3]: |
Sumário: Exercícios teorico-práticos.
| Aula Prática de 02.12.05 [Ref:4]: |
Sumário: Exercícios teorico-práticos.
| Aula Teórica de 02.12.12 [Ref:1]: |
Sumário: Esquemas recursivos Introdução às definições mutuamente recursivas. Sistemas de definições mutuamente recursivas e sua solução como um catamorfismo. Derivação da lei da recursividade mútua (ou de Fokkinga). Preenchimento do questionário de avaliação.
| Aula Teórica de 02.12.19 [Ref:2]: |
Sumário: Noção de paramorfismo e suas propriedades. Exemplos. Síntese final. Encerramento da disciplina.
| Aula Prática de 02.12.19 [Ref:3]: |
Sumário: Exercícios teorico-práticos.
| Aula Prática de 02.12.19 [Ref:4]: |
Sumário: Exercícios teorico-práticos.