| Métodos Formais de Programação I - 1999/2000 |
|---|---|
| [ 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/MI.HTML. Bibliografia.
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 aos binómio especificação /implementação.
Sumário: 1. Revisão de conceitos elementares de teoria dos conjuntos. 2. Introdução ao sistema CAMILA como um animador dessa teoria.
Sumário: 1. Revisão de conceitos elementares de teoria dos conjuntos. 2. Introdução ao sistema CAMILA como um animador dessa teoria.
Sumário: Composicionalidade. Combinação de programas. Modularidade e reutilização. APIs ('Application Program Interfaces'). «Dimensões» da informação. Sintaxe e semântica.Introdução à sintaxe formal : noção de assinatura algébrica. Espécies e operadores. Assinaturas homogéneas/ heterogéneas.
Sumário: Sintaxe formal (cont.) : Conversão de gramáticas independentes de contexto em assinaturas heterogéneas. Noção de termo sintático. Termos versus árvores sintáticas abstractas.
Sumário: 1. Exercícios 1.4, 1.5, 1.6 e 1.7 (Assinaturas e Gramáticas). 2. Revisão da noção de produto cartesiano e suas implementações em CAMILA .
Sumário: 1. Exercícios 1.4, 1.5, 1.6 e 1.7 (Assinaturas e Gramáticas). 2. Revisão da noção de produto cartesiano e suas implementações em CAMILA .
Sumário: Introdução à semântica formal (teoria dos modelos) : Noção de modelo ou álgebra de uma assinatura.Breve introdução à categoria Set . Conceito de função. Diagrama funcional. Domínio e codomínio. Composição de funções. Função identidade. Notação com ou sem variáveis.
Sumário: Teoria dos modelos (cont.) : introdução às construções ditas primitivas.As estruturas A + B e A ×B : O produto A ×B («struct»), suas projecções e a construção <f,g>. O coproduto A + B («union»), suas injecções e a construção [f,g]. Propriedades universais e suas consequências.
As construções functoriais f ×g e f+g. Propriedades de absorção e suas derivadas.
Sumário: Exploração da categoria Set: produto. Exercício: verificação de definição de f ×g 1.3 e 1.4 (do texto An Introduction to Pointfree Programming ). Derivação das leis de reflexão, fusão e absorção para o produto.
Sumário: Exploração da categoria Set: produto. Exercício: verificação da definição de f ×g 1.3 e 1.4 (do texto An Introduction to Pointfree Programming ). Derivação das leis de reflexão, fusão e absorção para o produto.
Sumário: Estudo das construções ditas primitivas (cont.) : continuação da aula teórica anterior.
Sumário: Estudo das construções ditas primitivas (cont.) : Invertibilidade à esquerda e à direita. Noção de isomorfismo. O isomorfismo A ×B =B ×A (swap). Outros isomorfismos célebres envolvendo produtos e coprodutos (assocr, undistr, etc).
Sumário: Exploração da categoria Set: coproduto. Exercício 1.12 (estendido à derivação das leis de absorção e funtorialidade, e verificação da definição de f + g). Exercícios 1.5, 1.6, 1.8 e 1.9 (do texto An Introduction to Pointfree Programming ).
Sumário: Exploração da categoria Set: coproduto. Exercício 1.12 (estendido à derivação das leis de absorção e funtorialidade, e verificação da definição de f + g). Exercícios 1.5, 1.6, 1.8 e 1.9 (do texto An Introduction to Pointfree Programming ).
Sumário: Estudo das construções ditas primitivas (cont.) : Lei da troca. Predicados e guardas. Condicional de McCarthy.
Sumário: Estudo das construções ditas primitivas (cont.) : Funções de ordem superior. Noção de espaço funcional. A exponencial BA. Propriedade universal e suas consequências (cancelamento, fusão e reflexão).
Sumário: 1. Experimentação das construções associadas ao produto e coproduto em CAMILA . 2. Exercício 1.7 (do texto An Introduction to Pointfree Programming ) e sua observação em CAMILA . 3. Construção de um modelo (funcional) e sua prototipagem em CAMILA para o BAMS.
Sumário: Não houve aula (Seminário sobre CAMILA na Univ. Bristol)..
Sumário: Estudo das construções ditas primitivas (conclusão) : A construção functorial fA e sua propriedade de absorção. Produtos e coprodutos n-ários ( n>=0). As funções ! : A ->1 e ? : 0 ->A. Tipos elementares genéricos: 0, 1, 2 (Bool) e Nat. Segmentos iniciais.
Sumário: Estudo das construções ditas derivadas : Resolução da equação X =1 + A ×X a partir de uma analogia com a programação imperativa. O conceito de «apontador» 1 + A.
Sumário: Não houve aula (Seminário sobre CAMILA na Univ. Bristol)..
Sumário: 1. Experimentação das construções associadas ao produto e coproduto em CAMILA . 2. Exercício 1.7 (do texto An Introduction to Pointfree Programming ) e sua observação em CAMILA . 3. Construção de um modelo (funcional) e sua prototipagem em CAMILA para o BAMS.
Sumário: Funções constantes. O combinador c . Propriedades. Explicação dos isomorfismos A¹ =A e A° =1 .Estudo das construções derivadas (cont.) : A construção A* (sequências finitas) como solução da equação X =1 + A ×X. A álgebra [<>,cons] e a coálgebra sua inversa.
Sumário: Estudo da construção A* : Introdução ao conceito de catamorfismo usando o tipo A* =1 + A ×A* . Resolução da equação funcional f ·[<>,cons] = g ·(id + id ×f) .
Sumário: 1. Forma condicional de McCarthy. Exercícios 1.13 e 1.14. 2. Exercícios 1.7, 1.16 e 1.22 (lei da troca e constantes) e sua verificação em CAMILA . 3. Derivação das leis de reflexão e fusão para o exponencial.
Sumário: Estudo da construção A* : Exemplos de catamorfismos: length e elems.Apresentação dos conceitos de anamorfismo e de hilomorfismo usando o tipo A* =1 + A ×A* . O factorial como hilomorfismo.
Sumário: Estudo da construção PA : Operações sobre conjuntos expressas como hilomorfismos sobre o tipo indutivo A* =1 + A ×A* .Parametrização (polimorfismo) e functorialidade (politipismo): breve introdução.
Sumário: 1. Derivação das propriedades functoriais da exponenciação. 2. Recursividade "pointfree": estudo de diversos catamorfismos sobre sequências (reduções por monoides, "mapping", "unzip" e sua inversa à esquerda. 3. Definição do catamorfismo sobre sequências como uma função em CAMILA . Observação em CAMILA dos exercícios anteriores.
Sumário: Não houve aula (Feriado nacional).
Sumário: (Cf. troca de turnos com CC) 1. Forma condicional de McCarthy. Exercícios 1.13 e 1.14. 2. Exercícios 1.7, 1.16 e 1.22 (lei da troca e constantes) e sua verificação em CAMILA . 3. Derivação das leis de reflexão e fusão para a exponencial.
Sumário: Parametrização (polimorfismo) e Functorialidade (politipismo) : Noção de functor. Propriedades functoriais básicas. Exemplos: functor identidade, functor constante e a exponencial. Outros exemplos: apresentação informal da construção functorial f-seq em CAMILA .
Sumário: Parametrização (polimorfismo) e functorialidade (politipismo) (cont.) : Noção de bi-functor. Propriedades. Exemplos: bi-functor produto e coproduto. Functores polinomiais.
Sumário: 1. Derivação das propriedades functoriais da exponenciação 2. Recursividade "pointfree": estudo de diversos catamorfismos sobre sequências (reduções por monóides, "mapping", "unzip" e sua inversa à esquerda. 3. Definição do catamorfismo sobre sequências como uma função em CAMILA . Verificação em CAMILA dos exercícios anteriores.
Sumário: Parametrização (polimorfismo) e functorialidade (politipismo) (cont.) : Functores polinomais. Forma canónica de um functor polinomial. Lei do binómio de Newton. Noção de tipo de dados indutivo polinomial: Introdução à triologia cata-ana-hilo generalizada a a tipos de dados indutivos polinomiais.
Sumário: Parametrização (polimorfismo) e functorialidade (politipismo) (cont.) : Estudo das propriedades dos catamorfismos polinomiais. Propriedade universal. Leis de reflexão, de cancelamento e de fusão.Conversão de gramáticas independentes de contexto (notação BNF) em sistemas de definições de tipos indutivos polinomiais.
Sumário: Não houve aula (Consulta médica do docente: aula reposta a 21.01.2000).
Sumário: 1. Exercícios sobre catamorfismos, anamorfismos e hilomorfismos. Aplicação a diversos functores. 2. Codificação dessas construções em CAMILA .
Sumário: Parametrização (polimorfismo) e functorialidade (politipismo) (cont.) : Parametrização. Noção de functor de base .
Sumário: Parametrização (polimorfismo) e functorialidade (politipismo) (conclusão) : Noção de functor de tipo e sua formulação genérica como catamorfismo.
Sumário: 1. Exercícios sobre catamorfismos, anamorfismos e hilomorfismos. Aplicação a diversos functores. 2. Codificação dessas construções em CAMILA .
Sumário: Os alunos não compareceram: participação nas Jornadas de LMCC concedida pela Direcção de Curso.
Sumário: Ferramentas de apoio à utilização de especificação formal à escala industrial. Ambientes de prototipagem. Apresentação do ambiente VDMTOOLS® - for Quality Software on Schedule pelo Dr. P.G. Larsen (IFAD ).
Sumário: Considerações finais. Avaliação e encerramento da disciplina.
Sumário: 1. Conclusão da aula anterior. 2. Exercícios sobre fusão-cata e construção de hilomorfismos retirados de provas de exame anteriores.
Sumário: Sessão extra: dúvidas e exercícios sugeridos pelos alunos.
Sumário: Sessão extra: dúvidas e exercícios sugeridos pelos alunos.