Métodos Formais de Programa��o II - 1998/99
[ DI/UM ]

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.a feira 10h00-12h00 T DI-A2 LESI+LMCC J.N. Oliveira 2 4.a feira 18h00-20h00 TP(1) DI-3 LESI+LMCC L.S. Barbosa

Atendimento

• Em qualquer altura: via email (jno@di.uminho.pt ), devendo ser colocando no assunto o 'string' MFP-II/9899; 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	12h00-13h00	LESI+LMCC	J.N. Oliveira
  Por definir	por definir	LESI+LMCC	L.S. Barbosa

Regime de Avalia��o

• Componentes:
  • t = informa��o te�rica por prova escrita 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 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 de Reifica��o de Dados - No��es de abstrac��o, de representa��o e de redund�ncia. Isomorfismo ou a equival�ncia entre representa��es. Epimorfismo ou a ordena��o de representa��es. No��o de invariante de abstrac��o. Ordem de redund�ncia.
• Aplica��es da Reifica��o de Dados - C�lculo de esquemas de base de dados relacionais. Modela��o E-R versus c�lculo alg�brico. Refinamento de tipos de dados indutivos. Desrecursiva��o. Representa��o gramatical de tipos indutivos.
• Reifica��o das Opera��es - S�ntese de programas como solu��es de diagramas de refinamento. C�lculo de catamorfismos e de hilomorfismos. T�cnicas de optimiza��o algor�tmica. Desfloresta��o. Refinamento com introdu��o de invariantes locais.
• Casos de estudo - C�lculo de opera��es de manipula��o de bases de dados e sua concretiza��o em SQL . C�lculo de um gestor de tabelas de 'hashing'. Redu��es monodais e c�lculo dos correspondentes ciclos for/while. 'Browsers'. C�lculo do problema �bill of materials� em suporte relacional. Generaliza��o a outros tipos hier�rquicos de dados.

Programa Detalhado

• Tipos de dados com invariantes.
  • Preserva��o de invariantes. Métodos indutivos de prova.
• C�lculo de Programas: Uma Introdu��o
  • O bin�mio especifica��o-implementa��o
  • Valida��o e verifica��o formal
  • T�cnicas de refinamento (reifica��o) - a abordagem �inventa & verifica� e seus inconvenientes. S�ntese por transforma��o versus prova de correc��o
  • Eixos de Refinamento
• Teoria de Reifica��o de Dados
  • No��es de abstrac��o, de representa��o e de redund�ncia
  • Isomorfismo ou a equival�ncia entre representa��es. O subc�lculo de isomorfismos. Exemplos de c�lculo
  • Epimorfismo ou a ordena��o de representa��es. No��o de invariante de abstrac��o. Ordem de redund�ncia. O subc�lculo de epimorfismos
• Aplica��es da Reifica��o de Dados
  • C�lculo de esquemas de base de dados relacionais
  • Abordagem formal � normaliza��o dos dados. Modela��o E-R versus c�lculo alg�brico
  • Refinamento de Tipos de Dados Indutivos. Leis de remo��o da recursividade em estruturas de dados. Exemplos de desrecursiva��o
  • Refinamento por �aumento� de recursividade
  • Representa��o gramatical de tipos indutivos. Convers�o/representa��o de gramáticas independentes de contexto em equa�ões polinomiais.
• Reifica��o das Opera��es
  • S�ntese de programas (simula��es, ou implementa��es) como solu��es de diagramas de refinamento
  • T�cnicas de optimiza��o algor�tmica.
  • C�lculo de catamorfismos. Leis de Fokkinga e �banana-split�.
• Casos de estudo
  • Exemplo 1 -- C�lculo de opera��es de manipula��o de bases de dados e sua concretiza��o em SQL
  • Exemplo 2 -- Redu��es monodais e c�lculo dos correspondentes ciclos for/while. 'Browsing' de listas e conjuntos.
• S�ntese final
  • Impacto do c�lculo de programas no desenho de bases de dados relacionais
  • C�lculo progressivo e sua integra��o com a prototipagem r�pida
  • No��o de estado. Especifica�ões com estado interno. Pré e p�s-condi�ões. Preserva��o relacional de invariantes.

Trabalho Laboratorial

• O enunciado do trabalho est� dispon�vel aqui .
• Este trabalho deve ser realizado por grupos com um m�ximo de tr�s alunos.
• O relat�rio dever� ser entregue, para avalia��o, na recep��o do Departamento de Inform�tica , at� duas semanas antes da data de encerramento dos Livros de Termos (�pocas normal, de recurso ou especial).
• At� uma semana 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 [13K] que, depois de expandido, dever� tornar dispon�veis:

-rw-r--r--   1 jno      jno         10648 Apr 21 00:16 bams.cam
-rw-r--r--   1 jno      jno          1692 Feb  3 13:39 ff.cam
-rw-r--r--   1 jno      jno          7122 Apr 29 00:41 ffs.cam
-rw-r--r--   1 jno      jno          2422 Feb 26 15:30 int.cam
-rw-r--r--   1 jno      jno          2971 Feb  3 13:39 io.cam
-rw-r--r--   1 jno      jno          1867 Apr 29 11:46 olap.cam
-rw-r--r--   1 jno      jno          2847 Feb 17 03:16 seq.cam
-rw-rw-r--   1 jno      jno          8568 Apr 29 00:32 setcat.cam
-rw-r--r--   1 jno      jno          1640 Feb  3 13:39 sql.cam
-rw-r--r--   1 jno      jno          2109 Feb  3 13:39 str.cam
-rw-r--r--   1 jno      jno          1398 Feb  3 13:39 txt.cam

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.

  NB:

  Este ficheiro est� sujeito a altera��es no decorrer da disciplina [�ltima actualiza��o: 1999.04.29]; os alunos devem periodicamente verificar se a sua c�pia est� actualizada.

• Ficheiro bams.cam - cont�m a demo bams que foi realizada nas aulas pr�ticas.
• Ficheiro olap.cam - cont�m o 'kit' para arranque do trabalho laboratorial .
• Os restantes ficheiros s�o auxiliares e pertencem � biblioteca 'standard' do CAMILA .

2.

Est� ainda dispon�vel um ficheiro em formato zip [495K] que contem um 'kit' de liga��o CAMILA -WINDOWS para apoio ao trabalho trabalho laboratorial. As instru��es de utiliza��o encontram-se no ficheiro mda99.doc que se obt�m ap�s a descompacta��o.

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.

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.

Ol95d

J. N. Oliveira.
Métodos Formais de Programa��o.
University of Minho, 4^th edition, 1997.
Textbook (489 p. in Portuguese [available as a 846K gzipped PS file]). English version under preparation at the time of writing.

Oli98

J. N. Oliveira.
A data structuring calculus and its application to program development, May 1998.
Lecture Notes (150 p. [available as a 390K gzipped PS file]). Departamento de Informatica, Facultad de Ciencias Fisico-Matematicas y Naturales, Universidad de San Luis, Argentina.

Provas de Avalia��o

• �poca Normal
  • 1.� chamada - 4.�-feira, 16 de Junho 1999, 9h30
    • Prova (incluindo correc��o)
  • 2.� chamada - 5.�-feira, 1 de Julho 1999, 9h30
    • Prova
• �poca de Recurso - 4.�-feira, 22 de Setembro 1999, 14h30, Sala 2304
  • Prova
• �poca Especial - 17 de Novembro 1999, 14h30, Sala 2312
  • Prova

Notas Finais

(a)

As alunas nrs. 7832 e 14638 devem contactar regente da disciplina por e-mail (jno@di.uminho.pt ).