Métodos Formais de Programação I - 2001/02
[ DI/UM ]

Sumários - 2001/2002

J.N. Oliveira 406006

  Aula Teórica de 01.10.04 [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 01.10.04 [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. Ciclo de vida do desenvolvimento formal de `software' .

Antevisão do programa da disciplina:
(a) Adopção do `standard' ISO/IEC 13817-1 (VDM-SL);
(b) Invariantes, obrigações de prova e métodos indutivos;
(c) Tipos colectivos de dados «quasi indutivos»: conjuntos e funções finitas.

  Aula Prática de 01.10.04 [Ref:3]:

Sumário: Inscrições.

  Aula Teórica de 01.10.11 [Ref:1]:

Sumário: 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 01.10.11 [Ref:2]:

Sumário: Tipos indutivos e seus morfismos (revisão de MP-I). Propriedades básicas de catamorfismos e sua aplicação na verificação construtiva (dedutiva) de propriedades de um modelo.

Exemplo: verificação dedutiva da propriedade involutiva da inversão de listas finitas: invl ·invl = id . Papel das propriedades de reflexão-cata e fusão-cata.

  Aula Prática de 01.10.11 [Ref:3]:

Sumário: Revisões de Métodos de Programação I. Exercícios sobre fusão-cata.

  Aula Prática de 01.10.12 [Ref:4]:

Sumário: Revisões de Métodos de Programação I. Exercícios sobre fusão-cata.

  Aula Teórica de 01.10.18 [Ref:1]:

Sumário: Propriedade de absorção-cata. Exemplos: prova da igualdade length = sum ·(1)*. Definição de filter p.

  Aula Teórica de 01.10.18 [Ref:2]:

Sumário: 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).

  Aula Prática de 01.10.18 [Ref:3]:

Sumário: Introdução às VDMTOOLS®. Exemplo de utilização: modelação de um sensor de temperatura.

  Aula Prática de 01.10.19 [Ref:4]:

Sumário: Introdução às VDMTOOLS®. Exemplo de utilização: modelação de um sensor de temperatura.

  Aula Teórica de 01.10.25 [Ref:1]:

Sumário: Introdução ao conceito de paramorfismo. Exemplos: factorial e `word count'.

  Aula Teórica de 01.10.25 [Ref:2]:

Sumário: Propriedades dos paramorfismos. Conversão entre paramorfismos e catamorfismos.

  Aula Prática de 01.10.25 [Ref:3]:

Sumário: Aula Laboratorial: Ficha 1 (especificação vs implementação de funções)

  Aula Prática de 01.10.26 [Ref:4]:

Sumário: Aula Laboratorial: Ficha 1 (especificação vs implementação de funções)

  Aula Teórica de 01.11.08 [Ref:1]:

Sumário: Introdução aos tipos não indutivos. Invertibilidade à esquerda e à direita. Inequações T <= F T e tipos quasi-indutivos. O tipo quasi-indutivo PA (set of A em VDM-SL) e respectivo morfismo (partes finitas de).

  Aula Teórica de 01.11.08 [Ref:2]:

Sumário: Propriedades do morfismo partes de. O functor Pf. Extensão, compreensão e filtragem. Notação-ZF. O tipo PA (set of A em VDM-SL)) e esboço de um seu morfismo (card ).

  Aula Prática de 01.11.08 [Ref:3]:

Sumário: Não houve aula (ausência do docente no estrangeiro).

  Aula Prática de 01.11.09 [Ref:4]:

Sumário: Não houve aula (ausência do docente no estrangeiro).

  Aula Teórica de 01.11.15 [Ref:1]:

Sumário: O tipo quasi-indutivo função finita A -> B (map A to B em VDM-SL) e seus operadores.

  Aula Teórica de 01.11.15 [Ref:2]:

Sumário: O tipo quasi-indutivo A -> B: operadores e propriedades. Relação entre A -> B e A^B: o isomorfismo A -> B =(B+1)^A.

  Aula Prática de 01.11.15 [Ref:3]:

Sumário: Exercícios de aplicação da lei da absorpção-cata. Lei de Fokkinga: casos particulares (funções "aninhadas", "banana-split"), derivação e aplicações.

  Aula Prática de 01.11.16 [Ref:4]:

Sumário: Exercícios de aplicação da lei da absorpção-cata. Lei de Fokkinga: casos particulares (funções "aninhadas", "banana-split"), derivação e aplicações.

  Aula Teórica de 01.11.22 [Ref:1]:

Sumário: Teoria de prova associada a um tipo quasi-indutivo. Essência da prova indutiva. Terminação versus indução. Ordens bem-fundadas.

  Aula Teórica de 01.11.22 [Ref:2]:

Sumário: Teoria de prova associada a um tipo quasi-indutivo (cont.) : Método de indução estrutural. Instâncias do método de indução estrutural - PA, A* e A -> B.

  Aula Prática de 01.11.22 [Ref:3]:

Sumário: Aula Laboratorial: Fichas 2 e 3 (modelação com conjuntos; invariantes; uso de invariantes em VDM-SL)

  Aula Prática de 01.11.23 [Ref:4]:

Sumário: Aula Laboratorial: Fichas 2 e 3 (modelação com conjuntos; invariantes; uso de invariantes em VDM-SL)

  Aula Teórica de 01.11.29 [Ref:1]:

Sumário: Teoria de prova associada a um tipo quasi-indutivo (conclusão) : Noções de coálgebra bem-fundada. Ordem bem-fundada definida por uma coálgebra bem-fundada. Método de indução polinomial.

  Aula Teórica de 01.11.29 [Ref:2]:

Sumário: Indução e ponto-fixo. Introdução ao cálculo de pontos-fixos.

  Aula Prática de 01.11.29 [Ref:3]:

Sumário: Aula Laboratorial: Fichas 4 e 5 (modelação com tipos indutivos e com correspondências)

  Aula Prática de 01.11.30 [Ref:4]:

Sumário: Aula Laboratorial: Fichas 4 e 5 (modelação com tipos indutivos e com correspondências)

  Aula Teórica de 01.12.06 [Ref:1]:

Sumário: Introdução ao cálculo de pontos-fixos (cont.) : Funções monótonas, pré/pós-pontos-fixos. Teorema de Tarski.

  Aula Teórica de 01.12.06 [Ref:2]:

Sumário: Introdução ao cálculo de pontos-fixos (conclusão) : leis de cálculo, `rolling rule', regra do quadrado, monotonia e regra de indução. Aplicações ao raciocínio sobre tipos indutivos de dados.

  Aula Prática de 01.12.06 [Ref:3]:

Sumário: Exercícios sobre tipos quasi-indutivos. Derivação dos esquemas de indução associados a diversos tipos indutivos (incluindo o tipo Space discutido na Ficha 4), conjuntos e correspondências.

  Aula Prática de 01.12.07 [Ref:4]:

Sumário: Exercícios sobre tipos quasi-indutivos. Derivação dos esquemas de indução associados a diversos tipos indutivos (incluindo o tipo Space discutido na Ficha 4), conjuntos e correspondências.

  Aula Teórica de 01.12.13 [Ref:1]:

Sumário: Aplicações de especificação formal: Esquemas de conversão de Diagramas ERA (`Entity-Relationship-Attribute') para modelos formais de dados e respectivos invariantes ([Ol95d], pág. 328).

  Aula Teórica de 01.12.13 [Ref:2]:

Sumário: Aplicações da especificação formal (cont.) : Base de dados de produção -- um exemplo de conversão de um diagrama ERA e sua transformação num modelo estruturado de dados.

  Aula Prática de 01.12.13 [Ref:3]:

Sumário: Aula Laboratorial: Fichas 6 e 7 (modelação com correspondências: multiconjuntos e tabelas de hash).

  Aula Prática de 01.12.14 [Ref:4]:

Sumário: Aula Laboratorial: Fichas 6 e 7 (modelação com correspondências: multiconjuntos e tabelas de hash).

  Aula Teórica de 01.12.20 [Ref:1]:

Sumário: Aplicações da especificação formal (cont.) : Esboço de uma semântica formal para a linguagem SQL/DDL, expressa em VDM-SL.

  Aula Teórica de 01.12.20 [Ref:2]:

Sumário: Aplicações da especificação formal (conclusão) : Conversão de gramáticas independentes de contexto (notação BNF) em sistemas de definições de tipos indutivos e quasi-indutivos ([Ol95d], pág. 104). Regras para a exportação de dados em formato XML.

Encerramento da disciplina. Preenchimento do questionário de avaliação.

  Aula Prática de 01.12.20 [Ref:3]:

Sumário: Conclusão da Ficha 7. Codificação de funcionais paramétricos em VDM-SL.

  Aula Prática de 01.12.21 [Ref:4]:

Sumário: Conclusão da Ficha 7. Codificação de funcionais paramétricos em VDM-SL.

Voltar à página principal de MFP-I. Outras disciplinas leccionadas pelo DIUM