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

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	3.�-feira	11h00-13h00	TP(1)	DI/2	LMCC	F.L. Neves
2	4.�-feira	11h00-13h00	T	C2/321	LMCC/LESI	J.N. Oliveira
3	4.�-feira	14h00-16h00	TP(1)	DI/2	LESI	F.L. Neves
4	6.�-feira	11h00-13h00	TP(2)	DI/2	LESI	F.L. Neves

Atendimento

• Em qualquer altura: via email (jno@di.uminho.pt ), devendo ser colocando no assunto o 'string' MFP-I/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	13h00-14h00	LESI+LMCC	J.N. Oliveira
  4.�-feira	16h00-17h00	LESI+LMCC	F.L. Neves

Regime de Avalia��o

• Nota te�rica, por prova escrita, de acordo com regulamenta��o interna em vigor - �pocas normal (1.� ou 2.� chamada), de recurso (Setembro) ou especial (Dezembro).
• Os alunos s� poder�o fazer melhoria de nota na �poca de recurso.

Sum�rios

• Te�ricas e Pr�ticas

Programa Resumido

• M�todos Formais - apresenta��o do conceito e dos seus antecendentes hist�ricos. Ciclo de vida do desenvolvimento de software baseado em M�todos Formais .
• Inicia��o � teoria dos modelos. No��es b�sicas de teoria das categorias úteis em especifica��o formal. Modelos primitivos e derivados. Propriedades de reflex�o, fus�o, absor��o e cancelamento. Lei da troca.
• Parametriza��o e polimorfismo. Tipos de dados �s�o� functores. Morfismos entre tipos de dados (functores). Transforma��es naturais e seus teoremas gr�tis! .
• Introdu��o � especifica��o recursiva. No��o de ponto fixo. Ordens parciais. Cpos. Recticulados. Teoremas de Tarski e de Kleene. Pontos fixos em Set. Introdu��o ao c�lculo de isomorfismos.
• Convers�o de gram�ticas independentes de contexto em equa��es polinomiais. Recursividade polinomial.
• Tipos de dados indutivos. �lgebras de functores. Esquemas de funcionalidade recursiva: Catamorfismos, anamorfismos e hilomorfismos. Functores de tipo.

Programa Detalhado

• Introdu��o
  • M�todos Formais - apresenta��o do conceito e dos seus antecendentes hist�ricos.
  • Ciclo de vida do desenvolvimento de sistemas de software baseado em M�todos Formais .
• Inicia��o � teoria dos modelos
  • No��es b�sicas de teoria de conjuntos úteis na especifica��o formal de um programa
  • Modelos primitivos: a categoria Set e seu produto, coproduto e exponencia��o. Objectos iniciais e terminais. Propriedades de reflex�o, fus�o, absor��o e cancelamento. Lei da troca.
  • Modelos derivados: sequências, (sub)conjuntos e fun��es parciais finitas.
  • Tipos de dados �s�o� functores. No��o de functor. Functores polinomais.
  • Transforma��es entre tipos de dados (functores). Parametriza��o e polimorfismo. Transforma��es naturais e seus teoremas gr�tis! . M�todo Hindley-Milner para inferência de tipos.
• Introdu��o � especifica��o recursiva
  • No��o de ponto fixo. Ordens parciais. Cpos. Recticulados. Teoremas de Tarski e de Kleene.
  • Determina��o de solu��es de equa��es em Set. Pontos fixos em Set.
  • Introdu��o ao c�lculo de isomorfismos.
  • Convers�o de gram�ticas independentes de contexto em equa��es polinomiais. Recursividade polinomial.
• Tipos de dados indutivos.
  • �lgebras de functores. �lgebras iniciais e terminais.
  • Esquemas de funcionalidade recursiva: Catamorfismos, anamorfismos e hilomorfismos. Politipismo. Propriedades de reflex�o, fus�o, absor��o e cancelamento. Functores de tipo.
  • Esquemas funcionais dos modelos derivados.

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.

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.

Material Pedag�gico

• Apontamentos auxiliares para a disciplina:
  • Cap�tulo 1 - p�gs.3-36: 90228 bytes de Postscript
  • Cap�tulo 2 - p�gs.37-52: 47845 bytes de Postscript
  ou ambos os ficheiros em formato *.tar.gz: 137876 bytes.
• Procure aqui se estiver interessado em obter m�dulos CAMILA que apoiam a mat�ria da disciplina.

Provas de Avalia��o

• �poca Normal
  • 1.� chamada - 29 de Janeiro 1999, 09h30, Salas 2319 e 2320 - Prova (incluindo correc��o)
  • 2.� chamada - 15 de Fevereiro 1999, 14h30, Sala 2211 - Prova
  • �poca de Recurso - 8 de Setembro de 1999, 14h30, Sala 2304 - Prova

Notas Finais

• � data da �poca de Recurso.
• A pauta est� ordenada por CoDisc (c�digo de disciplina) e Nome dos alunos.