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

Novo	Classificações finais da época especial

[ Equipa docente | Horário | Atendimento | Regime de Avaliação
Sumários | Programa Resumido | Programa Detalhado | Trabalho Experimental | Material Pedagógico
Bibliografia essencial | Bibliografia complementar | Provas de Avaliação | [NOVO] Classificações | Página principal ]

  Equipa docente

• Teóricas e teórico-práticas -- J.N. Oliveira (406006)

  Horário

Ref.	Dia	Hora	Tipo	Sala	Cursos	Docente
1	2.ª feira	9h00-11h00	TP(1)	DI-3	LMCC+LESI	J.N. Oliveira
2	2.ª feira	11h00-13h00	TP(2)	DI-3	LMCC	J.N. Oliveira
3	4.ª 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/0203; 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.N. Oliveira

  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

• Noção de modelo e de modelação formal. «Dimensões» de um modelo: sintaxe e semântica. APIs (`Application Program Interfaces'). Visão gramatical. `Domain specific languages'.
• Fundamentos do refinamento formal de dados. Refinamento de espécies de dados. Refinamento por cálculo. Lei do refinamento estrutural de tipos indutivos.
• Cálculo de refinamento formal de dados. Leis de isomorfismo. Repertório de inequações de refinamento e respectivas funções de abstracção e de representação. Teorema de desrecursivação genérica.
• Invariantes de refinamento. Cálculo de invariantes concretos induzidos por representação. Exemplos. Regra da síntese de invariantes concretos.
• Aplicações do refinamento formal de dados. Cálculo de refinamento para o modelo relacional da informação. Síntese da função de abstracção global. Implementação de tipos indutivos polinomais. Representação gramatical (BNF). Introdução de apontadores em linguagens tipo C/C++.
• Técnicas de refinamento algorítmico. Diagramas de refinamento de operadores. Caso particular: transformações naturais como refinamento de operadores functoriais. 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. Leis de fusão «horizontal» de processos algorítmicos: lei de Fokkinga e «banana-split». Refinamento por mudança da estrutura de dados virtual. Lei da introdução de parâmetros de acumulação. Desrecursivação algorítmica: cálculo de ciclos for/while.

  Programa Detalhado

• Introdução ao cálculo de programas. Análise das principais técnicas de refinamento (reificação) de especificações formais. Antecendentes históricos.
          Princípio da abstracção dos dados. Relações de abstracção e de representação. Invertibilidade. Inequações de refinamento da forma A <=B .

• Fundamentos do cálculo relacional. Análise dos operadores do cálculo relacional sob a forma de conecções de Galois. Propriedades. Leis de «shunting». Generalização dos principais combinadores funcionais (eg. split, either etc) a relações.

• Fundamentos do refinamento formal de dados. Leis de isomorfismo envolvendo tipos de dados quasi-indutivos (PA e A -> B). Propriedades da relação <=. Introdução ao repertório de inequações de refinamento e respectivas funções de abstracção e de representação.

• Cálculo de refinamento formal de dados. Teorema de desrecursivação genérica. Sua função de abstracção e invariante concreto. Relações de pertença estrutural e acessibilidade estrutural Exemplo: síntese da implementação de DecTree em SQL.
          Lei do refinamento estrutural de tipos indutivos Exemplos: relações de refinamento entre listas (morfismos blast e embed); síntese da implementação de GenDia à custa de DecTree. Prova construtiva da lei do refinamento estrutural de tipos indutivos.
          Implementação de tipos indutivos polinomais em linguagens com gestão de memória dinâmica: Introdução de apontadores em linguagens tipo C/C++. Introdução à representação gramatical (XML). Representação orientada a objectos.

• Cálculo de refinamento algorítmico. A eficiência como principal motivação para o refinamento algorítmico. Fases do refinamento algorítmico: simulação, redução do não-determinismo, mudança de estrutura de dados virtual.
          Lei de refinamento funcional -- satisfação de uma especificação implícita S por uma função f: S  |- f . Lei de refinamento relacional -- satisfação progressiva de uma especificação implícita S por outra especificação R: Propriedades de ordem parcial da relação   |- . Propriedade de -monotonia. Refinamento funcional. Leis de fusão «vertical» de processos algorítmicos (leis functoriais, de fusão e de absorção). Leis de fusão «horizontal» de processos algorítmicos: Lei de Fokkinga e «banana-split». Exemplos de aplicação.
          Paramorfismos. Dedução das regras de conversão de paramorfismos em hilomorfismos. Lei de refinamento de simultâneo de dados e algoritmos. Cálculo de ciclos while como hilomorfismos. Lei da introdução de parâmetros de acumulação. Desrecursivação algorítmica: cálculo de ciclos for/while.

• Prototipagem rápida e integração com outras tecnologias. Princípio da animação (vulg. «prototipagem») de especificações formais. Introdução ao VDM++. Integração de protótipos reactivos em arquitecturas cliente-servidor. Emulação de serviços intermédios («middleware») e de serviços de dados («dataware»). Integração com SQL. Especificação reversa de SQL e sua tradução em notação VDM-SL.

  Trabalho Experimental

• Tema proposto:

  Pacote de gestão de processos e organizações. Ver ficheiro mii0203tp.pdf no Material Pedagógico.

  NB: Nas condições do protocolo entre a Universidade do Minho e a IFAD [Licença académica para uso grátis das VDMTOOLS © pelo Departamento de Informática], o enunciado deste trabalho está escrito em inglês.

• Temas de projectos de outras disciplinas: compilação em curso

• Prazos de entrega: até três 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 publicado o calendário de orais de apresentação e demonstração dos trabalhos.

• Grupos de trabalho:

  Grupo	Nr	Nome	CoDisc	Tema	Oral
  1	30733	José Miguel Pereira Vilaça	7008N2	MFP-II	25-Jul, 16h00
  1	30730	João Paulo de Sousa Ferreira Fernandes	7008N2	MFP-II	25-Jul, 16h00
  2	30171	Bruno Maciel Almeida Costa	5308P3	DSI	Especial
  2	30164	Ângelo Simão Gonçalves Vilela	5308P3	DSI	Especial
  2	30175	Bruno Pacheco Machado dos Santos	5308P3	DSI	Especial
  2	30203	João Paulo dos Santos Martins	5308P3	DSI	Especial
  3	28146	Carla Susana Dantas Teixeira	7008N2	PED	25-Jul, 17h00
  3	28160	Lúcia Sofia de Sousa Belchior Miranda	7008N2	PED	25-Jul, 17h00
  4	29601	Alberto Manuel Gomes Mendes	7008N2	BD	16 Set, 10h30
  4	25351	Carlos Guilherme Pelaio Macedo Costa	7008N2	BD	16 Set, 10h30
  5	28152	Hélder Domingos Ferreira Mendes	7008N2	DSI
  5	28184	Rui Braga Nogueira Marques Ribeiro	7008N2	DSI
  5	30709	Conceição Silva Miranda Martins	7008N2	DSI
  6	30719	Filipe Leonel Ribeiro Pereira	7008N2	SDSD
  6	23188	José Manuel Certal Álvaro	7008N2	SDSD
  7	28191	Vítor Rui de Oliveira Gonçalves	7008N2	PP-IV
  7	28173	Miguel Filipe Teixeira Carreira	7008N2	PP-IV
  7	28142	Artur Jorge Oliveira de Carvalho	7008N2	PP-IV
  8	23777	Marlene de Jesus Camões Moura	7008N2		Especial?
  8	23218	Susana Marisa Morais Pacheco	7008N2		Desistiu?
  9	25351	Carlos Guilherme Pelaio Macedo Costa	7008N2	BD
  9	23201	Nélson Lopes Cardoso	7008N2	BD
  9	15889	Ricardo Miguel Carvalho Ferreira	7008N2	BD
  10	28136	Ana Luisa Pinto Teixeira	7008N2	MFP-II	Especial
  10	26327	Maria Inês Freitas de Campos	7008N2	MFP-II	Especial
  10	29016	Marco Paulo Martins da Cruz	7008N2	MFP-II	Especial
  11	8352	Óscar Fernando Ribeiro da Costa	7008N2	MFP-II	25-Jul, 18h00
  11	18690	Luís Pedro Morais Barata Valério	7008N2	MFP-II	25-Jul, 18h00
  11	13734	Fernando José Ribeiro Cunha Salgueiro	7008N2	MFP-II	25-Jul, 18h00
  12	28164	Márcio Abel Pereira Ferreira	7008N2	SDSD
  12	25400	Vânia Sofia Gomes Carvalho	7008N2	SDSD
  13	23163	Ana Cláudia Barbosa de Faria	7008N2	SDSD	22-Jul, 19h00
  13	23169	Balbina de Jesus Pereira Oliveira	7008N2	SDSD	22-Jul, 19h00
  14	20213	Noé Amorim da Rocha	7008N2		Especial
  14	23187	José Alves de Castro	7008N2		Especial

  Material Pedagógico

No ficheiro mii0203mp.zip encontram-se, até ao momento [data desta versão: 03.06.23]:

-

Ficheiro mii0203su_A.pdf - anexo aos sumários contendo algumas resoluções de exercícios das aulas práticas.

-

Ficheiro mi0203ln6.pdf - transparentes An Introduction to Algorithmic Refinement.

-

Ficheiro mi0203ln5.pdf - transparentes An Introduction to Data Refinement.

-

Ficheiro mi0203tp.pdf - tema para projecto da disciplina (Pacote de gestão de processos e organizações).

-

Ficheiros stack*.v*.

  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.ª	Sábado, 28 de Junho 2003	09h30	3303, 3304	...	pdf
Normal	2.ª	Sábado, 12 de Julho 2003	09h30	2302		pdf - incluindo a correcção
Recurso	-	3.ª-feira, 22 de Julho 2003	14h30	2202, 2208	...	pdf - incluindo a correcção
Especial	-	5.ª-feira, 4 de Setembro 2003	08h00	1208	2+18	pdf

  Classificações

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

Voltar à página principal de MFP-II.

Outras disciplinas leccionadas pelo DIUM