Métodos Formais de Programação II - 2000/01
[ 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 | Classificações | Página principal ]

  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 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 F.L. Neves

  Atendimento

• Em qualquer altura: via email (jno@di.uminho.pt), devendo ser colocando no assunto o `string' MFP-II/0001; 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	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 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

• Introdução às técnicas de refinamento (reificação) formal. O binómio especificação-implementação. Antecendentes históricos. Validação vs verificação formal. Prova de correcção. Verificação estática vs dinâmica. Semântica denotacional de linguagens de programação. O porquê da programação estruturada. Verificação vs cálculo de programas.

  Especificação directa e reversa. Compreensão e manutenção de programas. Exemplo de análise de um programa em C++ e conjectura da sua especificação formal recorrendo a catamorfismos.

• Métodos indutivos de prova. Da indução natural ( Nat0 =1 + Nat0) à indução sobre sequências (A* =1 + A * A*) e indução sobre tipos quasi indutivos (e.g. PA <=1 + A * PA). Indução polinomial.

• Teoria do refinamento algorítmico. Intercombinação de programas por fusão. Leis de fusão «horizontal» de processos algorítmicos. 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»). Leis de fusão «vertical» de processos algorítmicos (leis functoriais, de fusão e de absorção).

  Lei da introdução de parâmetros de acumulação. Desrecursivação algorímica: cálculo de ciclos for/while. Exemplo de utilização em engenharia reversa: análise do programa wc (C/Unix).

• Introdução às técnicas de refinamento dos 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.

  Diagramas de refinamento de operações. Abstração dos argumentos e representação dos resultados. Esquema de síntese de uma implementação como solução de um diagrama de refinamento.

  Cálculo de simulações. Exemplo: simulação de ina e de card. Refinamento algorítmico. Algoritmos de pesquisa e sua eficiência. Padrões de recursividade lineares vs bi-lineares. Alteração do padrão de recursividade da função belongsa.

• Teoria do refinamento formal de dados. Propriedades da relação A <=B: reflexividade, transitividade e monotonicidade. Leis de representação (ou de refinamento) envolvendo tipos de dados quasi-indutivos (PA e A -> B):
  PA =A -> 1
  0 -> A =1
  1 -> A =1 + A
  (C+B) -> A =(C -> A) * (B -> A)

  Repertório de leis e suas funções de abstracção e de representação, por exemplo:

  A -> B * C <=(A -> B) * (A -> C)
  A -> D * (B -> C) <= (A -> D) * ((A * B) -> C)

  Invariantes («concretos») induzidos por representação. Exemplos. Cálculo de invariantes concretos.

  Lei do refinamento estrutural de tipos indutivos. Exemplo: relações de refinamento entre listas (morfismos blast e embed). Prova por cálculo de morfismos. Mais exemplos: síntese da implementação de GenDia à custa de DecTree.

  Representação de tipos indutivos polinomais:

  • Representação gramatical (BNF).
  • Introdução de apontadores em linguagens tipo C/C++.
  • Desrecursivação orientada a linguagens tipo SQL. Teorema de desrecursivação genérica. Exemplo: síntese da implementação de DecTree em SQL.

• Modelação formal versus modelação em sistemas de informação de base relacional. Semântica formal de diagramas E-R (entidade relação) e seus invariantes. Exemplo - o problema PPD (árvores de produção e planeamento da produção). Reificação para modelo relacional do modelo PPD (árvores de produção e planeamento da produção).

• Componente laboratorial. Animação de especificações formais em VDM-SL. Definição de funções paramétricas que permitem realizar catamorfismos e anamorfismos sobre A*. Relações binárias e funções finitas. Resolução de exercícios: definição das funções dom, rng, A -> f, <:, <-:, pap e ++ sob a forma de morfismos sobre A -> B.

  Introdução à reengenharia formal de bases de dados relacionais. Apresentação de uma ferramenta de inversão formal de bases de dados (K-RF) desenvolvida em VDM-SL. Animação do cálculo de refinamento aplicado à engenharia reversa de bases de dados. Apresentação da ferramenta de auditoria à qualidade dos dados KARMA. Validação de invariantes em processos de limpeza de dados.

  Trabalho Laboratorial

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

Apontamentos:

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

Para obter os mesmos ficheiros em PDF (em lugar de Postscript), substituir no endereço respectivo "ps" por "pdf".

• 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 (inc. PDF and PS) file]).

Oli00a

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

Oli00b

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

Oli00c

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.ª	3.ª-feira, 12 de Junho 2001	09h30	1206, 1209, 1210	43 + 1	pdf.gz
Normal	2.ª	6.ª-feira, 6 de Julho 2001	09h30	2207 a 2209	61 + 1	pdf.gz
Recurso	-	6.ª-feira, 21 de Setembro 2001	09h30	1301	...	pdf.gz
Especial	-	2.ª-feira, 3 de Dezembro 2001	17h00	1214	18	pdf.gz

  Classificações

Observações:

• À data da época especial (Novembro)
• A pauta está ordenada por CoDisc (código de disciplina) e Nome dos alunos.
• Omitem-se os alunos não-avaliados.

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

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