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

[ Equipa docente | Horário | Atendimento | Regime de Avaliação
Sumários | Programa Resumido | Programa Detalhado | Trabalho Laboratorial | Material Pedagógico
Bibliografia essencial | Bibliografia complementar | Provas de Avaliação | Notas Finais ]

  Equipa docente

• Teóricas -- J.N. Oliveira (406006)
• Teórico-práticas -- F.L. Neves (406085)

  Horário

Ref. Dia Hora Tipo Sala Cursos Docente

1 2.a feira 11h00-13h00 TP(1) DI-3 LMCC+LESI F.L. Neves

2 3.a feira 11h00-13h00 TP(2) DI-3 LMCC+LESI F.L. Neves

3 4.a feira 11h00-13h00 T DI-A1 LMCC+LESI J.N. Oliveira

  Atendimento

• Em qualquer altura: via email (jno@di.uminho.pt), devendo ser colocando no assunto o `string' MFP-II/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
  6.ª-feira	15h00-16h00	LMCC+LESI	J.N. Oliveira
  2.ª-feira	08h00-10h00	LMCC+LESI	F.L. Neves

  Regime de Avaliação

• Componentes:
  • t = informação teórica por prova escrita, sem consulta, de acordo com regulamentação interna em vigor (épocas normal, de recurso e especial)
  • p = informação prática correspondente à nota de um trabalho prático a realizar em grupo.

• Fórmula de avaliação: a nota final nf será dada pela fórmula:

  nf = if p < 9.5 then (if t > 16 then 16 else t) else p * 0.4 + t* 0.6

  sujeita à condição:

  t >= (if (p >= 9.5) then 8.0 else 9.5)

• Os alunos só poderão fazer melhoria de nota na época de recurso.

  Sumários

• Teóricas
• Práticas

  Programa Resumido

• Tipos de dados quasi indutivos. Hilomorfismos bem-fundados. Conjuntos e funções parciais finitas.
• Propriedades invariantes. Preservação de invariantes. Métodos de prova indutiva.
• Parcialidade, persistência, estado e comportamento reactivo. Operações. Pré- e pós-condições.
• Prototipagem e `embedding' de especificações formais. Arquitectura de `software' a 3 níveis (interface, `middleware', e dados). Componentes reactivos e suas APIs.
• Introdução ao refinamento e ao cálculo de programas. O binómio especificação-implementação. Validação e verificação formal. Síntese por transformação versus prova de correcção. Eixos de Refinamento
• Teoria da Reificação de Dados.
• Aplicações da Reificação de Dados - Cálculo de esquemas de base de dados relacionais. Refinamento de tipos de dados indutivos.
• Reificação das Operações. Síntese de programas como soluções de diagramas de refinamento. Cálculo de catamorfismos e de hilomorfismos. Síntese de C/C++.

  Programa Detalhado

• Propriedades de um tipo de dados. Invariantes. Obrigações de prova inerentes à preservação de propriedades invariantes. "Normware". Exemplos. 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.

• Tipos de dados quasi-indutivos (coálgebra out é bem-fundada e inversa à direita de in). Exemplo: PA . Seus hilomorfismos. o invariante fdp sobre P(A * B) e o correspondente tipo "função finita A -> B . Seus hilomorfismos e método de prova indutiva. Essência da prova indutiva. Relações bem-fundadas. Coálgebras bem-fundadas e seus anamorfismos. Terminação versus indução.

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

• Os tipos de dados quasi-indutivos PA e A -> B :
  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.

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

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

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

  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.

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

  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.

  Trabalho Laboratorial

• O enunciado do trabalho laboratorial desta disciplina já está disponível (documento em POSTSCRIPT compactado, 25K).
• O trabalho deve ser realizado por grupos com um máximo de três alunos.
• Deverá ser enviado, para avaliação, por correio electrónico para qualquer um dos docentes da disciplina, havendo o cuidado de citar o `string' MFP-II/9900: Trabalho Laboratorial no assunto da mensagem. Alternativamente, poderá ser entregue na recepção do Departamento de Informática.
• Prazos de entrega: até duas semanas antes da data de encerramento dos Livros de Termos (épocas normal, de recurso ou especial).
• Sessão de avaliação: Até duas semanas antes da data acima referida, deverá ser combinada com a equipa docente a sua discussão e demonstração.

  Material Pedagógico

1. Está disponível um ficheiro em formato tgz [32K] que, depois de expandido, deverá tornar disponíveis:

   -rw-rw-r--   1 jno      jno         40791 May 10 05:39 _mii9900tp.cam.ps
   -rw-r--r--   1 jno      jno          2215 Apr 30 03:15 ff.cam
   -rw-r--r--   1 jno      jno          7656 May  3 22:16 ffs.cam
   -rw-r--r--   1 jno      jno          2662 Nov 10  1999 int.cam
   -rw-r--r--   1 jno      jno          3008 Nov 17 07:00 io.cam
   -rw-r--r--   1 jno      jno         14100 May 10 05:33 mii9900tp.cam
   -rw-r--r--   1 jno      jno           952 Nov 10  1999 mon.cam
   -rw-r--r--   1 jno      jno          3513 Apr 12 01:53 mse.cam
   -rw-rw-r--   1 jno      jno           448 Apr 12 01:41 sae
   -rw-rw-r--   1 jno      jno          4272 Apr 18 22:55 sae.cam
   -rw-rw-r--   1 jno      jno          2400 Apr 18 22:55 saebib.cam
   -rw-r--r--   1 jno      jno          3081 Nov 10  1999 seq.cam
   -rw-rw-r--   1 jno      jno          8879 Mar 27 20:39 setcat.cam
   -rw-r--r--   1 jno      jno          1308 Nov  9  1999 sets.cam
   -rw-r--r--   1 jno      jno          2035 Feb  1 07:24 str.cam
   -rw-r--r--   1 jno      jno          2408 Nov 10  1999 tex.cam
   -rw-r--r--   1 jno      jno          1419 Nov 10  1999 txt.cam
   

   NB: Este ficheiro está sujeito a alterações no decorrer da disciplina [última actualização: 2000.05.10]; os alunos devem periodicamente verificar se a sua cópia está actualizada.

2. Observações:
   • Ficheiro setcat.cam - contém uma biblioteca de funções CAMILA que permitem «correr» o cálculo de estruturas de dados apresentado nas aulas.
   • O ficheiro sae.cam (e auxiliares sae*) contém uma pequena demo que foi realizada nas aulas.
   • Os ficheiros *mii9900tp* incluem material de apoio ao trabalho laboratorial.
   • Os restantes ficheiros são auxiliares e pertencem à biblioteca `standard' do CAMILA.

  Bibliografia essencial

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

Ol99b

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

  Bibliografia complementar

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.

Jon86

C. B. Jones.
Systematic Software Development Using VDM.
Series in Computer Science. Prentice-Hall International, 1986.
C. A. R. Hoare.

Mor90

C. Morgan.
Programming from Specification.
Series in Computer Science. Prentice-Hall International, 1990.
C. A. R. Hoare, series editor.

Ol99a

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

  Provas de Avaliação

• Época Normal
  • 1.ª chamada - 4.ª-feira, 14 de Junho 2000, 14h30, Sala 2309 -
    • Prova
  • 2.ª chamada - Sábado, 8 de Julho 2000, 9h30
    • Prova
• Época de Recurso - Sábado, 16 de Setembro 2000, 09h30, Salas 2302, 2306
  • Prova
• Época Especial - 7 de Dezembro 2000, 17h00, Sala 1319
  • Prova

  Notas Finais

Notas à data da época especial:

Nr REG Ano Nome Claissificação

11234 T-E 5 Abigail Vieira de Sá Faltou

9852 T-E 5 Aida Eduarda Ferreira da Silva Desistiu

23801 Ord 4 Alberto Manuel Brandão Simões 16

23161 Ord 4 Alexandre de Castro Santos 12

11235 T-E 5 Américo Leite da Costa Faltou

20186 Ord 5 Ana Paula da Silva Ferreira 10

14638 Ord 5 Anabela Mariano Teixeira Reprovado

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

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

12971 T-E 5 António Francisco da Costa Machado Reprovado

7807 Ord 5 António João de Carvalho Gama Rocha Faltou

17079 T-E 5 António José da Lomba Rodrigues Reprovado

9272 Ord 5 António Manuel Gomes Teixeira Faltou

11239 T-E 5 Armando César Dámaso Ferreira de Castro Faltou

15857 Ord 4 Arménia Moutinho Rua Faltou

7808 T-E 5 Belmiro de Castro Pereira Faltou

23170 Ord 4 Bruno Miguel da Cunha e Silva Reprovado

23172 Ord 4 Carla Manuela da Silva Araújo 11

18837 T-E 4 Carla Maria Mendes de Castro Faltou

15861 T-E 5 Carlos Manuel dos Santos Osório Faltou

7811 T-E 4 Daniel Carlos Mendes Rebelo Faltou

18844 Ord 5 Elsa Carina Teixeira Martins Reprovado

18673 Ord 5 Emanuel José Pereira Mota Faltou

18674 Ord 4 Emília Dulce Teixeira de Araújo Reprovado

15867 T-E 5 Eva Gonçalves Fernandes Desistiu

14822 T-E 5 Fernando Jorge de Oliveira Ferreira Faltou

12988 T-E 5 Fernando Jorge Fernandes Faltou

13734 Ord 4 Fernando José Ribeiro Cunha Salgueiro Faltou

23738 Ord 4 Filipe Ferreira Rocha Faltou

11751 Ord 5 Francisco José Martins Diz Faltou

9280 Ord 5 Gustavo Adolfo da Costa Neves Faltou

6217 T-E 5 Helder Alexandre Lacerda de Sousa e Silva Faltou

12994 T-E 5 Isabel Alexandra Dantas Alves de Araújo Reprovado

21803 Ord 4 Isabel Teresa Zagalo das Neves 11

23183 Ord 4 Joana Rita Henriques de Brito 13

20204 Ord 5 João Alberto Pereira Duarte 15

9284 Ord 5 João Manuel Bacelar Barreto Seabra Faltou

18683 Ord 5 João Manuel da Silva Abreu Reprovado

12996 T-E 5 João Manuel Lourenço Fernandes da Silva Faltou

19866 Ord 4 João Miguel Martins Veloso Soares Desistiu

18685 T-E 4 João Miguel Quintas Lopes Faltou

11250 Ord 4 Joaquim Manuel de Carvalho Pereira Faltou

18686 Ord 5 Joaquim Ricardo Ribeiro Gonçalves Faltou

20775 T-E 4 Jorge Filipe Pereira da Cruz Faltou

8342 Ord 5 Jorge Manuel Afonso de Freitas Faltou

14642 T-E 5 José Pedro Pinheiro Marques Faltou

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

14644 Ord 5 Luís Manuel da Fonseca Correia Nunes Faltou

11255 Ord 5 Luís Miguel Silva Ribeiro Faltou

15881 T-E 5 Magda Joana de Castro Pereira da Silva Faltou

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

12458 T-E 5 Manuel António Pereira Cardoso Faltou

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

18694 T-E 5 Manuela da Costa Fernandes Reprovado

13005 T-E 5 Maria Celeste Marques Pinto Desistiu

13736 Ord 5 Maria Cristina Carvalho Fernandes Faltou

11259 Ord 4 Maria da Conceição Gonçalves da Costa Faltou

23192 Ord 4 Maria Emília de Castro Ribeiro 11

23195 Ord 4 Maria Goreti Dias da Costa 10

15882 T-E 5 Maria Isabel Meireles Ribeiro Faltou

18881 Ord 5 Maria José Couto Nóvoa Reprovado

4624 T-E 5 Maria Paula Sampaio Coelho Faltou

20209 Ord 4 Maria Sofia Mendes de Sousa 15

20210 Ord 4 Mário Bento Brito Nóbrega Ramos de Azevedo Faltou

23197 Ord 4 Marisa Alexandra de Jesus Oliveira Moreira 11

23727 Ord 4 Miguel José Lopes Rodrigues Martins Vaz Desistiu

7832 Ord 5 Mónica Nogueira Santos Faltou

20213 Ord 4 Noé Amorim da Rocha Faltou

11267 T-E 5 Norberto dos Santos Cardoso Faltou

5798 Ord 4 Nuno Alexandre Varela dos Santos Faltou

20217 Ord 4 Nuno André de Sampaio Faria Reprovado

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

18706 Ord 5 Paula Cristina Neves Ferreira Faltou

20222 Ord 4 Paula Sofia Silva Rocha Gomes Morais Reprovado

6236 T-E 5 Paulo Alexandre Freitas Jorge Faltou

26346 T-E 4 Paulo José Portela Rodrigues Faltou

9306 Ord 5 Paulo Manuel Pacheco Moreira Faltou

15887 T-E 5 Raquel Maria Marinho Carvalho 11

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

15889 Ord 4 Ricardo Miguel Carvalho Ferreira Faltou

20176 Ord 4 Ricardo Nuno Martins de Sá 16

13740 T-E 5 Rosa Maria Barbosa Capa Reprovado

21150 T-E 4 Rui Daniel Queirós Faria Gonçalves 10

11757 T-E 5 Rui Edgar Pinto Jorge Faltou

11279 T-E 5 Rui Fernando Gomes Ribeiro Barroso Faltou

6240 Ord 5 Rui Manuel Duarte Araújo Faltou

26326 Ord 4 Rui Manuel Mendes Ribeiro Fonseca Martins Faltou

23210 Ord 4 Rui Miguel de Pinho Alves Ferreira Trabalho

20230 T-E 4 Rui Paulo Correia Monteiro 12

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

15892 Ord 5 Sandra Manuela Esteves da Silva Reprovado

21153 Ord 4 Sandra Maria Gomes Araújo Rodrigues Trabalho

20231 Mel 5 Sandra Maria Miranda Fernandes 12

18713 Ord 4 Sandra Susana Ferreira Coelho Faltou

20233 Ord 4 Sandro Filipe da Silva Almeida Reprovado

23214 Ord 4 Sara Alexandra Gomes Correia 12

20234 Ord 5 Sérgio Alberto Morim Petejo 13

18718 T-E 5 Sofia Lara Grosso Lobão Mendes de Freitas Desistiu

23216 Ord 4 Sónia Santos Leite 11

20241 Ord 4 Susana Azevedo Pereira Faltou

21154 Ord 4 Teresa Susana Mendes Pereira Reprovado

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