Métodos Formais de Programação II - 1999/2000
[ 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 | Notas Finais ]

  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 3.a feira 11h00-13h00 TP(2) DI-3 LMCC+LESI F.L. Neves

3 4.a feira 11h00-13h00 T DI-A1 LMCC+LESI J.N. Oliveira

  Atendimento

• Em qualquer altura: via email (jno@di.uminho.pt), devendo ser colocando no assunto o `string' MFP-II/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
  6.ª-feira	15h00-16h00	LMCC+LESI	J.N. Oliveira
  2.ª-feira	08h00-10h00	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
• Práticas

  Programa Resumido

• Tipos de dados quasi indutivos. Hilomorfismos bem-fundados. Conjuntos e funções parciais finitas.
• Propriedades invariantes. Preservação de invariantes. Métodos de prova indutiva.
• Parcialidade, persistência, estado e comportamento reactivo. Operações. Pré- e pós-condições.
• Prototipagem e `embedding' de especificações formais. Arquitectura de `software' a 3 níveis (interface, `middleware', e dados). Componentes reactivos e suas APIs.
• Introdução ao refinamento e 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 da Reificação de Dados.
• Aplicações da Reificação de Dados - Cálculo de esquemas de base de dados relacionais. Refinamento de tipos de dados indutivos.
• Reificação das Operações. Síntese de programas como soluções de diagramas de refinamento. Cálculo de catamorfismos e de hilomorfismos. Síntese de C/C++.

  Programa Detalhado

• Propriedades de um tipo de dados. Invariantes. Obrigações de prova inerentes à preservação de propriedades invariantes. "Normware". Exemplos. Prova de propiedades invariantes num modelo. Métodos indutivos de prova. Método de indução associado a um tipo indutivo. Exemplos: o tipo X = 1 + X e a indução natural. Indução sobre sequências finitas. Indução polinomial.

• Tipos de dados quasi-indutivos (coálgebra out é bem-fundada e inversa à direita de in). Exemplo: PA . Seus hilomorfismos. o invariante fdp sobre P(A * B) e o correspondente tipo "função finita A -> B . Seus hilomorfismos e método de prova indutiva. Essência da prova indutiva. Relações bem-fundadas. Coálgebras bem-fundadas e seus anamorfismos. Terminação versus indução.

• Introdução ao repertório de operadores sobre tipos quasi-indutivos. Principais operadores polimórficos e seus "teoremas grátis" (transformações naturais): elems , Pf, dom , ran , A -> f.

• Os tipos de dados quasi-indutivos PA e A -> B :
  1. filtros e os operadores functoriais Pf e A -> f.
  2. Alguns isomorfismos célebres como 2^A =PA , P(A * B) =(PB)^A , (B+1)^A =A -> B e o seu corolário 2^A =A -> 1.
  3. Exemplo de modelação com funções finitas e conjuntos - o suporte de dados do modelo relacional da informação.

• Especificação formal em grande escala. Das funções e assinaturas até às acções e as APIs. Parcialidade, persistência, estado interno e comportamento reactivo. Acções e sua decomposição funcional. Pré-condições. Prototipagem em CAMILA. Componentes e bibliotecas. Interfaces. Arquitectura a 3 níveis (dados, funções e "butões") e sua heterogeneidade tecnológica.

• Introdução ao processamento formal de 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.

• Introdução ao refinamento formal de dados. Leis de representação (ou de refinamento) envolvendo tipos de dados quasi-indutivos. Repertório de leis e suas funções de abstracção e de representação disponíveis em setcat.cam. Propriedades da relação A <= B : reflexividade, transitividade e monotonicidade. Lei do refinamento estrutural e sua prova por cálculo de morfismos.

  Invariantes («concretos») induzidos por representação. Relação com a noção de representação gramatical. Exemplos: implementação de listas; síntese da implementação de GenDia à custa de DecTree.

  Implementação de Tipos de Dados Indutivos. Introdução de apontadores em linguagens tipo C/C++. Desrecursivação orientada a linguagens tipo SQL. Teorema de desrecursivação genérica. Exemplos de aplicação: GenDia e DecTree.

• Introdução ao refinamento formal das operações. Síntese de programas (simulações, ou implementações) como soluções de diagramas de refinamento. Exemplo: cálculo de operações de `browsing' functoriais, eg. f-set implementada por f-seq.

  Solução de diagramas de refinamento com base em cálculo de catamorfismos e da exponenciação. Exemplo: operação de pertença em conjuntos.

  Técnicas de optimização algorítmica: 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»). Introdução de parâmetros de acumulação. Desrecursivação algorímica: cálculo de ciclos for/while.

  Trabalho Laboratorial

• O enunciado do trabalho laboratorial desta disciplina já está disponível (documento em POSTSCRIPT compactado, 25K).
• O trabalho deve ser realizado por grupos com um máximo de três alunos.
• Deverá ser enviado, para avaliação, por correio electrónico para qualquer um dos docentes da disciplina, havendo o cuidado de citar o `string' MFP-II/9900: Trabalho Laboratorial no assunto da mensagem. Alternativamente, poderá ser entregue na recepção do Departamento de Informática.
• 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

1. Está disponível um ficheiro em formato tgz [32K] que, depois de expandido, deverá tornar disponíveis:

   -rw-rw-r--   1 jno      jno         40791 May 10 05:39 _mii9900tp.cam.ps
   -rw-r--r--   1 jno      jno          2215 Apr 30 03:15 ff.cam
   -rw-r--r--   1 jno      jno          7656 May  3 22:16 ffs.cam
   -rw-r--r--   1 jno      jno          2662 Nov 10  1999 int.cam
   -rw-r--r--   1 jno      jno          3008 Nov 17 07:00 io.cam
   -rw-r--r--   1 jno      jno         14100 May 10 05:33 mii9900tp.cam
   -rw-r--r--   1 jno      jno           952 Nov 10  1999 mon.cam
   -rw-r--r--   1 jno      jno          3513 Apr 12 01:53 mse.cam
   -rw-rw-r--   1 jno      jno           448 Apr 12 01:41 sae
   -rw-rw-r--   1 jno      jno          4272 Apr 18 22:55 sae.cam
   -rw-rw-r--   1 jno      jno          2400 Apr 18 22:55 saebib.cam
   -rw-r--r--   1 jno      jno          3081 Nov 10  1999 seq.cam
   -rw-rw-r--   1 jno      jno          8879 Mar 27 20:39 setcat.cam
   -rw-r--r--   1 jno      jno          1308 Nov  9  1999 sets.cam
   -rw-r--r--   1 jno      jno          2035 Feb  1 07:24 str.cam
   -rw-r--r--   1 jno      jno          2408 Nov 10  1999 tex.cam
   -rw-r--r--   1 jno      jno          1419 Nov 10  1999 txt.cam
   

   NB: Este ficheiro está sujeito a alterações no decorrer da disciplina [última actualização: 2000.05.10]; os alunos devem periodicamente verificar se a sua cópia está actualizada.

2. 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.
   • O ficheiro sae.cam (e auxiliares sae*) contém uma pequena demo que foi realizada nas aulas.
   • Os ficheiros *mii9900tp* incluem material de apoio ao trabalho laboratorial.
   • Os restantes ficheiros são auxiliares e pertencem à biblioteca `standard' do CAMILA.

  Bibliografia essencial

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]).

Ol99b

J.N. Oliveira.
Recursion in the Pointfree Style.
33p., Departamento de Informática, Universidade do Minho, 1999.

  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.

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.

Ol99a

J.N. Oliveira.
An Introduction to Pointfree Programming.
37p., Departamento de Informática, Universidade do Minho, 1999.

  Provas de Avaliação

• Época Normal
  • 1.ª chamada - 4.ª-feira, 14 de Junho 2000, 14h30, Sala 2309 -
    • Prova
  • 2.ª chamada - Sábado, 8 de Julho 2000, 9h30
    • Prova
• Época de Recurso - Sábado, 16 de Setembro 2000, 09h30, Salas 2302, 2306
  • Prova
• Época Especial - 7 de Dezembro 2000, 17h00, Sala 1319
  • Prova

  Notas Finais

Notas à data da época especial:

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

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