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

Novo	Classificações à data da época especial

[ 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 | Classificações | Página principal ]

  Equipa docente

• Teóricas -- J.N. Oliveira (406006)
• Teórico-práticas -- J.B. Barros (406024)

  Horário

Ref. Dia Hora Tipo Sala Cursos Docente

1 2.a feira 11h00-13h00 TP(1) DI-3 LMCC+LESI J.B. Barros

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

3 4.a feira 14h00-16h00 TP(2) DI-3 LMCC+LESI J.B. Barros

  Atendimento

• Em qualquer altura: via email (jno@di.uminho.pt), devendo ser colocando no assunto o `string' MFP-II/0102; 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
  4.ª-feira	13h00-14h00	LMCC+LESI	J.N. Oliveira
  4.ª-feira	16h00-18h00	LMCC+LESI	J.B. Barros

  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 e práticas

  Programa Resumido

• Introdução às técnicas de reificação (refinamento) e de 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: dados e operações. Noções de abstracção e de representação.
• Teoria do refinamento formal dos dados. Cálculo de refinamento estrutural. Invariantes de representação.
• Aplicações do refinamento de dados. Transformação e migração de dados. Formatos isomorfos de dados. Processamento formal de dados. Especificação de operações de data-mining. Cálculo de esquemas de base de dados relacionais. Refinamento de tipos de dados indutivos. Recurso a apontadores em linguagens tipo C/C++.
• Teoria do refinamento formal das operações. Síntese de programas como soluções de diagramas de refinamento. Técnicas de optimização algorítmica: Leis da recursividade mútua (Fokkinga) e de «banana-split». 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.

  Programa Detalhado

• Noção de modelo e de modelação formal. «Dimensões» de um modelo: sintaxe e semântica. Modelos «são» álgebras. Introdução aos tipos algébricos de dados : noção de assinatura algébrica. Espécies e operadores. Assinaturas homogéneas/ heterogéneas. APIs (`Application Program Interfaces').
          Visão gramatical. `Domain specific languages'. Conversão de gramáticas independentes de contexto em assinaturas heterogéneas. Noção de termo sintático. Termos versus árvores sintáticas abstractas. [Ol95d, pp.1-18]
          Modelos de uma assinatura (álgebras). Recticulado de todos os modelos de uma assinatura. Modelo inicial e modelo terminal. [Ol95d, pp.33-38]

• Fundamentos do refinamento formal de dados. Refinamento de espécies de dados. Inequações da forma A <=B . Propriedades da relação A <=B: reflexividade, transitividade e monotonia. Cálculo estrutural. [Ol00b, pp.102-103] Funções de abstracção e de representação. Invertibilidade à direita e à esquerda. Caso particular: isomorfismos de modelos de dados. [Ol00b, pp.95-97] Lei do refinamento estrutural de tipos indutivos. Prova construtiva da lei do refinamento estrutural de tipos indutivos. [Ol00b, pp.104-107]
          Exemplos: relações de refinamento entre listas (morfismos blast e embed); síntese da implementação de GenDia à custa de DecTree. Estudo do refinamento relacional do modelo PPD. Estudo de um caso de aplicação de lei de refinamento estrutural: o modelo GenDia implementado por DecTree. [Ol00b, pp.105-106]

• Cálculo de refinamento formal de dados. Leis de isomorfismo envolvendo tipos de dados quasi-indutivos (PA e A -> B). Repertório de inequações de refinamento e respectivas funções de abstracção e de representação. [Ol00b, pp.98-101] Teorema de desrecursivação genérica e respectiva função de abstracção e de representação. [Ol00b, pp.112-117]
          Exemplos. Refinamento de conjuntos em sequências e tabelas de hashing. Síntese da implementação relacional de DecTree.

• Invariantes de refinamento. Cálculo de invariantes concretos induzidos por representação. Exemplos. Regra da síntese de invariantes concretos. [Ol00b, pp.108-109]

• Aplicações do refinamento formal de dados. Cálculo de refinamento para o modelo relacional da informação. [Ol00b, pp.109] Exemplo: cálculo da implementação relacional do moldelo de dados BAMS. Síntese da função de abstracção global. [Ol95d, pp.297-298]
          Implementação de tipos indutivos polinomais. Representação gramatical (BNF). [Ol95d, pp.104-107] Introdução de apontadores em linguagens tipo C/C++. [Ol00b, pp.110-112] Exercício sobre implementação «universal» de produtos e coprodutos em estruturas de apontadores. Implementação em C/C++ do tipo indutivo LTree.

• Técnicas de refinamento algorítmico. Diagramas de refinamento de operadores. Caso particular: transformações naturais como refinamento de operadores functoriais. Exemplo: f* implementa Pf. [Ol00c, pp.119-121]
          Leis de fusão «vertical» de processos algorítmicos (leis functoriais, de fusão e de absorção). Resolução de diagramas de refinamento por fusão-cata. Exemplo: cálculo de belongs sobre listas. [Ol00c, pp.121-124] Leis de fusão «horizontal» de processos algorítmicos: lei de Fokkinga e «banana-split' (revisão). [Ol00c, pp.132-136]
          Refinamento por mudança da estrutura de dados virtual. Exemplo de aumento de polinomialidade: derivação de bbelongs. Lei da introdução de parâmetros de acumulação. Desrecursivação algorítmica: cálculo de ciclos for/while. [Ol00c, pp.124-131]

  Trabalho Laboratorial

• Temas propostos:

  (A)

  Pacote de gestão de de horários e salas de aulas. Ver especificação VDM manuscrita em fotocópia.

  (B)

  Tema proposto na disciplina de Desenvolvimento de Sistemas de Informação.

  (C)

  Processador de base de dados de exames. Tema proposto pelos alunos do grupo.

  (D)

  Formalizaçao dos Processos de Migraçao de um DW. Tema proposto pelos alunos do grupo, em conjunto com a disciplina de SDSD.

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

• Grupos de trabalho:

  Nr	Nome	Grupo	Tema	Época
  24874	Rui José Gonçalves de Castro	G1	C
  20192	Carlos Henrique Chagas Alves	G1	C
  13734	Fernando José Ribeiro Cunha Salgueiro	G2	A
  18702	Nuno Miguel Sousa Nogueira	G2	A
  8352	Óscar Fernando Ribeiro da Costa	G2	A
  28144	Candida Susana Gonçalves da Silva	G3	B
  25374	Marlene Azevedo da Silva	G3	B
  26967	Nuno Miguel Feixa Rodrigues	G3	B
  25400	Vânia Sofia Gomes Carvalho	G4	D	recurso
  28149	Daniel Edgar Pinto Soares	G5	B	recurso
  28166	Maria da Conceição Vieira da Mota	G5	B	recurso
  28190	Vítor Manuel Almeida da Vinha Catarino	G5	B	recurso
  12994	Isabel Alexandra Dantas Alves de Araújo	G6	00/01	especial
  28873	David Filipe Oliveira Costa	G7	A
  13011	Sandra Cristina Marinho Gonçalves da Silva Lopes	G8	A	especial
  15881	Magda Joana de Castro Pereira da Silva	G8	A
  11259	Maria da Conceição Gonçalves da Costa	G8	A	especial

  Material Pedagógico

Apontamentos:

• Capítulo 3 (tipos «quase indutivos»)
• Capítulo 4 (refinamento de tipos de dados)
• Capítulo 5 (refinamento das operações)

• Folha de exercícios laboratoriais

  Bibliografia essencial

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 zipped 2.8 Mb (PDF+PS) file]).

Ol00a

J.N. Oliveira.
Quasi-inductive datatypes, June 2000.
Departamento de Informática, Universidade do Minho. Chapter of book in preparation.

Ol00b

J.N. Oliveira.
Data representation and refinement, June 2000.
Departamento de Informática, Universidade do Minho. Chapter of book in preparation.

Ol00c

J.N. Oliveira.
Operation refinement, June 2000.
Departamento de Informática, Universidade do Minho. Chapter of book in preparation.

  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.

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.

Ol99b

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

  Provas de Avaliação

Época	Chamada	Data	Hora	Salas	Inscritos	Prova
Normal	1.ª	4.ª-feira, 12 de Junho 2002	09h30	2207, 2208	1+33	pdf
Normal	2.ª	6.ª-feira, 5 de Julho 2002	09h30	2208,2209	51	pdf
Recurso	-	Sábado, 7 de Setembro 2002	09h30	2212	...	pdf
Especial	-	6.ª-feira, 15 de Novembro 2002	17h00	2303	0+13	pdf

  Classificações

[ Informação removida (RGPD artigo 17º) ]

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