Métodos Formais de Programação I - 2005/06
[ 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
Programa Resumido | Programa Detalhado | Práticas Laboratoriais
| Material Pedagógico
Bibliografia | 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	4.ª-feira	09h00-10h00	TP(1)	DI-0.11	LESI/LMCC	L.S. Barbosa
2	5.ª-feira	09h00-11h00	T	DI-A2	LMCC/LESI	J.N. Oliveira
3	5.ª-feira	14h00-16h00	TP(2)	DI-0.11	LESI/LMCC	L.S. Barbosa

  Atendimento

• Em qualquer altura: via e-mail, devendo ser colocando no assunto o `string' MFP-I/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
  5.ª-feira	13h00-14h00	LESI+LMCC	J.N. Oliveira
  4.ª-feira	11h00-13h00	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 laboratoriais -- 20%

  Sumários

• Teóricas e Práticas

  Programa Resumido

• Introdução ao problema do controlo de qualidade em `software' . Especificação formal -- porquê e para quê?

• Ciclo de vida usando métodos formais. Redução do risco e dos custos.

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

• Introdução ao cálculo relacional. 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''.

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

• 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.

• 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.

• 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 IFAD.

  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. Preservação de um invariante por uma função. Preservação de um invariante por um par pré/pós-condição Spec = (pre,post) em VDM-SL. Noção de precondição mais fraca que garante uma propriedade. Noção de propriedade como tipo. Noção de invariante como tipo. Polimorfismo orientado à propriedade. Algumas regras da combinação de especificações que satisfazem propriedades: identidade, composição, inclusão.

• 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 VDMTOOLS - for Quality Software on Schedule da IFAD.

  Práticas Laboratoriais

Informação sobre VDMTOOLS :

• Acesso aos executáveis: ftp://ftp.di.uminho.pt/pub/di/VDMTools/

• Script de configuração (adaptar!):

  VDMSLROOT=/home/lsb/vdmhome
  LM_LICENSE_FILE=/home/lsb/vdmhome/u_minho_students4.dat
  PATH=$PATH:/home/lsb/vdmhome
  export VDMSLROOT LM_LICENSE_FILE PATH
  

• O ficheiro u_minho_students4.dat é fornecido nas aulas práticas.

  Material Pedagógico

• Em ficheiro zip encontram-se, até à data desta versão [05.12.18]:

  

  Ficheiro mi0506su+adenda.pdf - sumários completos com anexo

  

  Ficheiros ifmsl.{pdf|ps} - transparentes An Introduction to Formal Modelling
  (22 slides).

  

  Ficheiros rfmsl*.{pdf|ps} - transparentes Relational Formal Modelling
  (84 slides).

  

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

  

  Ficheiro rel.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 IFAD [Licença académica para uso grátis das VDMTOOLS pelo Departamento de Informática], os enunciados estão escritos em inglês.

  Bibliografia

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.

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.ª	4.ª-feira, 25 de Janeiro 2006	14h00	2111	16	pdf
Normal	2.ª	Sábado, 04 de Fevereiro 2006	09h30	1301-1302	27+2	pdf
Recurso	-	6.ª-feira, 17 de Fevereiro 2006	09h30	2210		pdf
Especial	-	3.ª-feira, 3 de Outubro de 2006	10h00	3101		pdf

  Classificações

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

Voltar à página principal de MFP-I.

Outras disciplinas leccionadas pelo DIUM