Métodos Formais de Programação I - 1999/2000
[ DI/UM ]

Novo	As notas finais à data da época especial (Dezembro) encontram-se disponíveis na secção respectiva.

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.ª-feira	09h00-11h00	TP(1)	DI-1.07	LMCC/LESI	L.S. Barbosa
2	5.ª-feira	09h00-10h00	T	DI-1.06	LMCC/LESI	J.N. Oliveira
3	5.ª-feira	10h00-11h00	T	DI-1.06	LESI/LMCC	J.N. Oliveira
4	5.ª-feira	11h00-13h00	TP(2)	DI-1.07	LESI/LMCC	L.S. Barbosa

Atendimento

• Em qualquer altura: via email (jno@di.uminho.pt), devendo ser colocando no assunto o 'string' MFP-I/9900; 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
  5.ª-feira	18h00-19h00	LESI/LMCC	J.N. Oliveira
  5.ª-feira	13h00-15h00	LESI/LMCC	L.S. Barbosa

Regime de Avaliação

• Nota teórica, por prova escrita sem consulta, 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

• Introdução à especificação formal como método de controlo de qualidade em 'software' .
• Composicionalidade. Combinação de programas. Modularidade e reutilização. «Dimensões» da informação. Sintaxe e semântica.
• Introdução à sintaxe formal. Introdução à semântica formal (teoria dos modelos).
• Breve introdução à categoria Set . Introdução às construções ditas primitivas. Estudo das construções ditas derivadas.
• Estudo da construção A* . Introdução ao conceito de catamorfismo. Apresentação dos conceitos de anamorfismo e de hilomorfismo. Parametrização (polimorfismo) e Functorialidade (politipismo). Noção de functor. Noção de bi-functor. Introdução à triologia cata-ana-hilo generalizada a a tipos de dados indutivos polinomiais. Estudo das propriedades dos catamorfismos polinomiais.
• Conversão de gramáticas independentes de contexto (notação BNF) em sistemas de definições de tipos indutivos polinomiais.
• Parametrização. Noção de functor de base. Noção de functor de tipo e sua formulação genérica como catamorfismo.

Programa Detalhado

• Introdução à especificação formal como método de controlo de qualidade em 'software' . Especificação formal -- porquê e para quê? Introdução aos binómio especificação /implementação. Ciclo de vida usando métodos formais.
• Ferramentas de apoio à utilização de especificação formal à escala industrial. Ambientes de prototipagem: CAMILA e VDMTOOLS® .
• Composicionalidade. Combinação de programas. Modularidade e reutilização. APIs ('Application Program Interfaces'). «Dimensões» da informação. Sintaxe e semântica. Introdução à sintaxe formal : noção de assinatura algébrica. Espécies e operadores. Assinaturas homogéneas/ heterogéneas. Conversão de gramáticas independentes de contexto em assinaturas heterogéneas. Noção de termo sintático. Termos versus árvores sintáticas abstractas.

• Introdução à semântica formal (teoria dos modelos) : Noção de modelo ou álgebra de uma assinatura. Breve introdução à categoria Set . Conceito de função. Diagrama funcional. Domínio e codomínio. Composição de funções. Função identidade. Notação com ou sem variáveis.

• Introdução às construções ditas primitivas. As estruturas A + B e A × B : O produto A × B («struct»), suas projecções e a construção <f,g>. O coproduto A + B («union»), suas injecções e a construção [f,g]. Propriedades universais e suas consequências. As construções functoriais f × g e f+g . Propriedades de absorção e suas derivadas. Invertibilidade à esquerda e à direita. Noção de isomorfismo. O isomorfismo A × B =B × A (swap). Outros isomorfismos célebres envolvendo produtos e coprodutos (assocr, undistr, etc). Lei da troca. Predicados e guardas. Condicional de McCarthy. Funções de ordem superior. Noção de espaço funcional. A exponencial B^A. Propriedade universal e suas consequências (cancelamento, fusão e reflexão). A construção functorial f^A e sua propriedade de absorção. Produtos e coprodutos n-ários ( n>=0 ). As funções ! : A ->1 e ? : 0 ->A . Tipos elementares genéricos: 0, 1 , 2 (Bool) e Nat . Segmentos iniciais.

• Estudo das construções ditas derivadas : Resolução da equação X =1 + A × X a partir de uma analogia com a programação imperativa. O conceito de «apontador» 1 + A. Funções constantes. O combinador c . Propriedades. Explicação dos isomorfismos A¹ =A e A° =1 . A construção A* (sequências finitas) como solução da equação X =1 + A × X. A álgebra [<>,cons] e a coálgebra sua inversa.

• Estudo da construção A* : Introdução ao conceito de catamorfismo usando o tipo A* =1 + A × A* . Resolução da equação funcional f ·[<>,cons] = g ·(id + id × f) . Exemplos de catamorfismos: length e elems . Apresentação dos conceitos de anamorfismo e de hilomorfismo usando o tipo A* =1 + A × A* . O factorial como hilomorfismo.

• Parametrização (polimorfismo) e Functorialidade (politipismo) : Noção de functor. Propriedades functoriais básicas. Exemplos: functor identidade, functor constante e a exponencial. Outros exemplos: apresentação informal da construção functorial f-seq em CAMILA. Noção de bi-functor. Propriedades. Exemplos: bi-functor produto e coproduto. Functores polinomais. Forma canónica de um functor polinomial. Lei do binómio de Newton. Noção de tipo de dados indutivo polinomial: Introdução à triologia cata-ana-hilo generalizada a a tipos de dados indutivos polinomiais. Estudo das propriedades dos catamorfismos polinomiais. Propriedade universal. Leis de reflexão, de cancelamento e de fusão. Conversão de gramáticas independentes de contexto (notação BNF) em sistemas de definições de tipos indutivos polinomiais. Parametrização. Noção de functor de base. Noção de functor de tipo e sua formulação genérica como catamorfismo.

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.

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 846K gzipped PS file]).

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 Normal
  • 1.ª chamada - 25 de Janeiro 2000, 09h30, Salas 2303 e 2304 - Prova
  • 2.ª chamada - 9 de Fevereiro 2000, 09h30, Sala 206 - Prova
• Época de Recurso - 7 de Setembro 2000, 14h30, Sala 2302
• Época Especial

Notas Finais

Observações:

• À data da Época especial (Dezembro).
• 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