Métodos Formais de Programação I - 1999/2000
[ DI/UM ]

Novo	As notas finais à data da época especial (Dezembro) encontram-se disponíveis na secção respectiva.

Equipa docente

• Teóricas -- J.N. Oliveira (406006)
• Teórico-práticas -- L.S. Barbosa (406023)

Horário

Ref.	Dia	Hora	Tipo	Sala	Cursos	Docente
1	4.ª-feira	09h00-11h00	TP(1)	DI-1.07	LMCC/LESI	L.S. Barbosa
2	5.ª-feira	09h00-10h00	T	DI-1.06	LMCC/LESI	J.N. Oliveira
3	5.ª-feira	10h00-11h00	T	DI-1.06	LESI/LMCC	J.N. Oliveira
4	5.ª-feira	11h00-13h00	TP(2)	DI-1.07	LESI/LMCC	L.S. Barbosa

Atendimento

• Em qualquer altura: via email (jno@di.uminho.pt), devendo ser colocando no assunto o 'string' MFP-I/9900; toda a resposta que tenha interesse geral será aqui afixada numa secção de 'FAQ's, a criar oportunamente.
• Sujeito a marcação verbal pelo docente respectivo, com um mínimo de uma semana de antecedência:

  Dia	Hora	Cursos	Docente
  5.ª-feira	18h00-19h00	LESI/LMCC	J.N. Oliveira
  5.ª-feira	13h00-15h00	LESI/LMCC	L.S. Barbosa

Regime de Avaliação

• Nota teórica, por prova escrita sem consulta, de acordo com regulamentação interna em vigor - épocas normal (1.ª ou 2.ª chamada), de recurso (Setembro) ou especial (Dezembro).
• Os alunos só poderão fazer melhoria de nota na época de recurso.

Sumários

• Teóricas e Práticas

Programa Resumido

• Introdução à especificação formal como método de controlo de qualidade em 'software' .
• Composicionalidade. Combinação de programas. Modularidade e reutilização. «Dimensões» da informação. Sintaxe e semântica.
• Introdução à sintaxe formal. Introdução à semântica formal (teoria dos modelos).
• Breve introdução à categoria Set . Introdução às construções ditas primitivas. Estudo das construções ditas derivadas.
• Estudo da construção A* . Introdução ao conceito de catamorfismo. Apresentação dos conceitos de anamorfismo e de hilomorfismo. Parametrização (polimorfismo) e Functorialidade (politipismo). Noção de functor. Noção de bi-functor. Introdução à triologia cata-ana-hilo generalizada a a tipos de dados indutivos polinomiais. Estudo das propriedades dos catamorfismos polinomiais.
• Conversão de gramáticas independentes de contexto (notação BNF) em sistemas de definições de tipos indutivos polinomiais.
• Parametrização. Noção de functor de base. Noção de functor de tipo e sua formulação genérica como catamorfismo.

Programa Detalhado

• Introdução à especificação formal como método de controlo de qualidade em 'software' . Especificação formal -- porquê e para quê? Introdução aos binómio especificação /implementação. Ciclo de vida usando métodos formais.
• Ferramentas de apoio à utilização de especificação formal à escala industrial. Ambientes de prototipagem: CAMILA e VDMTOOLS® .
• 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. Conversão de gramáticas independentes de contexto em assinaturas heterogéneas. Noção de termo sintático. Termos versus árvores sintáticas abstractas.

• 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.

• 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. 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). Lei da troca. Predicados e guardas. Condicional de McCarthy. Funções de ordem superior. Noção de espaço funcional. A exponencial B^A. Propriedade universal e suas consequências (cancelamento, fusão e reflexão). A construção functorial f^A 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.

• 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. Funções constantes. O combinador c . Propriedades. Explicação dos isomorfismos A¹ =A e A° =1 . 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.

• 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) . 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.

• 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. Noção de bi-functor. Propriedades. Exemplos: bi-functor produto e coproduto. 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. 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. Parametrização. Noção de functor de base. Noção de functor de tipo e sua formulação genérica como catamorfismo.

Bibliografia

BdM97

R. Bird and O. de Moor.
Algebra of Programming .
Series in Computer Science. Prentice-Hall International, 1997.
C. A. R. Hoare, series editor.

FL98

J. Fitzgerald and P.G. Larsen.
Modelling Systems: Practical Tools and Techniques .
Cambridge University Press, 1st edition, 1998.

Ol95d

J. N. Oliveira.
Métodos Formais de Programação.
Departamento de Informática, Universidade do Minho, 4.ª edição, 1998.
489 p. [available as a 846K gzipped PS file]).

Ol99a

J.N. Oliveira.
An Introduction to Pointfree Programming.
37p., Departamento de Informática, Universidade do Minho, 1999.

Ol99b

J.N. Oliveira.
Recursion in the Pointfree Style.
33p., Departamento de Informática, Universidade do Minho, 1999.

Provas de Avaliação

• Época Normal
  • 1.ª chamada - 25 de Janeiro 2000, 09h30, Salas 2303 e 2304 - Prova
  • 2.ª chamada - 9 de Fevereiro 2000, 09h30, Sala 206 - Prova
• Época de Recurso - 7 de Setembro 2000, 14h30, Sala 2302
• Época Especial

Notas Finais

Observações:

• À data da Época especial (Dezembro).
• A pauta está ordenada por CoDisc (código de disciplina) e Nome dos alunos.

No CoDisc Reg Ano Nome Classif.

23160 5307P6 ORD 4 Agostinho Manuel Araújo da Costa Desistiu

4958 5307P6 T-E 5 João Paulo Vieira de Brito Faltou

22690 5307P6 ORD 4 Marta Isabel Ferreira Moreira de Magalhães Oliveira Reprovado

19721 5307P6 T-E 3 Marta Isabel Moreira de Oliveira Reprovado

12646 5307P6 ORD 5 Marta Susana de Sousa Matos Faltou

11234 7007N2 T-E 5 Abigail Vieira de Sá Desistiu

23801 7007N2 ORD 4 Alberto Manuel Brandão Simões 18

23161 7007N2 ORD 4 Alexandre de Castro Santos 13

11235 7007N2 T-E 5 Américo Leite da Costa Desistiu

20186 7007N2 ORD 5 Ana Paula da Silva Ferreira 14

14639 7007N2 T-E 4 Angelina Maria da Silva Gonçalves Faltou

6835 7007N2 T-E 5 António dos Santos Afonso Faltou

7807 7007N2 ORD 5 António João de Carvalho Gama Rocha Faltou

9272 7007N2 ORD 5 António Manuel Gomes Teixeira Faltou

15857 7007N2 ORD 4 Arménia Moutinho Rua Reprovado

23170 7007N2 ORD 4 Bruno Miguel da Cunha e Silva 10

23172 7007N2 ORD 4 Carla Manuela da Silva Araújo 10

18837 7007N2 T-E 4 Carla Maria Mendes de Castro Faltou

21135 7007N2 ORD 5 Cristina Pires da Silva Cunha 12

7811 7007N2 T-E 4 Daniel Carlos Mendes Rebelo Faltou

21136 7007N2 T-E 5 Eduardo Jorge Teixeira Leite Pereira Faltou

18844 7007N2 ORD 5 Elsa Carina Teixeira Martins 10

18673 7007N2 ORD 5 Emanuel José Pereira Mota Reprovado

18674 7007N2 ORD 4 Emília Dulce Teixeira de Araújo 12

15867 7007N2 T-E 5 Eva Gonçalves Fernandes Desistiu

12988 7007N2 T-E 5 Fernando Jorge Fernandes Faltou

13734 7007N2 ORD 4 Fernando José Ribeiro Cunha Salgueiro Faltou

23738 7007N2 ORD 4 Filipe Ferreira Rocha Reprovado

11751 7007N2 ORD 5 Francisco José Martins Diz Faltou

9279 7007N2 T-E 5 Francisco Miguel da Costa Teixeira de Melo Faltou

12994 7007N2 T-E 5 Isabel Alexandra Dantas Alves de Araújo 10

21803 7007N2 ORD 4 Isabel Teresa Zagalo das Neves 11

23183 7007N2 ORD 4 Joana Rita Henriques de Brito 10

20204 7007N2 ORD 5 João Alberto Pereira Duarte 14

9284 7007N2 ORD 5 João Manuel Bacelar Barreto Seabra Faltou

18683 7007N2 ORD 5 João Manuel da Silva Abreu Reprovado

19866 7007N2 ORD 4 João Miguel Martins Veloso Soares 10

18685 7007N2 T-E 4 João Miguel Quintas Lopes Reprovado

11250 7007N2 ORD 4 Joaquim Manuel de Carvalho Pereira Faltou

7819 7007N2 T-E 3 Jorge António do Rego Guerra Faltou

20775 7007N2 T-E 4 Jorge Filipe Pereira da Cruz 13

8342 7007N2 ORD 5 Jorge Manuel Afonso de Freitas Reprovado

17090 7007N2 ORD 5 José David Campos Nunes 12

14642 7007N2 T-E 5 José Pedro Pinheiro Marques Faltou

7821 7007N2 T-E 5 Leonel Correia de Mendonça Faltou

15881 7007N2 T-E 5 Magda Joana de Castro Pereira da Silva Desistiu

13004 7007N2 T-E 3 Manuel Álvaro Gonçalves de Oliveira Faltou

11256 7007N2 T-E 5 Manuel António Dias Monteiro Faltou

11257 7007N2 T-E 5 Manuel Custódio Marinho Lopes Faltou

11259 7007N2 ORD 4 Maria da Conceição Gonçalves da Costa Faltou

23192 7007N2 ORD 4 Maria Emília de Castro Ribeiro 11

23195 7007N2 ORD 4 Maria Goreti Dias da Costa Reprovado

4624 7007N2 T-E 5 Maria Paula Sampaio Coelho Faltou

20209 7007N2 ORD 4 Maria Sofia Mendes de Sousa 11

20210 7007N2 ORD 4 Mário Bento Brito Nóbrega Ramos de Azevedo Reprovado

23197 7007N2 ORD 4 Marisa Alexandra de Jesus Oliveira Moreira 14

23727 7007N2 ORD 4 Miguel José Lopes Rodrigues Martins Vaz 14

20213 7007N2 ORD 4 Noé Amorim da Rocha Faltou

5798 7007N2 ORD 4 Nuno Alexandre Varela dos Santos Faltou

20217 7007N2 ORD 4 Nuno André de Sampaio Faria 12

11271 7007N2 T-E 5 Patrícia Manuela Tenreiro Santiago Faltou

18706 7007N2 ORD 5 Paula Cristina Neves Ferreira Faltou

20222 7007N2 ORD 4 Paula Sofia Silva Rocha Gomes Morais 10

26346 7007N2 T-E 4 Paulo José Portela Rodrigues 13

9306 7007N2 ORD 5 Paulo Manuel Pacheco Moreira Faltou

6237 7007N2 T-E 5 Rafael José da Cunha Ferreira Reprovado

9309 7007N2 T-E 5 Ricardo Jorge Miguel Dámaso de Oliveira Branco Faltou

15889 7007N2 ORD 4 Ricardo Miguel Carvalho Ferreira Reprovado

20176 7007N2 ORD 4 Ricardo Nuno Martins de Sá 19

13740 7007N2 T-E 5 Rosa Maria Barbosa Capa Reprovado

21150 7007N2 T-E 4 Rui Daniel Queirós Faria Gonçalves 12

6240 7007N2 ORD 5 Rui Manuel Duarte Araújo Faltou

26326 7007N2 ORD 4 Rui Manuel Mendes Ribeiro Fonseca Martins Reprovado

23210 7007N2 ORD 4 Rui Miguel de Pinho Alves Ferreira Reprovado

20230 7007N2 T-E 4 Rui Paulo Correia Monteiro 10

13011 7007N2 T-E 5 Sandra Cristina Marinho Gonçalves da Silva Lopes Faltou

15892 7007N2 ORD 5 Sandra Manuela Esteves da Silva 10

21153 7007N2 ORD 4 Sandra Maria Gomes Araújo Rodrigues 13

18713 7007N2 ORD 4 Sandra Susana Ferreira Coelho Desistiu

20233 7007N2 ORD 4 Sandro Filipe da Silva Almeida 10

23214 7007N2 ORD 4 Sara Alexandra Gomes Correia 12

23216 7007N2 ORD 4 Sónia Santos Leite 10

20241 7007N2 ORD 4 Susana Azevedo Pereira Reprovado

21154 7007N2 ORD 4 Teresa Susana Mendes Pereira 11

Voltar à página principal de MFP-I. Outras disciplinas leccionadas pelo DIUM