SumáriosAulas

T (2004.09.23): Apresentação da Disciplina. Introdução aos métodos formais de especificação e desenvolvimento de software. O binómio especificação-implementação. Objectivos e programa da disciplina; sua integração no plano curricular do curso.

TP (2004.09.22): Apresentação: marcação de turnos.

TP (2004.09.22): Apresentação: marcação de turnos.

T (2004.09.30): Motivação para a especificação relacional. Introdução ao Cálculo Relacional. Operadores básicos e propriedades.

TP (2004.09.29): Apresentação do VDMTools. Resolução do problema 02 do guião das sessões de laboratório(Modelling with Sequences).

TP (2004.09.30): Apresentação do VDMTools. Resolução do problema 02 do guião das sessões de laboratório (Modelling with Sequences).

T (2004.10.07): Cálculo Relacional: Lei modular; técnicas de prova; exemplos.

TP (2004.10.06): Resolução do problema 03 dos guiões (Modelling with Sets).

TP (2004.10.07): Resolução do problema 03 dos guiões (Modelling with Sets).

T (2004.10.14): Dispensa de aulas concedida pelo Senhor Reitor

TP (2004.10.13): Resolução do problema 06 dos guiões (Modelling with Mappings).

TP (2004.10.14): Resolução do problema 06 dos guiões (Modelling with Mappings).

T (2004.10.21): Raciocínio com funções: regras de shunting; especialização de leis. Conexões de Galois: motivação, definição e exemplos. Propriedades básicas associadas a uma conexão de Galois. Prova da preservação de supremos (infimos) pelo adjunto inferior (superior).

TP (2004.10.20): Resolução do problema 07 dos guiões (Multisets "are" Mappings).

TP (2004.10.21): Resolução do problema 07 dos guiões (Multisets "are" Mappings).

T (2004.10.28): Continuação da aula anterior: análise de diversos exemplos de conexões de Galois e derivação de propriedades. Noção de either e split relacionais.

TP (2004.10.27): Resolução da Ficha 1 (Cálculo Relacional).

TP (2004.10.28): Resolução da Ficha 1 (Cálculo Relacional).

T (2004.11.04): Faltou o docente (por deslocação em serviço). Em substituição foi dada uma aula TP a cargo da Prof. Olga Pacheco.

TP (2004.11.03): Resolução da Ficha 2 (Cálculo Relacional).Resolução do problema 04 dos guiões (Datatype Invariants).

TP (2004.11.04): Resolução da Ficha 2 (Cálculo Relacional).Resolução do problema 04 dos guiões (Datatype Invariants).

T (2004.11.11): Semântica relacional da meta-linguagem de VDM. Definição recursiva de relações. Noção de hilomorfismo relacional. Incursão na semântica das definições recursivas. Teorema de Knaster-Tarski.

TP (2004.11.10): Faltou a docente (deslocação em serviço).

TP (2004.11.11): Faltou a docente (deslocação em serviço).

T (2004.11.18): Faltou o docente (deslocação em serviço).

Esta aula será reposta no dia 14 Dez (terça-feira) pelas 14.30 h.

TP (2004.11.17): Faltou a docente. (Aula de substituição).

TP (2004.11.18): Faltou a docente. (Aula de substituição).

T (2004.11.25): Cálculo de pontos fixos. Leis básicas e exemplos. Aplicação ao cálculo de hilomorfismos relacionais.

TP (2004.11.24): Resolução da Ficha 3 (Conexões de Galois).Resolução do problema 09 dos guiões (A Toy Production Database model).

TP (2004.11.25): Resolução da Ficha 3 (Conexões de Galois).Resolução do problema 09 dos guiões (A Toy Production Database model).

T (2004.12.02): Propriedades dos hilomorfismos relacionais. Aplicação ao estudo dos tipos colectivos (não indutivos) de VDM (conjuntos e corresponências).

TP (2004.12.01): Feriado Nacional.

TP (2004.12.02): Resolução da Ficha 4 (Conexões de Galois). Continuação da resolução do problema 09 dos guiões.

T (2004.12.09): Relação de acessibilidade e pertença em tipos de dados. Factorização em equações-hilo. Condições para a existência de soluções únicas. Aplicações.

TP (2004.12.08): Feriado Nacional.

TP (2004.12.09): (Aulas de dúvidas)

T (2004.12.14): (Reposição aula de 18 Nov) Discussão de exercícios de aplicação.

T (2004.12.16): Conclusão da disciplina. Preenchimento do questionário de avaliação.

TP (2004.12.15): (Aulas de dúvidas)

TP (2004.12.16): (Aulas de dúvidas)

-- LuisSoaresBarbosa - 21 Sep 2004

Métodos Formais de Programação I

2004-2005

Equipa Docente

Horários

Tipo Horário Sala
T 5as: 09-11 h DI A2
TP (Turno 1) 4as: 09-11 h DI 0.11
TP (Turno 2) 5as: 14-16 h DI 0.11

Horários de Atendimento

Docente Horário
Luís S. Barbosa 5as 13-14
Olga Pacheco 3as 15-16 e 6as 11-12

Nota: o contacto com os docentes através de email deve ser sempre feito a partir de contas institucionais da Universidade e com a indicação clara do nome da disciplina no subject.

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 do software usando métodos formais. Redução do risco e dos custos. Áreas típicas de aplicação. Sistemas críticos e confiáveis. Qualidade de serviços.
  • 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).
  • Prototipagem e animação. Experiência com a utilização do ambiente VDMTOOLS.
  • Introdução ao cálculo relacional. Combinadores relacionais básicos. Taxonomia de relações binárias. Conexões de Galois. Pontos fixos.
  • Semântica relacional para VDM-SL e cálculo de especificações.

Critérios de Avaliação

  • Nota final
    • Componente Teórica (Exame): 80% (nota mínima de 8 valores)
    • Componente Prática: 20% em avaliação contínua e entrega de relatórios das aulas laboratoriais (nota mínima de 10 valores)
    • Recorda-se que o estatuto de Trabalhador-Estudante não isenta os alunos nessas condições da obrigatoriedade de realizar a componente experimental da disciplina.

Provas de Avaliação

  • 05.02.21 - 1a Ch (com correcção parcial) (pdf)
  • 05.02.02 - 2a Ch (com correcção parcial) (pdf)

Acetatos e Textos de Apoio

  • Formal Methods in Software Engineering (slides)
  • no ficheiro slides encontram-se cópias dos acetatos utilizados nas aulas teóricas:
    • Ficheiros ifmsl.{pdf|ps} - An Introduction to Formal Modelling (22 slides).
    • Ficheiros rfmsl*.{pdf|ps} - Relational Formal Modelling (84 slides).
    • Ficheiros irhsl*.{pdf|ps} - An Introduction to Relational Hylomorphisms (45 slides).
    • Ficheiros tffsl*.{pdf|ps} - Theorems for Free: an Introduction (22 slides).
  • Guião das sessões de laboratório sobre VDMTOOLS.
  • Aqui encontra-se a resolução de um dos exercícios discutidos na aula de 14 Dez.
  • Formulário com leis do Cálculo Relacional.
  • Formulário com leis do Cálculo Funcional.

Aulas Práticas

  • Fichas

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

VDMSLROOT=/home/your_account/vdmhome

LM_LICENSE_FILE=/home/your_account/vdmhome/u_minho_students4.dat

PATH=$PATH:/home/your_account/vdmhome

export VDMSLROOT LM_LICENSE_FILE PATH

Bibliografia

Classificações Exame (Época Normal)

Nr Nome Exame Recurso Laboratório NOTA FINAL
35803 Alexandra Martins Silva 19   18 19
30969 Alexandre Soares Barbosa R 8.5 14 10
28141 Arnaldino Pinto Faltou   10  
30706 Carla Sofia Carmo R   15  
35810 Carlos Moutinho Machado 13 15 17 16
32220 Carlos Manuel Pereira Faltou D 14  
30711 Dário Samico Faltou   15  
35803 Jácome Miguel Cunha 12   17 13
30655 Joana Teresa Neves Faltou   15  
28156 Jorge Soares Lima 10   10 10
  Leonel Mendonça Faltou   10  
17092 Lígia Rodrigues Teixeira 10   10 10
30662 Luís Miguel Neiva Ferros 14   14 14
25371 Luís Pedro Gomes R 11.5 10 12
29016 Marco Paulo Martins Cruz 10   14 11
26327 Maria Inês Campos Faltou   10  
30743 Maria Madalena Varzim Faria 10   15 11
28171 Marlene Silva Amorim R 9 15 10
23198 Marta Carneiro Silva R R 10  
33723 Miguel Angelo Duarte Faltou   10  
33724 Miguel Henrique Fernandes 13   17 14
23203 Paulo Alexandre Afonso Dias D R 10  
35856 Pedro Gonçalves Silva R 11.5 15 12
30748 Pedro Rui Dinis Silva Faltou   14  
24870 Pedro Silva Faltou   10  
28179 Raquel Couto Pires R Oral: 10 10 10
33730 Ricardo Pinheiro Faltou   15  
20225 Ricardo Gaspar Paz R 8.5 Sem Informação Contactar Docente
30752 Rogério Leite Costa R D 14  
20232 Sandrina Maciel Faltou   10  
23218 Susana Morais Pacheco R R 10  
20838 Vitor Sá Pereira R   14  
25403 Wagner Barretoo Faria Faltou   15  

-- LuisSoaresBarbosa - 4 Mar 2005