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

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:

  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

Observações:

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

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

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