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

Novo	Classificações finais da época 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	11h00-13h00	TP	DI-0.11	LMCC+LESI	J.N. Oliveira
2	2.ª feira	14h00-16h00	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/0506; 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
  6.ª-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. A «equação de Wirth» Algorithms + Data Structures = Programs e o binómio especificação / implementação. Necessidade de eficiência. Eficiência das implementações versus clareza das especificações. Noçao de detalhe de implementação. Múltiplas implementações para a mesma especificação (modelo). Necessidade de estratégias (ordens) para o refinamento.

• Introdução ao refinamento de modelos. Princípios gerais de substituição de um modelo por outro. Nível algorítmico: relação de satisfação (substituição, ou refinemento). A tradicional ordem s menos definido do que r entre autómatos de estados finitos (vistos como funções de estado actual para estados sucessores). Nível dos dados: necessidade de mudança de formato dos dados. Caso mais simples: formatos isomorfos. Relaxe da relação de isomorfismo à relação A <=B captando o facto de A ter menos informação que B. Relações de abstracção (simples + sobrejectivas) e de representação (injectivas e inteiras).

• Refinamento de dados por cálculo. Exemplo introdutório:lei da representação por «apontador»: Estudo do isomorfismo de totalização de correspondências.
          Início do estudo do repertório de inequações de refinamento e respectivas funções de abstracção e de representação. A projecção relacional e seu caso particular para relações simples f -> g que é usado em funções de abstração/representação.
          Propriedades da relação <=: reflexividade e transitividade e suas provas. Relacionadores (relators) e o refinamento estruturado. Análise detalhada das representações e abstracções das leis estudadas até ao momento.
          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.

• Recurso ao cálculo de pontos-fixos. 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.
          Leis do refinamento relacional -- satisfação progressiva de uma especificação implícita S por outra especificação R. Propriedades de ordem parcial da relação   |- . Propriedade de -monotonia.
          Refinamento funcional -- satisfação de uma especificação implícita S por uma função f. Exemplos.
          O refinamento funcional f  |- g e a procura de eficiência. Leis de fusão «vertical» de processos algorítmicos (leis functoriais, de fusão e de absorção). Leis de fusão «horizontal» de processos algorítmicos. A lei de Fokkinga e o seu corolário «banana-split».
          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.

• Polimorfismo paramétrico. Teorema «grátis» de um tipo polimórfico t. Operador de Reynolds. Exemplos. Teorema «grátis» do operador cata (_ e seus corolários. Leis de fusão e de absorção.

• 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

Novo	Registo de problemas que alguns de vocês me enviaram quanto ao uso das VDMTools

NB: Nas condições de benefício de licença académica para uso grátis das VDMTOOLS pelo Departamento de Informática, o enunciado deste trabalho está escrito em inglês.

• Project requirements:
  A Bologna 2nd Cycle Course Server
  The following data model in VDM-SL notation

          types
          
          Course :: name: seq of char
                    credits: ECTSs;
          ECTSs = map ACMtopic to nat1;
          
          CourseId = token;
          IdDeg = token;
          StudentId = token;
          ACMtopic  = token;
          Classif  = real;
          
          Univ :: courses: map CourseId to Course
                  degrees: map IdDeg to ECTSs
                  students: map StudentId to (IdDeg * map CourseId to Classif)
  		topics: map ACMtopic to ACMtopic
  	inv u == degreesOk(u) and coursesOk(u) and topicsOk(u)
  
  functions
  
  	degreesOk: Univ -> bool
  	degreesOk(u) == { a | mk_(a,b) in set rng u.students } subset dom u.degrees;
  
  	coursesOk : Univ -> bool
  	coursesOk(u) == dunion { dom b | mk_(a,b) in set rng u.students } subset dom u.courses ;
  
  	topicsOk : Univ -> bool
  	topicsOk(u) == dunion { dom x | x in set rng u.degrees } union
  		       dunion { dom x.credits | x in set rng u.courses } subset allTopics(u) ;
  
  	allTopics: Univ -> set of ACMtopic
  	allTopics(u) == dom u.topics union rng u.topics
  

  should be regarded as the starting point for a model recording the offer of a particular university with respect to its 2nd Cycle Course curricula.

  All courses should be regarded as elective. Given university u, students get their degrees once the courses they have completed with success amount at least the number of ECTSs which are required by their degree's specification. Among the functionality required by the model, the following should be considered at least:

          allCred : StudentId * Univ -> ECTSs
  

  which computes the current ECTS total of a particular student,

          calCred : StudentId * Univ -> ECTSs
  

  which computes the multiset of ECTSs which a particular student is still required to obtain in order to complete her/his degree.

  The most interesting functionality will be that which, given students' topic preferences and the degree they are targeting at, suggest which courses they should undertake.

• Project specification:

  The project consists of building a VDM++ model of the proposed theme and, using the VDMTools API, converting it into the server of a web-service which should help students in choosing courses and degrees in the 2nd cycle of their degrees. Students are welcome to investigate details of the proposed theme and come up with a realistic prototype.

• Bibliography:

  A LabMF project report will be of help concerning the overall Java layer architecture of the web-service.

  Material Pedagógico

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

iar.pdf - transparentes An Introduction to Algorithmic Refinement

Ficheiros *.cam - módulos CAMILA cuja funcionalidade pode ser útil transliterar para VDM na realização do trabalho prático.

tffsl.pdf - transparentes Theorems for Free: an Introduction

mii0506su*.pdf -- sumários, incluindo apêndices

idr.pdf -- transparentes Uma Introdução ao Refinamento de Dados (aulas em curso).

irhsl.pdf -- transparentes An Introduction to Relational Hylomorphisms (aulas em curso).

Directoria mii0506_vdm

mii0506.vdm* -- especificações VDM das aulas práticas

vdmsl-2e.sty, a4.sty, vpp.sty, evdm.sty, etc -- ficheiros auxiliares ao processamento L^ATEX de mii0506.vdm

Ficheiros stack*vpp* em VDM++ apresentados nas aulas práticas.

Ficheiros relativos à execução do trabalho proposto na disciplina:

• iApiMan_letter.pdf -- Manual de Utilização da API das VDMTools (©IFAD)
• acm*ml -- Taxonomia de tópicos ACM (gentilmente comunicada pelo Prof. )

  Bibliografia essencial

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

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

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.

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

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.ª	4.ª-feira, 21 de Junho de 2006	09h30	1316 a 1318	34	pdf
Normal	2.ª	2.ª-feira, 10 de Julho 2006	14h00	2201, 2202	45	pdf
Recurso	-	Sábado, 22 de Julho 2006	09h30	2210, 2211	...	pdf
Especial	-	2.ª-feira, 9 de Outubro 2006	16h00	2205	...	pdf

  Classificações

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

Voltar à página principal de MFP-II.

Outras disciplinas leccionadas pelo DIUM