Métodos Formais de Programação II - 2000/01
[ DI/UM ]

Sumários - 2000/2001

J.N. Oliveira 406006

  Aula Prática de 2001.02.12 [Ref:1]:

Sumário: Revisão de M.F.P.-I: Métodos indutivos de prova. Indução natural ( Nat0 =1 + Nat0) e indução sobre sequências (A* =1 + A × A*). Resolução dos exercícios 3.3, 3.4 e 3.5.

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

Sumário: Apresentação da disciplina. Equipa docente. Programa da disciplina e seu enquadramento no plano de estudos. Regime de avaliação. Bibliografia.

Informação electrónica sobre a disciplina: www.di.uminho.pt/~jno/html/mii.html.

Introdução às técnicas de refinamento (reificação) de especificações formais. Antecendentes históricos.

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

Sumário: Métodos indutivos de prova. Indução natural ( Nat0 =1 + Nat0) e indução sobre sequências (A* =1 + A × A*). Resolução dos exercícios 3.3, 3.4 e 3.5.

  Aula Prática de 2001.02.19 [Ref:1]:

Sumário: Resolução dos exercícios 3.3, 3.4 e 3.5 (cont.). Métodos indutivos de prova. Indução sobre conjuntos (PA <=1 + A × PA). Resolução de exercícios.

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

Sumário: Introdução às técnicas de refinamento (cont.) : Validação vs verificação formal. Verificação estática vs dinâmica. Semântica denotacional de linguagens de programação. O porquê da programação estruturada. Verificação vs cálculo de programas.

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

Sumário: Resolução dos exercícios 3.3, 3.4 e 3.5 (cont.). Métodos indutivos de prova. Indução sobre conjuntos (PA <=1 + A × PA). Resolução de exercícios.

  Aula Prática de 2001.02.26 [Ref:1]:

Sumário: Relações binárias e funções finitas. Resolução de exercícios: definição das funções dom, rng, A -> f, |s, , pap e ++ sob a forma de morfismos sobre A -> B. Resolução dos exercícios 3.7 e 3.8.

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

Sumário: Introdução às técnicas de refinamento (cont.) : Especificação directa e reversa. Compreensão de programas. Exemplo de análise de um programa em C++ e conjectura da sua especificação formal recorrendo a catamorfismos.

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

Sumário: Relações binárias e funções finitas. Resolução de exercícios: definição das funções dom, rng, A -> f, |s, , pap e ++ sob a forma de morfismos sobre A -> B. Resolução dos exercícios 3.7 e 3.8.

  Aula Prática de 2001.03.05 [Ref:1]:

Sumário: Combinação de funções mutuamente dependentes. A lei de Fokkinga. A lei de Banana-Split. Resolução de exercícios.

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

Sumário: Técnicas de refinamento algorítmico : Leis de fusão «horizontal» de processos algorítmicos. Lei da recursividade mútua de Fokkinga. Lei de «banana-split» e sua utilização na intercombinação de ciclos. Eliminação de estruturas de dados intermédias («desflorestação»).

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

Sumário: Combinação de funções mutuamente dependentes. A lei de Fokkinga. A lei de Banana-Split. Resolução de exercícios.

  Aula Prática de 2001.03.12 [Ref:1]:

Sumário: Não houve aula (participação do docente em congresso internacional).

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

Sumário: Não houve aula (participação do docente em congresso internacional).

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

Sumário: Não houve aula (participação do docente em congresso internacional).

  Aula Prática de 2001.03.19 [Ref:1]:

Sumário: Aula laboratorial. Definição das funções dom, rng, A -> f, |s, , pap e ++, escritas sob a forma de morfismos sobre A -> B, em VDM-SL.

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

Sumário: Técnicas de refinamento algorítmico : Leis de fusão «vertical» de processos algorítmicos (leis functoriais, de fusão e de absorção).

Introdução às técnicas de refinamento dos dados : Transformações isomorfas. Transformações sobrejectivas e injectivas. Invertibilidade à direita e à esquerda. Noções de abstracção e de representação. Inequações da forma A <=B . Exemplos. Diagramas de refinamento de operações. Abstração dos argumentos e representação dos resultados. Esquema de síntese de uma implementação como solução de um diagrama de refinamento.

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

Sumário: Aula laboratorial. Definição das funções dom, rng, A -> f, |s, , pap e ++, escritas sob a forma de morfismos sobre A -> B, em VDM-SL.

  Aula Prática de 2001.03.26 [Ref:1]:

Sumário: Aula laboratorial. Definição, em VDM-SL, de funções paramétricas que permitem realizar catamorfismos e anamorfismos sobre A*.

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

Sumário: Refinamento formal de dados : Propriedades da relação A <=B: reflexividade, transitividade e monotonicidade.

Leis de representação (ou de refinamento) envolvendo tipos de dados quasi-indutivos (PA e A -> B):

PA =A -> 1
0 -> A =1
1 -> A =1 + A
(C+B) -> A =(C -> A) × (B -> A)

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

Sumário: Aula laboratorial. Definição, em VDM-SL, de funções paramétricas que permitem realizar catamorfismos e anamorfismos sobre A*.

  Aula Prática de 2001.04.02 [Ref:1]:

Sumário: Cálculo de simulações. Resolução de exercícios: simulação de ina e de card. Refinamento algorítmico. Algoritmos de pesquisa e sua eficiência. Padrões de recursividade lineares vs bi-lineares. Resolução de exercícios: alteração do padrão de recursividade da função belongsa.

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

Sumário: Refinamento formal de dados (cont.) : Repertório de leis e suas funções de abstracção e de representação.

A -> B × C <=(A -> B) × (A -> C)
A -> D × (B -> C) <= (A -> D) × ((A × B) -> C)

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

Sumário: Cálculo de simulações. Resolução de exercícios: simulação de ina e de card. Refinamento algorítmico. Algoritmos de pesquisa e sua eficiência. Padrões de recursividade lineares vs bi-lineares. Resolução de exercícios: alteração do padrão de recursividade da função belongsa.

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

Sumário: Refinamento formal de dados (cont.) : Invariantes («concretos») induzidos por representação. Exemplos. Cálculo de invariantes concretos.

Modelação formal versus modelação em sistemas de informação de base relacional. Semântica formal de diagramas E-R (entidade relação) e seus invariantes.

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

Sumário: Representação de dados e refinamento. Invertibilidade à direita e à esquerda. O cálculo de isomorfismo. Resolução de exercícios: definição de funções de abstracção e suas inversas. Invertibilidade apenas à direita. O cálculo inequacional. Resolução de exercícios. Definição de funções de abstracção e de representação.

  Aula Prática de 2001.04.23 [Ref:1]:

Sumário: Representação de dados e refinamento. Invertibilidade à direita e à esquerda. O cálculo de isomorfismo. Resolução de exercícios: definição de funções de abstracção e suas inversas. Invertibilidade apenas à direita. O cálculo inequacional. Resolução de exercícios. Definição de funções de abstracção e de representação.

  Aula Prática de 2001.04.30 [Ref:1]:

Sumário: O cálculo inequacional (cont.). Introdução à reengenharia formal de bases de dados relacionais. Resolução dos exercícios 4.1, 4.2, 4.3 e 4.4.

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

Sumário: Semântica formal de diagramas E-R (conclusão) : Exemplo - o problema PPD (árvores de produção e planeamento da produção).

Lei do refinamento estrutural de tipos indutivos. Exemplo: relações de refinamento entre listas (morfismos blast e embed).

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

Sumário: O cálculo inequacional (cont.). Introdução à reengenharia formal de bases de dados relacionais. Resolução dos exercícios 4.1, 4.2, 4.3 e 4.4.

  Aula Prática de 2001.05.07 [Ref:1]:

Sumário: Apresentação da ferramenta de inversão formal de bases de dados K-RF. Animação do cálculo de refinamento aplicado à engenharia reversa de bases de dados.

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

Sumário: Refinamento estrutural de tipos indutivos (conclusão) : Prova por cálculo de morfismos. Mais exemplos: síntese da implementação de GenDia à custa de DecTree.

Representação de tipos indutivos polinomais:

• Representação gramatical (BNF).
• Introdução de apontadores em linguagens tipo C/C++.
• Desrecursivação orientada a linguagens tipo SQL. Teorema de desrecursivação genérica. Exemplo: síntese da implementação de DecTree em SQL.

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

Sumário: Apresentação da ferramenta de inversão formal de bases de dados K-RF. Animação do cálculo de refinamento aplicado à engenharia reversa de bases de dados. Apresentação da ferramenta de auditoria à qualidade dos dados KARMA. Validação de invariantes em processos de limpeza de dados.

  Aula Prática de 2001.05.14 [Ref:1]:

Sumário: Apresentação da ferramenta de auditoria à qualidade dos dados KARMA. Validação de invariantes em processos de limpeza de dados.

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

Sumário: Não houve aula (tolerância do Enterro da Gata).

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

Sumário: Não houve aula (tolerância do Enterro da Gata).

  Aula Prática de 2001.05.21 [Ref:1]:

Sumário: Propriedades básicas do cálculo inequacional: reflexividade, transitividade e monotonicidade. Resolução dos exercícios 4.6 (1) e 4.6 (2). Reificação para modelo relacional do modelo PPD (árvores de produção e planeamento da produção).

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

Sumário: Refinamento algorítmico (conclusão) : Lei da introdução de parâmetros de acumulação. Desrecursivação algorímica: cálculo de ciclos for/while.

Exemplo de utilização em engenharia reversa: análise do programa em C wc.

Avaliação da disciplina.

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

Sumário: Propriedades básicas do cálculo inequacional: reflexividade, transitividade e monotonicidade. Resolução dos exercícios 4.6 (1) e 4.6 (2). Reificação para modelo relacional do modelo PPD (árvores de produção e planeamento da produção).

  Aula Teórica (Suplementar) de 2001.06.04:

Sumário: Aula de dúvidas e preparação para o exame.

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