| Métodos Formais de Programação II - 2001/02 |
|---|---|
| [ DI/UM ] |
| Aula Prática de 2002.02.25 [Ref:1]: |
Sumário: Aula laboratorial (exercício 8)
| Aula Teórica de 2002.02.27 [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.
| Aula Prática de 2002.02.27 [Ref:3]: |
Sumário: Aula laboratorial (exercício 8)
Aula Prática de 2002.03.4 [Ref:1]:
Sumário: Aula laboratorial (exercício 9)
| Aula Teórica de 2002.03.6 [Ref:2]: |
Sumário: Não houve aula (A compensar).
| Aula Prática de 2002.03.6 [Ref:3]: |
Sumário: Aula laboratorial (exercício 9)
Aula Prática de 2002.03.11 [Ref:1]:
Sumário: Aula laboratorial (exercício 10)
| Aula Teórica de 2002.02.13 [Ref:2]: |
Sumário: Noção de modelo e de modelação formal. «Dimensões» de um modelo: sintaxe e semântica. Modelos «são» álgebras.
Introdução aos tipos algébricos de dados : noção de assinatura algébrica. Espécies e operadores. Assinaturas homogéneas/ heterogéneas. APIs (`Application Program Interfaces'). Visão gramatical. `Domain specific languages'. Conversão de gramáticas independentes de contexto em assinaturas heterogéneas. Noção de termo sintático. Termos versus árvores sintáticas abstractas. [Ol95d, pp.1-18]
| Aula Prática de 2002.03.13 [Ref:3]: |
Sumário: Aula laboratorial (exercício 10)
Aula Prática de 2002.03.18 [Ref:1]:
Sumário: Assinaturas e modelos. Análise do problema de escalonamento de peritos.
| Aula Teórica de 2002.03.20 [Ref:2]: |
Sumário: Introdução aos tipos algébricos de dados (conclusão) : Modelos de uma assinatura (álgebras). Recticulado de todos os modelos de uma assinatura. Modelo inicial e modelo terminal. [Ol95d, pp.33-38]
Introdução ao refinamento (implementação) de modelos algébricos : Refinamento de espécies de dados. Inequações da forma A <=B . Funções de abstracção e de representação. Invertibilidade à direita e à esquerda. Caso particular: isomorfismos de modelos de dados. [Ol00b, pp.95-97]
Diagramas de refinamento de operadores. Caso particular: transformações naturais como refinamento de operadores functoriais. Exemplo: f* implementa Pf. [Ol00c, pp.119-121]
| Aula Prática de 2002.03.20 [Ref:3]: |
Sumário: Assinaturas e modelos. Análise do problema de escalonamento de peritos.
Aula Teórica de 2002.04.03 [Ref:2]:
Sumário: Refinamento formal de dados : leis de isomorfismo envolvendo tipos de dados quasi-indutivos (PA e A -> B):
A -> B = (B + 1)^A PA = A -> 1 0 -> A = 1 1 -> A = 1 + A (C+B) -> A = (C -> A) × (B -> A)
Introdução ao repertório de inequações de refinamento e respectivas funções de abstracção e de representação:
(C × A) -> B <= C -> (A -> B) A -> (B × C) <= (A -> B) × (A -> C)
[Ol00b, pp.98-100]
| Aula Prática de 2002.04.03 [Ref:3]: |
Sumário: Refinamento: alguns exemplos. Refinamento de conjuntos em sequências e tabelas de hashing.
Aula Prática de 2002.04.08 [Ref:1]:
Sumário: Refinamento: alguns exemplos. Refinamento de conjuntos em sequências e tabelas de hashing.
| Aula Teórica de 2002.04.10 [Ref:2]: |
Sumário: Refinamento formal de dados (cont.) : Continuação do estudo das principais inequações de refinamento e respectivas 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) PA <= A -> B PA <= Nat-> A A* <= Nat-> A A -> B <= B -> PA
[Ol00b, pp.100-101]
| Aula Prática de 2002.04.10 [Ref:3]: |
Sumário: Invariantes e suas provas. Provas por indução. Exemplos: naturais e listas. [Ol00a, pp.84-88]
Aula Prática de 2002.04.15 [Ref:1]:
Sumário: Invariantes e suas provas. Provas por indução. Exemplos: naturais e listas. [Ol00a, pp.84-88]
Aula Teórica de 2002.04.17 [Ref:2]:
Sumário: Refinamento formal de dados (cont.) : Propriedades da relação A <=B: reflexividade, transitividade e monotonia. Cálculo estrutural. [Ol00b, pp.102-103] Área de aplicação: cálculo de refinamento para o modelo relacional da informação. [Ol00b, pp.109] Exemplo: cálculo da implementação relacional do moldelo de dados BAMS. Síntese da função de abstracção global. [Ol95d, pp.297-298]
Lei do refinamento estrutural de tipos indutivos. Exemplos: relações de refinamento entre listas (morfismos blast e embed); síntese da implementação de GenDia à custa de DecTree. [Ol00b, pp.104-106]
| Aula Prática de 2002.04.17 [Ref:3]: |
Sumário: Inferência das funções de abstracção/representação das principais inequações de refinamento estudadas nas aulas teóricas.
Aula Prática de 2002.04.22 [Ref:1]:
Sumário: Inferência das funções de abstracção/representação das principais inequações de refinamento estudadas nas aulas teóricas.
| Aula Teórica de 2002.04.24 [Ref:2]: |
Sumário: Refinamento formal de dados (cont.) : Prova construtiva da lei do refinamento estrutural de tipos indutivos. [Ol00b, pp.107]
Cálculo de invariantes concretos induzidos por representação. Exemplos. Regra da síntese de invariantes concretos. [Ol00b, pp.108-109]
Implementação de tipos indutivos polinomais: Representação gramatical (BNF). [Ol95d, pp.104-107] Introdução de apontadores em linguagens tipo C/C++. [Ol00b, pp.110-112]
| Aula Prática de 2002.04.24 [Ref:3]: |
Sumário: Estudo do refinamento relacional do modelo PPD.
Aula Prática de 2002.04.29 [Ref:1]:
Sumário: Estudo do refinamento relacional do modelo PPD.
Aula Prática de 2002.05.06 [Ref:1]:
Sumário: Estudo de um caso de aplicação de lei de refinamento estrutural: o modelo GenDia implementado por DecTree.
Aula Teórica de 2002.05.08 [Ref:2]:
Sumário: Refinamento formal de dados (conclusão) : Implementação de tipos indutivos polinomais: Teorema de desrecursivação genérica. Função de abstracção e de representação. Exemplo: síntese da implementação de DecTree em SQL. [Ol00b, pp.112-117]
Aula Prática de 2002.05.08 [Ref:3]:
Sumário: Estudo de um caso de aplicação de lei de refinamento estrutural: o modelo GenDia implementado por DecTree. [Ol00b, pp.105-106]
Aula Teórica (Suplementar) de 2002.05.08:
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). Resolução de diagramas de refinamento por fusão-cata. Exemplo: cálculo de belongs sobre listas. [Ol00c, pp.121-124]
Leis de fusão «horizontal» de processos algorítmicos: lei de Fokkinga e «banana-split' (revisão). [Ol00c, pp.132-136]
Aula Teórica de 2002.05.15 [Ref:2]:
Sumário: Não houve aula (tolerância do Enterro da Gata).
Aula Prática de 2002.05.20 [Ref:1]:
Sumário: Resolução do exercício 4.3 e 4.4. [Ol00b, p.101 e p.109] Exercício sobre implementação «universal» de produtos e coprodutos em estruturas de apontadores. Implementação em C/C++ do tipo indutivo LTree.
| Aula Teórica de 2002.05.22 [Ref:2]: |
Sumário: Técnicas de refinamento algorítmico (conclusão): refinamento por mudança da estrutura de dados virtual. Exemplo de aumento de polinomialidade: derivação de bbelongs. [Ol00c, pp.124-125] Lei da introdução de parâmetros de acumulação. Desrecursivação algorítmica: cálculo de ciclos for/while. [Ol00c, pp.125-131]
Avaliação da disciplina.
| Aula Prática de 2002.05.22 [Ref:3]: |
Sumário: Resolução do exercício 4.3 e 4.4. [Ol00b, p.101 e p.109] Exercício sobre implementação «universal» de produtos e coprodutos em estruturas de apontadores. Implementação em C/C++ do tipo indutivo LTree.
| Aula Prática (Suplementar) de 2002.05.27: |
Sumário: Técnicas de refinemento algorítmico. Resolução do exercício 5.1. [Ol00c, pp.136]
| Aula Prática (Suplementar) de 2002.05.27: |
Sumário: Técnicas de refinemento algorítmico. Resolução do exercício 5.1. [Ol00c, pp.136]
Voltar à página principal de MFP-II.
Outras disciplinas
leccionadas pelo DIUM