FAEP (Aulas teóricas)

Ano lectivo 2003/2004

Paula Gouveia

Sumários

1. 01 MARÇO
   Apresentação.
2. 04 MARÇO
   Considerações genéricas sobre  tipos de dados abstractos e sua relevância no âmbito da especificação formal, desenvolvimento e verificação de programas de grande escala. Noção informal de tipo de dados abstracto e sua especificação algébrica. Exemplo de trabalho: Torres de Hanói. 
3. 08 MARÇO
   Linguagem das especificações algébricas: assinaturas, termos, equações e especificações. Exemplos.
4. 11 MARÇO
   Substituição e instanciação. Cálculo equacional: sistema dedutivo e derivação. Exemplos.
5. 15 MARÇO
   Reescrita: regras de reescrita, sistemas de reescrita, redução, noções de computação terminada e divergente, forma normal. Sistema de reescrita induzido por especificação e derivação por reescrita. Exemplos.
6. 18 MARÇO
   Modelos: álgebras sobre assinatura, interpretação de termos, satisfação de equações e consequência semântica. Álgebra dos termos e álgebra dos termos fechados. Correcção do cálculo equacional (início).
7. 22 MARÇO
   Correcção do cálculo equacional (conclusão). Implementação vs. modelos. Exemplos. Homomorfismo entre álgebras, homomorfismo sobrejectivo, injectivo e isomorfismo.
8. 25 MARÇO
   Preservação da satisfação de equações entre termos fechados  por homomorfismo (prova feita na aula prática). Preservação da satisfação de equações  por homomorfismo sobrejectivo. Definição de categoria. Exemplos: Set, (C,<=), (M,.,e).
9. 29 MARÇO
   Exemplos de categorias: Par, Alg(Sigma), Mod(spec). Definições de objecto inicial e objecto terminal. Dualidade. Exemplos em Set, Par, (C,<=), (M,.,e), Alg(Sigma) (inicialidade da álgebra dos termos fechados). Definição de subcategoria. Exemplos. Isormorfismos. Prova de que objectos iniciais (terminais) são isomorfos e de que um objecto isomorfo a um objecto inicial (terminal) é também inicial (terminal).
10. 1 ABRIL
    Congruência em álgebra e álgebra quociente. Lema da interpretação de termos fechados em álgebra quociente. Categoria dos modelos de uma congruência.
11. 5 ABRIL
    Inicialidade da álgebra quociente na categoria dos modelos de uma congruência. Congruência gerada por especificação e álgebra quociente gerada por especificação. Categoria dos modelos de uma especificação como subcategoria da categoria dos modelos da congruência gerada pela especificação. Exemplo de que o recíproco não se verifica. Inicialidade da álgebra quociente gerada por especificação na categoria dos modelos da especificação (início). 
    
    8 ABRIL- Férias Páscoa
    
    12 ABRIL- Férias Páscoa
    
    
12. 15 ABRIL
    Conclusão da aula anterior. Prova de que álgebra quociente gerada por especificação é gerada pela assinatura e típica para a família vazia de variáveis na classe dos modelos da especificação. Extensão ao caso de uma qualquer álgebra inicial  na categoria dos modelos da especificação. Implementação apropriada. Prova de que qualquer modelo da especificação que seja gerado pela assinatura e típico para a família vazia de variáveis na classe dos modelos da especificação é inicial na categoria dos modelos da especificação (início)
13. 19 ABRIL
    Conclusão da aula anterior. Adequação do cálculo equacional. Exemplo de que equações com variáveis satisfeitas por uma implementação apropriada não são necessariamente satisfeitas por todos os modelos da especificação, mas são-no por qualquer outra implementação apropriada.
14. 22 ABRIL
    Construção rigorosa da álgebra quociente gerada por especificação a partir de uma especificação dada.
15. 26 ABRIL
    Adequação da derivação por reescrita no sistema de reescrita induzido por especificação. Referência à indecidibilidade das propriedades de terminação e confluência de sistemas de reescrita. Ordem de reescrita e ordem de redução (início).
16. 29 ABRIL
    Ordem de reescrita e ordem de redução (conclusão). Exemplos. Terminação vs ordem de redução. Ordem de redução obtida por interpretação em álgebra. Exemplos.
17. 3 MAIO
    Exemplos de sistemas não confluentes. Esboço da prova do lema dos pares críticos (início).
18. 6 MAIO
    Conclusão da aula anterior. Pares críticos. Exemplos de procura de pares críticos.
19. 10 MAIO
    Teorema dos pares críticos. Decidibilidade da confluência em sistemas de reescritas finitos e terminantes. Procedimento básico de completação. Exemplos.
20. 13 MAIO
    Desenvolvimento (usando o método da programação por camadas centrado nos dados) de um programa em Mathematica para determinar se fórmulas proposicionais dadas pelo utilizador são ou não tautologias, usando tableaux: início do exercício a concluir na aula prática. 
21. 17 MAIO
    Agregação e interligação de especificações: motivação. A categoria Sig e a categoria Spec.
22. 20 MAIO
    Revisões sobre coprodutos e co-igualadores. Soma amalgamada. Prova de que se pode obter uma soma amalgamada através de um coproduto e um co-igualador. Preenchimento dos inquéritos pedagógicos.
23. 27 MAIO
    Produtos na categoria Spec.
24. 31 MAIO
    Somas amalgamadas em Spec. 
25. 3 JUNHO
    Composição paralela de processos com e sem sincronização: motivação e exemplos. Produtos fibrados vs produtos e igualadores. A categoria Proc. Produto em Proc sua relação com  a composição paralela de processos sem sincronização.
26. 7 JUNHO
    Produtos fibrados em Proc e sua relação com  a composição paralela de processos com sincronização. Exemplos.
    
    

Fim