Métodos Formais de Programação II - 2006/07
[ DI/UM ]

Novo	Classificações da época de especial -- ver Classificações.

[ Contacto | Página principal
| Equipa docente Horário | Atendimento | Regime de Avaliação
Sumários | Material Pedagógico | FAQs
Programa Resumido | Programa Detalhado | Trabalho Experimental |
Bibliografia essencial | Bibliografia complementar | Provas de Avaliação | Classificações ]

  Equipa docente

• Teóricas e teórico-práticas -- J.N. Oliveira (406006)

  Horário

Ref.	Dia	Hora	Tipo	Sala	Cursos	Docente
1	2.ª feira	16h00-18h00	TP	DI-A2	LMCC+LESI	J.N. Oliveira
2	5.ª feira	14h00-16h00	T	DI-A2	LMCC+LESI	J.N. Oliveira

  Atendimento

• Em qualquer altura: via correio electrónico (jno@di.uminho.pt), devendo ser colocado no assunto o `string' MFP-II/0607; 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
  2.ª-feira	09h00-10h00	LMCC+LESI	J.N. Oliveira
  5.ª-feira	09h00-10h00	LMCC+LESI	J.N. Oliveira

  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 e práticas

  Programa Resumido

• Introdução ao cálculo de programas. Princípio da abstracção dos dados. Relações de abstracção e de representação. Inequações de refinamento.

• Cálculo de refinamento formal de dados. Teorema de desrecursivação genérica. Relações de pertença estrutural e acessibilidade estrutural.
          Implementação de tipos indutivos polinomais em linguagens com gestão de memória dinâmica: Introdução de apontadores em linguagens tipo C/C++. Representação orientada a objectos.

• Cálculo de refinamento algorítmico. A eficiência como principal motivação para o refinamento algorítmico. Fases do refinamento algorítmico: simulação, redução do não-determinismo, mudança de estrutura de dados virtual.
          Lei de refinamento funcional. Lei de refinamento relacional. Leis de fusão «vertical» e «horizontal». Lei de refinamento de simultâneo de dados e algoritmos. Cálculo de ciclos while como hilomorfismos.

• Prototipagem rápida e integração com outras tecnologias. Introdução ao VDM++. Integração de protótipos reactivos em arquitecturas cliente-servidor. Emulação de serviços intermédios («middleware») e de serviços de dados («dataware»).

  Programa Detalhado

• Introdução. De volta ao ciclo de vida de Balzer e ao binómio especificação / implementação. Relações como especificações e funções como implementações. Necessidade de realizar (reificar) especificações. Princípio da reificação de um par pre/post por uma função f e sua transformação-PF. Generalização: satisfação de uma qualquer relação binária S por uma função f do mesmo tipo.
          Interpretação destes conceitos no contexto do VDM++. A omnipresença das variáveis de instância. Noção de estado interno de um modelo VDM++. Semântica relacional de uma operação (pre/post) em VDM++.

• Introdução ao refinamento de modelos. Reificação entre especificações por aumento simultâneo de definição e de determinismo, e reificação envolvendo mudança de tipos de dados. Noção de abstracção e de representação de dados. Refinamento de dados versus conversão de formatos. Aspectos práticos: migração e canalização de dados sem perda de informação.
          Caso mais simples: formatos isomorfos. Relaxe da relação de isomorfismo A =B à relação A <=B captando o facto de A ter menos informação que B. Exemplo: representação de conjuntos de naturais por sequências ordenadas sem elementos repetidos. Relações de abstracção (simples e sobrejectivas) e de representação (injectivas e inteiras). O requisito de invertibilidade.

• Refinamento de dados por cálculo. Manutenção do requisito de invertibilidade por inequações de representação. Exemplos envolvendo produtos e coprodutos. Cálculo simples de R e F para estes exemplos, baseado em leis de fusão. Noção de invariante concreto induzido por uma inequação de representação.
          Estudo de um catálogo de leis de refinamento de dados. O isomorfismo como caso particular de refinamento: revisão dos principais isomorfismos envolvendo produtos, coprodutos e funções (exponenciais). Apresentação dos isomorfismos de transposição de relações. Abordagem relacional ao refinamento de estruturas como listas, mappings, etc. Estudo das leis envolvendo <=. Papel da transposição na dedução destas leis.
          Propriedades da relação <=: reflexividade e transitividade e suas provas. Relacionadores (relators) e o refinamento estruturado.

• Recurso ao cálculo de pontos-fixos. Introdução ao refinemento de modelos de dados recursivos. Necessidade de hilomorfismos relacionais para exprimir abstracções e representações. Exemplos introdutórios: «fold» de conjuntos e de mappings.
          Funções monótonas, pré/pós-pontos-fixos. Teorema de Tarski. Notação µ. Resolução de equações relacionais. Casos típicos: hilo-equações e outras (eg. fecho transitivo). Teorema da fusão-µ e suas aplicações.
          Os tipos colectivos de dados em VDM-SL e seus hilomorfismos. O tipo map A to B. O tipo setof A. Catamorfismos relacionais. Predicados indutivos vistos como catamorfismos coreflexivos.
          Teorema de desrecursivação genérica e exemplos de aplicação. Estudo da função de abstracção e do invariante concreto associado a esta lei. Relações de pertença estrutural e acessibilidade estrutural.

• Cálculo de refinamento algorítmico. A eficiência como principal motivação para o refinamento algorítmico. Cálculo de ciclos for/while a partir de hilomorfismos. Introdução de parâmetros de acumulação. Leis de factorização iterativa. Uso do cálculo de hilomorfismos.

• Prototipagem rápida e integração com outras tecnologias. Princípio da animação de especificações formais. Noções gerais de arquitectura de `software'. Arquitectura cliente-servidor. Interfaces, APIs e «middleware».
          Introdução ao VDM++. Integração de protótipos reactivos em arquitecturas cliente-servidor. Emulação de serviços intermédios («middleware») e de serviços de dados («dataware»).

  Trabalho Experimental

• O tema do projecto é o Verified File-System
• Para uma primeira ideia do tema do trabalho vejam o artigo cujo PDF que se encontra na directoria VFSproject do Material Pedagógico
• Vamos basear-nos no trabalho já realizado no projecto Open Linux VERification (OLVER).
• O grupo de funções fs.* em linuxtesting.org/results/lsb_specs/by_group, por exemplo, dá uma ideia de como e por onde começar.
• O modelo FS que consta do apêndice aos sumários (secção B.2) será o nosso ponto de partida.
• Funcionaremos como uma empresa, devendo ser feitos time-cards de toda a actividade desenvolvida no projecto.
• Toda a documentação será escrita em inglês.
• Outros links que podem consultar:
  • en.wikipedia.org/wiki/Mondex
  • qpq.csl.sri.com/vsr/private/repository/MondexCaseStudy
  • secure.ucd.ie/documents/proposals/mondex.html

  Material Pedagógico

No habitual ficheiro zip encontram-se, até ao momento [data desta versão: 2007.06.17 ]:

• Directoria VFSproject: artigos sobre o projecto
• Directoria biblio: texto Data Transformation by Calculation que se recomenda como biliografia auxiliar
• Directoria aulas:
  • sumários das aulas (com o anexo actualizado), transparentes, etc:
  • Ficheiros i*r*.pdf - transparentes mostrados nas aulas.
  • Ficheiro RelCal2.pdf -- formulário (consultável no exame)
• Directoria vdm/doc: manuais
• Directoria vdm/examples: Ficheiros stack*vpp* em VDM++ apresentados nas aulas práticas.
• Directoria latex: vdmsl-2e.sty, a4.sty, vpp.sty, evdm.sty, etc -- ficheiros auxiliares ao pretty-printing de ficheiros vdm, vpp.

  Bibliografia essencial

John Fitzgerald, Peter Gorm Larsen, Paul Mukherjee, Nico Plat, and Marcel Verhoef.
Validated Designs for Object-oriented Systems.
Springer, New York, 2005.

C. B. Jones.
Systematic Software Development Using VDM.
Series in Computer Science. Prentice-Hall International, 1986.
C. A. R. Hoare.

J.N. Oliveira.
Program Design by Calculation . Draft of textbook in preparation.
Departamento de Informática, Universidade do Minho, 2005.

  Bibliografia complementar

R. Bird and O. de Moor.
Algebra of Programming .
Series in Computer Science. Prentice-Hall International, 1997.
C. A. R. Hoare, series editor.

J. Fitzgerald and P.G. Larsen.
Modelling Systems: Practical Tools and Techniques.
Cambridge University Press, 1st edition, 1998.

C. Morgan.
Programming from Specification.
Series in Computer Science. Prentice-Hall International, 1990.
C. A. R. Hoare, series editor.

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 zipped 2.8 Mb (PDF+PS) file]).

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

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

  Provas de Avaliação

Época	Chamada	Data	Hora	Salas	Inscritos	Prova
Normal	1.ª	25-Jun	14H00	1216, 1220, 1308	-	pdf
Normal	2.ª	4-Jul	09H30	1314, 2201	6+11+6	pdf
Recurso	-	20-Jul	14H00	1313, 2207	-	pdf
Especial	-	11-Set	17H00	2206	-	pdf

  Classificações

[ Informação removida (RGPD artigo 17º) ] Voltar à página principal de MFP-II.

Outras disciplinas leccionadas pelo DIUM