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

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

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

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	5.�-feira	09h00-11h00	T	DI-A2	LMCC/LESI	J.N. Oliveira
2	5.�-feira	14h00-16h00	TP(1)	DI-0.11	LESI/LMCC	L.S. Barbosa

Atendimento

• Em qualquer altura: via correio-electrónico, devendo ser colocado no assunto o `string' MFP-I/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
  5.�-feira	13h00-14h00	LESI+LMCC	J.N. Oliveira
  4.�-feira	08h00-11h00	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 ou especial -- 80%
• Avaliação contínua nas aulas práticas e laboratoriais -- 20%

Sumários

• Teóricas e Práticas

Programa Resumido

• Métodos formais e controlo de qualidade em `software' . Ciclo de vida usando métodos formais. Redução do risco e dos custos. Resolução de problemas por modelação e cálculo. Requisitos e modelos. Prototipagem e animação. Validação por teste. Não-determinismo e parcialidade. Necessidade de modelar com relações. Relação (especificação) versus função (implementação).

• Linguagens e métodos para especificação formal. Estudo do `standard' ISO/IEC 13817-1 (VDM-SL). Especificação por pré/pós-condições. Invariantes. Sub-especificação e não-determinismo. Modelação por conjuntos, sequências e funções finitas.

• Introdução ao cálculo de relações. Combinadores relacionais básicos. Taxonomia de relações binárias. Ordens. Estruturação do cálculo relacional com base em conecções de Galois. Formulação de propriedades em notação ``pointfree''. O cálculo funcional como caso particular.

• Semântica relacional da notação VDM-SL. Significado de um modelo VDM-SL. Semântica relacional de um par pre-/post-. Relações em compreensão. ``Mappings'' e suas propriedades.

• Invariantes. Significado de um invariante em VDM-SL. Prova de preservação de um invariante. Noção de precondição mais fraca que garante uma propriedade. Exemplos. A integridade-referencial como uma classe de invariantes sobre relações simples e finitas em bases de dados. Diagramas Entidades-Relações (ER) e sua semântica pointfree baseada na preordem de definição de relações.

• Especificação indutiva. Estratégia de divide-and-conquer e sua captação sob a forma de um hilomorfismo relacional. Cálculo de pontos-fixos. Notação �. Teorema da fusão-�. Aplicações: os tipos colectivos de dados em VDM-SLe seus hilomorfismos.

• Prototipagem e animação. Casos de estudo laboratorial. Ambientes de desenvolvimento formal. Experiência com a utilização do ambiente VDMTOOLS - for Quality Software on Schedule da CSK. Objectificação: evolução de um modelo VDM-SL para VDM++)

Programa Detalhado

• A especificação formal como método de controlo de qualidade em `software' Motivação: especificação formal -- porquê e para quê? Introdução ao binómio especificação /implementação. Adopção do `standard' ISO/IEC 13817-1 (VDM-SL). Ciclo de vida do desenvolvimento formal de `software' . Áreas típicas de aplicação. Sistemas críticos e confiáveis. Especificação formal construtiva. Modelação de um problema. Prototipagem e animação. Validação por teste. Importância da verificação formal das propriedades de um modelo. Não-determinismo e parcialidade. Necessidade de modelar com relações.

• Introdução ao cálculo de relações. Inclusão de relações. Composição e intersecção de relações. Monotonia da composição: Conversa de uma relação e a propriedade de contravariância. Ordens e sua taxonomia. As funções vistas como casos particulares de relações.

• O cálculo relacional «pointfree». Formulação de propriedades em notação «pointfree». Exemplo -- injectividade de uma função f. Os operadores ker e img. Relações inteiras (totais), sobrejectivas e simples (funcionais). Taxonomia de relações binárias. A igualdade entre relações, «pointwise» e «pointfree»: a inclusão cíclica (vulg «ping-pong») e a igualdade indirecta. Igualdade de funções. Transformada-PF. Representação de predicados unários (conjuntos) por coreflexivas ou por condições. Estruturação do cálculo relacional com base em conecções de Galois (CG). Quadro das principais CG do cálculo relacional. As propriedades básicas de uma CG intuídas a partir de um exemplo da aritmética. Exemplos: converso, regras de «shunting», divisão relacional. Intersecção e união. Versões relacionais de <R,S> e [R,S] como conecções de Galois. Definição de uma relação. Domínio e contradomínio como conecções de Galois.

• Semântica relacional da notação VDM-SL. Significado de uma especificação via pré/pós-condições em VDM-SL. Semântica relacional de um par pre- / post-: Spec =Post · Pre . Papel da pre-condição. Relações em compreensão. Relações simples finitas e sua representação em VDM-SL(«mappings»). Uso do operador ker f em pós-condições para especificar relações de equivalência. Exemplo: isPermutation = ker seq2bag. Semântica relacional dos operadores de VDM-SL. Versão relacional do condicional de McCarthy e sua utilização na semântica do operador de sobreposição de funções parciais finitas.

• Cálculo de propriedades em VDM-SL. Significado informal de um invariante em VDM-SL. Sintaxe VDM-SLpara invariantes. Exemplos de invariantes e sua relação com as regras de negócio dos sistemas de informação. Obrigações de prova associadas à formulação de invariantes e pares pré/pós-condição Spec = (pre,post): (a) satisfabilidade e sua transformada-PF; (b) preservação de invariantes e sua transformada-PF. Caso particular em que Spec é uma função. Necessidade de leis de cálculo-PF para realizar estas provas. Noção de invariante como tipo.

• Aplicações. A integridade-referencial como uma classe de invariantes sobre relações simples e finitas em bases de dados. Diagramas Entidades-Relações (ER) e sua semântica pointfree baseada na preordem de definição de relações. Exemplos: relacionamentos M:M e M:1. Diagramas ER e sua semântica relacional (conclusão): Relacionamentos 1:1. Preservação de integridade referencial.

• Prototipagem e animação. Ambientes de desenvolvimento formal. Casos de estudo laboratorial. Experiência com a utilização do ambiente - for Quality Software on Schedule da CSK.

Práticas Laboratoriais

Informação sobre VDMTOOLS : entrar em www.vdmbook.com/tools.php, onde uma versão livre está disponível para Windows

Material Pedagógico

• Em ficheiro zip encontram-se, até à data desta versão [2006.12.22] os ficheiros/directorias:

  

  Ficheiro mi0607su.pdf - sumários completos com anexo

  

  Ficheiros ifmsl.pdf - transparentes An Introduction to Formal Modelling
  (22 slides).

  

  Ficheiros rfmsl_small.pdf - transparentes Relational Formal Modelling em formato para impressão

  

  Ficheiro mpiCalFun.pdf - contendo tabela de leis de cálculo funcional.

  

  Ficheiro miCalRel.pdf - contendo tabela de leis de cálculo relacional.

• Guião das sessões de laboratório sobre VDMTOOLS.

  NB: Nas condições do protocolo entre a Universidade do Minho e a empresa proprietária das VDMTOOLS [Licença académica para uso grátis das VDMTOOLS pelo Departamento de Informática], os enunciados estão escritos em inglês.

Bibliografia essencial

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.

Ol06

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

Bibliografia complementar

F*05

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

Ol95d

J. N. Oliveira.
Métodos Formais de Programação.
Departamento de Informática, Universidade do Minho, 4.� edição, 1998.
489 p. [mfp.zip]

Ol99b

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

Oli00

J.N. Oliveira.
Quasi-inductive datatypes, June 2000.
Departamento de Informática, Universidade do Minho. Chapter of book in preparation.

Provas de Avaliação

Calendário:

Época	Chamada	Data	Hora	Salas	Inscritos	Prova
Normal	1.�	2.�-feira, 8-Jan	09h30	2305, 2306	26	pdf
Normal	2.�	5.�-feira, 25-Jan	14h00	2306	25	pdf
Recurso	-	6.�-feira, 16-Fev	09h30	1315	42	pdf
Especial	-	Sábado, 15 de Setembro de 2007	09h30	1317		pdf

Classificações

[ Informa��o removida (RGPD artigo 17�) ]

Outras disciplinas leccionadas pelo DIUM