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

Novo	Classificações do exame da época especial - ver 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-10h00	T	DI-A2	LMCC/LESI	J.N. Oliveira
2	5.ª-feira	10h00-11h00	T	DI-A2	LESI/LMCC	J.N. Oliveira
3	5.ª-feira	11h00-13h00	TP(2)	DI-A2	LESI/LMCC	L.S. Barbosa
4	6.ª-feira	11h00-13h00	TP(1)	CP2-210	LMCC	L.S. Barbosa

  Atendimento

• Em qualquer altura: via email (jno@di.uminho.pt), devendo ser colocando no assunto o `string' MFP-I/0102; 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
  6.ª-feira	17h00-19h00	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 (Setembro) ou especial (Dezembro) -- 80%
• Avaliação contínua nas aulas laboratoriais -- 20%
• 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 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.

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

• Prototipagem e animação. Ambientes de desenvolvimento formal. Experiência com a utilização do ambiente VDMTOOLS® - for Quality Software on Schedule da IFAD.

• Formalização do modelo relacional da informação. Diagramas UML e sua semântica formal.

  Programa Detalhado

• 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. Ciclo de vida do desenvolvimento formal de `software' . Adopção do `standard' ISO/IEC 13817-1 (VDM-SL).

• Especificação formal construtiva. Modelação de um problema. Prototipagem e animação. Recurso às VDMTOOLS®. Importância da verificação formal das propriedades de um modelo. Técnicas de prova.

  Exemplo: verificação dedutiva da propriedade involutiva da inversão de listas finitas: invl ·invl = id . Papel das propriedades de reflexão-cata e fusão-cata. Propriedade de absorção-cata. Exemplos: prova da igualdade length = sum ·(1)*. Definição de filter p.

• Introdução às 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). Introdução ao conceito de paramorfismo. Exemplos: factorial e `word count'. Propriedades dos paramorfismos. Conversão entre paramorfismos e catamorfismos.

• Introdução aos tipos não indutivos. Invertibilidade à esquerda e à direita. Inequações T <= F T e tipos quasi-indutivos. O tipo quasi-indutivo PA (set of A em VDM-SL) e respectivo morfismo (partes finitas de).

• Propriedades do morfismo partes de. O functor Pf. Extensão, compreensão e filtragem. Notação-ZF. O tipo PA (set of A em VDM-SL)) e esboço de um seu morfismo (card ). O tipo quasi-indutivo função finita A -> B: operadores e propriedades. Relação entre A -> B e A^B: o isomorfismo A -> B =(B+1)^A.

• Teoria de prova associada a um tipo quasi-indutivo. Essência da prova indutiva. Terminação versus indução. Ordens bem-fundadas. Método de indução estrutural. Instâncias do método de indução estrutural - PA, A* e A -> B. Noções de coálgebra bem-fundada. Ordem bem-fundada definida por uma coálgebra bem-fundada. Método de indução polinomial. Derivação dos esquemas de indução associados a diversos tipos indutivos.

• Indução e ponto-fixo. Introdução ao cálculo de pontos-fixos. Funções monótonas, pré/pós-pontos-fixos. Teorema de Tarski. Leis de cálculo, `rolling rule', regra do quadrado, monotonia e regra de indução. Aplicações ao raciocínio sobre tipos indutivos de dados.

• `Case-studies' em especificação formal:
  • Esquemas de conversão de Diagramas ERA (`Entity-Relationship-Attribute') para modelos formais de dados e respectivos invariantes ([Ol95d], pág. 328).
  • Base de dados de produção -- um exemplo de conversão de um diagrama ERA e sua transformação num modelo estruturado de dados.
  • Esboço de uma semântica formal para a linguagem SQL/DDL, expressa em VDM-SL.
  • Conversão de gramáticas independentes de contexto (notação BNF) em sistemas de definições de tipos indutivos e quasi-indutivos ([Ol95d], pág. 104). Regras para a exportação de dados em formato XML.

• Utilização laboratorial das VDMTOOLS®.

  Práticas Laboratoriais

Informação sobre VDMTOOLS® :

• Para aceder 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
  

• A licença u_minho_students4.dat é fornecida nas aulas práticas.

  Material Pedagógico

-

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.

-

No ficheiro mi0102mp.zip encontram-se, até ao momento [data desta versão: 01.12.20]:

Ficheiro «A Brief Introduction to VDM-SL.ppt»

Ficheiro mi0102ln.pdf contendo adenda aos apontamentos (material adicional como paramorfismos, etc)

Ficheiro sql.pdf contendo transparentes sobre esboço de semântica de SQL em VDM-SL.

  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.ª	4.ª-feira, 16 de Janeiro 2002	09h30	2206, 2207	24 + 2	pdf
Normal	2.ª	4.ª-feira, 30 de Janeiro 2002	14h30	2110, 2111	35 + 6	pdf
Recurso	-	6.ª-feira, 6 de Setembro 2002	14h30	...	...	pdf
Especial	-	4.ª-feira, 13 de Novembro 2002	14h00	2203	0+3	pdf

  Classificações

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

Voltar à página principal de MFP-I. Outras disciplinas leccionadas pelo DIUM