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

[ Equipa docente | Horário | Atendimento | Regime de Avaliação | Sumários
Programa Resumido | Programa Detalhado | Material Pedagógico
Bibliografia | Provas de Avaliação | Notas Finais ]

  Equipa docente

• Teóricas -- J.N. Oliveira (406006)
• Teórico-práticas -- F.L. Neves (406085)

  Horário

Ref.	Dia	Hora	Tipo	Sala	Cursos	Docente
1	4.ª-feira	09h00-11h00	TP(1)	DI-1.07	LMCC/LESI	F.L. Neves
2	5.ª-feira	09h00-10h00	T	DI-A2	LMCC/LESI	J.N. Oliveira
3	5.ª-feira	10h00-11h00	T	DI-A2	LESI/LMCC	J.N. Oliveira
4	6.ª-feira	15h00-17h00	TP(2)	DI-A2	LESI/LMCC	F.L. Neves

  Atendimento

• Em qualquer altura: via email (jno@di.uminho.pt), devendo ser colocando no assunto o `string' MFP-I/0001; 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	12h00-13h00	LESI+LMCC	J.N. Oliveira
  4.ª-feira	11h00-13h00	LESI+LMCC	F.L. Neves

  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 E-R e sua semântica.

  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 aos binómio especificação /implementação.

  Introdução às VDMTOOLS® . Início do estudo da linguagem de especificação `standard' ISO/IEC 13817-1 (VDM-SL).

• Definição de tipos de dados. Introdução ao conceito de invariante de um tipo de dados. Álgebra de produto. Construtores mk_ e selectores. Predicados is_ e sua relação com construtores mk_. O tipo [ A ]. Tipos indutivos e seus morfismos (revisão de MP-I). O tipo A (seq of A em VDM-SL)).

• Introdução aos tipos não indutivos. O tipo PA (set of A em VDM-SL)) e esboço de um seu morfismo (card ). 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).

• Operadores sobre PA. O functor Pf. Extensão, compreensão e filtragem. Notação-ZF. Conjuntos de pares ou relações binárias: P(A × B). Domínio e codomínio de uma relação binária. Relações parciais, injectivas, sobrejectivas e funcionais. Composição de relações e transitividade. Ordens. Pré-ordens, ordens parciais e relações de equivalência. O tipo quasi-indutivo função finita A -> B (map A to B em VDM-SL) e seus operadores. Propriedades. Relação entre A -> B e A^B: o isomorfismo A -> B =(B+1)^A.

• Introdução ao estudo do meta-modelo de dados do modelo relacional da informação como exemplo de modelação com funções finitas e conjuntos:

  Base_de_Dados = map Id to Tabela;
  Tabela = set of Tuplo;
  Tuplo = map Atributo to Valor;

  e sua evolução para

  Tabela = map Tuplo to Tuplo

• Introdução à noção de argumento formal (prova) sobre um modelo formal. Propriedades de um tipo de dados. Invariantes. Obrigações de prova inerentes à preservação de propriedades invariantes. "Normware". Prova de propiedades invariantes num modelo. Introdução aos métodos indutivos de prova. Método de indução associado a um tipo indutivo. Exemplos: o tipo X =1 + X e a indução natural. Indução sobre sequências finitas. Método de indução polinomial.

• Propriedade universal-cata e suas derivadas: cancelamento-cata e reflexão-cata. derivação da lei de fusão-cata. Lei de absorção-cata.

• Teoria de prova associada a um tipo quasi-indutivo. Noções de ordem e de coálgebra bem-fundadas. Essência da prova indutiva. Terminação versus indução. Método de indução estrutural.

• Esquemas de conversão de Diagramas ERA (`Entity-Relationship-Attribute') para modelos formais de dados e respectivos invariantes. Exemplo de conversão de um diagrama ERA e sua transformação num modelo estruturado de dados.

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

  Material Pedagógico

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

  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_pdf.zip]

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, 10 de Janeiro 2001	09h30	2204 e 2205	75 + 6	pdf.gz
Normal	2.ª	4.ª-feira, 24 de Janeiro de 2001	09h30	2312	...	pdf.gz
Recurso	-	4.ª-feira, 5 de Setembro 2001	14h30	2206	28	pdf.gz
Especial	-	Sábado, 24 de Novembro 2001	09h30	2107	5	pdf.gz

  Notas Finais

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

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