| Métodos Formais de Programação II - 1998/99 |
|---|---|
| [ DI/UM ] |
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/MII.HTML. Bibliografia.
Sumário: Correcção do exame de 2.ª-chamada da disciplina Métodos Formais de Programação I .
Sumário: Tipos de dados com invariantes. Preservação de invariantes. Tipos indutivos. Métodos indutivos de prova.
Sumário: Invariantes: formulação e prova de preservação por uma operação. Exemplo 2.4.1. Exercícios: 2.26, 2.28, 2.32. Formulação do predicado BiSexuado como um catamorfismo sobre o modelo AG para árvores geneológicas.
Sumário: Teoria da Reificação de Dados. Introdução ao cálculo de estruturas de dados. Noção de equivalência entre estruturas de dados e sua correspondência com a noção matemática de isomorfismo. Principais isomorfismos naturais envolvendo produtos e coprodutos.
Sumário: Exercícios sobre indução: 2.53, 2.54, 2.55, 7.1 e 7.3.
Sumário: Não houve aula (ausência do docente em congresso internacional).
Sumário: Apresentação e discussão da especificação do Bams e sua animação em CAMILA. Breve introdução ao sistema CAMILA. Exercício: 1.34.
Sumário: Teoria da Reificação de Dados (cont.): Subcálculo de isomorfismos (conclusão): isomorfismos naturais sobre exponenciações. Considerações sobre o isomorfismo A-> B =(B+1)^A.Epimorfismo matemático e sua correspondência com as noções de redundância e de ordenação de modelos de dados. Noção de invariante de abstracção. Definição da ordem de redundância A <= B entre dois modelos de dados A e B.
Sumário: Formulação e verificação de isomorfismos básicos em SETS . Prova da naturalidade de assocr e undistr . Exercícios: 8.5, 1.20 e 2.57.
Sumário: Teoria da Reificação de Dados (cont.): O subcálculo de epimorfismo: factos resultantes da generalização das leis da exponenciação a funções parciais finitas.
Sumário: Estudo detalhado da factorização de relações. Implementação de A* sobre listas recursivas.
Sumário: Teoria da Reificação de Dados (cont.): Epimorfismos célebres envolvendo funções finitas e sequências finitas.
Sumário: Não houve aula (participação (autorizada) do docente em congresso internacional).
Sumário: Teoria da Reificação de Dados (conclusão): Introduçao de invariantes no refinamento. Sua utilidade para recuperar a propriedade iso . Redefinição da ordem de redundância: invariantes de abstracção. Propriedades: reflexividade, transitividade e antissimetria (a menos de um iso). Teorema do cálculo estrutural.Aplicações da Reificação de Dados: Reificação sobre o modelo relacional da informação como generalização da teoria clássica da normalização da informação . Cálculo estrutural de esquemas de bases de dados na 3FN.
Sumário: Estudo detalhado do refinamento do exemplo Bams . Animação em CAMILA do processo de refinamento (protótipo bams.cam). Exercícios: 8.10 e 8.11.
Sumário: Aplicações da Reificação de Dados (conclusão): Conversão de diagramas Entidade-Relação em modelos matemáticos de dados e vice-versa (quando possível).
Sumário: Não houve aula (por motivo de doença).
Sumário: Implementação de Tipos de Dados Indutivos: Conversão de gramáticas independentes de contexto em equações polinomiais. Representação gramatical de tipos indutivos. Noção de linguagem orientada ao domínio ('domain specific language').Implementação Não-recursiva de Tipos de Dados Indutivos: Introdução à desrecursivação dos dados. Teoremas de desrecursivação genérica. Exemplo de aplicação: GenDia.
Sumário: Exercícios: 8.30, 2.56 e 2.64 (incompleto). Exercícios adicionais: notas 23 e 25 (curso de San Luis).
Sumário: Tolerância de Ponto: Enterro da Gata .
Sumário: Tolerância de Ponto: Enterro da Gata .
Sumário: Implementação Não-recursiva de Tipos de Dados Indutivos (conclusão): Exemplos de aplicação: DecTree em GenDia .Apresentação do Eng. Luís Gama, da Novabase , sobre técnicas e sistemas de OLAP (assunto do trabalho laboratorial da disciplina).
Sumário: (por integrar)
Sumário: Reificação das Operações : Síntese de programas (simulações, ou implementações) como soluções de diagramas de refinamento . Exemplo: cálculo de operações functoriais associadas às funções de abstracção (transformações naturais).Cálculo de programas por transformação recorrendo ao método FOLD/UNFOLD . Exemplo: cálculo da operação de pertença em conjuntos representados por listas.
Sumário: Reificação das Operações (cont.): Solução de diagramas de refinamento com base em cálculo de catamorfismos e da exponenciação. Exemplo: operação de pertença em conjuntos.
Sumário: Reificação das Operações (cont.): Técnicas de optimização algorítmica: Lei da recursividade mútua de Fokkinga. Lei de «banana-split» e sua utilização na intercombinação de ciclos.Avaliação da disciplina.
Sumário: (por integrar)
Sumário: Reificação das Operações (conclusão): Reduções monodais e cálculo dos correspondentes ciclos for/while. 'Browsing' de listas e conjuntos. Cálculo de operações de manipulação de bases de dados e sua concretização em SQL . Considerações finais.