| Métodos Formais de Programação I - 1999/2000 |
|---|---|
| [ DI/UM ] |
| Aula Teórica de 00.02.23 [Ref:3]: |
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:
URL: HTTP://WWW.DI.UMINHO.PT/~JNO/HTML/MII.HTML .
| Aula Teórica de 00.03.01 [Ref:3]: |
Sumário: Antevisão do programa da disciplina: (a) Invariantes e métodos de prova indutiva (b) Tipos de dados "quasi indutivos": conjuntos e funções finitas. (c) Parcialidade, persistência, estado e comportamento reactivo. Operações. (d) Prototipagem e "embedding". Componentes reactivos e suas APIs. (e) Comparação de especificações e refinamento. (f) Cálculo de programas.Propriedades de um tipo de dados. Invariantes. Obrigações de prova inerentes à preservação de propriedades invariantes. "Normware". Exemplos: os tipos Ímpar e Data.
| Aula Teórica de 00.03.08 [Ref:3]: |
Sumário: Prova de propiedades invariantes num modelo. Métodos indutivos de prova. Método de indução associado a um tipo indutivo. Exemplos: o tipo X =1 + X e a indução natural. Indução sobre sequências finitas. Indução polinomial.
| Aula Teórica de 00.03.15 [Ref:3]: |
Sumário: Tipos de dados quasi-indutivos (coálgebra out é bem-fundada e inversa à direita de in). Exemplo: PA . Seus hilomorfismos.Essência da prova indutiva. Relações bem-fundadas (p.41, Ex 1.22). Coálgebras bem-fundadas e seus anamorfismos. Terminação versus indução.
| Aula Teórica de 00.03.22 [Ref:3]: |
Sumário: Tipos de dados quasi-indutivos (continuação): O invariante fdp sobre P(A×B) e o correspondente tipo "função finita A-> B . Seus hilomorfismos e método de prova indutiva.Introdução ao repertório de operadores sobre tipos quasi-indutivos. Principais operadores polimórficos e seus "teoremas grátis" (transformações naturais): elems , Pf, dom , ran , A-> f.
| Aula Teórica de 00.03.29 [Ref:3]: |
Sumário: Os tipos de dados quasi-indutivos PA e A-> B (conclusão) :
- 1.
- filtros e os operadores functoriais Pf e A-> f.
- 2.
- Alguns isomorfismos célebres como 2^A =PA , P(A×B) =(PB)^A , (B+1)^A =A-> B e o seu corolário 2^A =A-> 1.
- 3.
- Exemplo de modelação com funções finitas e conjuntos - o suporte de dados do modelo relacional da informação, em sintaxe CAMILA :
- (a)
- sem dependências funcionais:
Tuplo = Atributo -> Valor;
Tabela = Tuplo-set;
BD = Id -> Tabela;- (b)
- com dependências funcionais: basta redefinir
Tabela = Tuplo -> Tuplo;
| Aula Teórica de 00.04.05 [Ref:3]: |
Sumário: Especificação formal em grande escala. Das funções e assinaturas até às acções e as APIs. Parcialidade, persistência, estado interno e comportamento reactivo. Acções e sua decomposição funcional. Pré-condições. Prototipagem em CAMILA . Componentes e bibliotecas. Interfaces. Arquitectura a 3 níveis (dados, funções e "butões") e sua heterogeneidade tecnológica.
| Aula Teórica de 00.04.12 [Ref:3]: |
Sumário: Especificação formal em grande escala. continuação da aula anterior.
| Aula Teórica de 00.04.19 [Ref:3]: |
Sumário: Introdução ao processamento formal de 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.
| Aula Teórica de 00.05.03 [Ref:3]: |
Sumário: Introdução ao refinamento formal de dados. Leis de representação (ou de refinamento) envolvendo tipos de dados quasi-indutivos. Repertório de leis e suas funções de abstracção e de representação disponíveis em setcat.cam .
| Aula Teórica de 00.05.10 [Ref:3]: |
Sumário: Refinamento formal de dados (cont.): Propriedades da relação A <=B : reflexividade, transitividade e monotonicidade. Lei do refinamento estrutural e sua prova por cálculo de morfismos. Invariantes («concretos») induzidos por representação. Relação com a noção de representação gramatical. Exemplos: implementação de listas; síntese da implementação de GenDia à custa de DecTree.
| Aula Teórica de 00.05.17 [Ref:3]: |
Sumário: Não houve aula (tolerância do Enterro da Gata).
| Aula Teórica de 00.05.24 [Ref:3]: |
Sumário: Refinamento formal de dados (conclusão): Implementação de Tipos de Dados Indutivos. Introdução de apontadores em linguagens tipo C/C++. Desrecursivação orientada a linguagens tipo SQL. Teorema de desrecursivação genérica. Exemplos de aplicação: GenDia e DecTree.
| Aula Teórica de 00.05.31 [Ref:3]: |
Sumário: Introdução ao refinamento formal 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 de 'browsing' functoriais, eg. f-set implementada por f-seq.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.
Avaliação da disciplina.
| Aula Teórica de 00.06.07 (Aula suplementar) [Ref:3]: |
Sumário: Refinamento das operações (conclusão): 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. Eliminação de estruturas de dados intermédias («desflorestação»). Introdução de parâmetros de acumulação. Desrecursivação algorímica: cálculo de ciclos for/while.