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

Novo	As notas finais (à data da época especial e após o encerramento da edição 2003/04 da disciplina) estão disponíveis em Classificações

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

  Atendimento

• Em qualquer altura: via email (jno@di.uminho.pt), devendo ser colocando no assunto o `string' MFP-I/0304; 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
  3.ª-feira	08h30-11h30	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ê? Introdução aos binómio especificação /implementação.

• Ciclo de vida usando métodos formais. Redução do risco e dos custos. Áreas típicas de aplicação. Sistemas críticos e confiáveis. Saúde. Qualidade de serviços. Sistemas de informação avançados.

• Linguagens e métodos para especificação formal. Antecendentes históricos. Do método de Viena (VDM) ao `standard' ISO/IEC 13817-1 (VDM-SL).

• Estudo da notação 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. Conexões de Galois.

• Prova de propriedades (invariantes). Obrigações de prova. Métodos de prova. Tipos de dados quase-indutivos. Prova indutiva. Indução estrutural.

• Prototipagem e animação. «Design patterns» e 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

• Especificação formal.
          Introdução à 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' . 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.
• Cálculo de relações.
          Inclusão de relações. Composição e intersecção de relações. Conversa de uma relação. Propriedades. Ordens e sua taxonomia. Formulação de propriedades em notação «pointfree». Exemplo: injectividade da função factorial. Os operadores ker e img. Relações inteiras (totais), sobrejectivas e simples (funcionais). Taxonomia de relações binárias. Estruturação do cálculo relacional com base em conecções de Galois. Propriedades básicas. Exemplos: converso, regras de «shunting», divisão relacional. Intersecção e união. Versões relacionais de <R,S> e [R,S]. Domínio e contradomínio como conecções de Galois. Propriedades.
• Notação VDM-SL.
          Relações em compreensão. Relações simples finitas e sua representação em VDM-SL («mappings»). Significado de uma especificação via pré/pós-condições em VDM-SL. Uso do operador ker f em especificações. 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.
• Especificação indutiva.
          Estratégia de divide-and-conquer e sua representação formal sob a forma de um hilomorfismo relacional. 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. Teorema da fusão-µ. Aplicações.
          Os tipos colectivos de dados em VDM-SL e seus hilomorfismos. O tipo map A to B. O tipo setof A e a notação g. Catamorfismos relacionais. Predicados indutivos vistos como catamorfismos coreflexivos.
          Hilomorfismos com soluções únicas. Noção de acessibilidade e pretença estrutural. Exemplo: acessibilidade sobre sequências. Teorema da hilo-factorização. Estruturas de dados virtuais. Indução estrutural e ordens bem fundadas.
          Definições mutuamente recursivas. Sistemas de definições mutuamente recursivas e sua solução como um catamorfismo. Derivação da lei da recursividade mútua (ou de Fokkinga).
• Polimorfismo paramétrico.
          Porquê e para quê? Teorema «grátis» de um tipo polimórfico t. Operador de Reynolds. Exemplos. Teorema «grátis» do operador catamorfismo de e seus corolários. Leis de fusão e de absorção.
• Prototipagem e animação.
          «Design patterns» e casos de estudo laboratorial. Ambientes de desenvolvimento formal. 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 [04.09.16]:
  • Ficheiros ifmsl.{pdf|ps} - transparentes An Introduction to Formal Modelling
    (22 slides).
  • Ficheiros rfmsl*.{pdf|ps} - transparentes Relational Formal Modelling
    (84 slides).
  • Ficheiros irhsl*.{pdf|ps} - transparentes An Introduction to Relational Hylomorphisms
    (45 slides).
  • Ficheiros tffsl*.{pdf|ps} - transparentes Theorems for Free: an Introduction
    (22 slides).

• 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

Época	Chamada	Data	Hora	Salas	Inscritos	Prova
Normal	1.ª	3.ª-feira, 20 de Janeiro 2004	09h30	2201	25+1	pdf
Normal	2.ª	2.ª-feira, 2 de Fevereiro 2004	14h00	2105	30 + 2	pdf
Recurso	-	4.ª-feira, 18 de Fevereiro 2004	14h00	2301	...	pdf
Especial	-	5.ª-feira, 16 de Setembro 2004	14h00	1211	0+7	pdf

  Classificações

• À data da época especial.
• Todas as classificações negativas (na pauta: Reprovou) são inferiores a 8 (oito) valores.
• Pauta ordenada por CoDisc (código de disciplina) e Nome dos alunos.
  [ Informação removida (RGPD artigo 17º) ]

Voltar à página principal de MFP-I.

Outras disciplinas leccionadas pelo DIUM