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

Novo	Classificações (época especial)

[ 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 | [NOVO] Classificações ]

  Equipa docente

• Teóricas -- J.N. Oliveira (406006)
• Teórico-práticas -- (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

  Atendimento

• Em qualquer altura: via email (), devendo ser colocando no assunto o `string' MFP-I/0203; 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	tabular

  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.

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

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

  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.
• 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. Técnicas de prova.

• Introdução aos tipos colectivos de dados. Tipos não indutivos. Invertibilidade à esquerda e à direita. Inequações T <= F T e tipos quasi-indutivos. Conjuntos: introdução ao tipo quasi-indutivo PA (set of A em VDM-SL). Não-determinismo e parcialidade: relações versus funções. Operações sobre o tipo set of A. Definição do morfismo (partes finitas de) como um hilomorfismo. Compreensão de conjuntos.

• Introdução à especificação formal por pares pré/pós-condições. Necessidade de estender funções a relações: não-determinismo e parcialidade. Sub-especificação.

• Introdução ao cálculo de relações. Inclusão de relações. Composição e intersecção de relações. Conversa de uma relação. Propriedades. Provas de igualdade relacional. Ordens e sua taxonomia. As ordens coreflexivas e a modelação de predicados. Os operadores ker e img. Sua utilização em especificação. Exemplo: isPermutation. Taxonomia de relações binárias. Relações inteiras (totais), sobrejectivas e simples (funcionais) Significado de uma especificação constituída por pares-pre/post.

• As relações finitas como estruturas de dados: set of (A * B). Notação e operadores. Notação em compreensão. Relações binárias finitas com uma dependência funcional. O tipo de dados função parcial finita map A to B e seus operadores básicos. Notação em compreensão. Estudo de formalização dos morfismos associados aos tipos quasi-indutivos PA e (set of A em VDM-SL). Noção de hilomorfismo relacional. Relacionadores versus functores. Factorização de um hilomorfismo relacional através do tipo indutivo associado (ponto-fixo do respectivo relacionador de base).

• Cálculo de pontos-fixos : Funções monótonas, pré/pós-pontos-fixos. Teorema de Tarski. Notação µ. Aplicação à definição indutiva de um tipos de dados com ponto fixo µF de um functor polinomial F. Unicidade do catamorfismo associado. Hilomorfismos como pontos fixos de equações relacionais. Teorema da factorização-hilo. Aplicação aos morfismos de conjuntos e funções finitas. Terminação versus indução. Ordens bem-fundadas. Propriedades de reflexão-cata e fusão-cata e sua utilidade na prova construtiva de propriedades. Exemplo: verificação da propriedade involutiva da inversão de listas finitas, invl ·invl = id . Propriedade de absorção-cata. Exemplo: prova da igualdade length = sum ·(1)*. Hilomorfismos como pontos fixos de equações relacionais. Teorema da factorização-hilo. Aplicação aos morfismos de conjuntos e funções finitas. Terminação versus indução. 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). Preenchimento do questionário de avaliação. Noção de paramorfismo e suas propriedades. Exemplos.

• Diagramas ERA (`Entity-Relationship-Attribute') e sua conversão para modelos formais de dados baseados em funções parciais finitas e respectivos invariantes.

  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_students5.dat
  PATH=$PATH:/home/lsb/vdmhome
  export VDMSLROOT LM_LICENSE_FILE PATH
  

• O ficheiro u_minho_students5.dat é fornecido 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 mi0203mp.zip encontram-se, até ao momento [data desta versão: 03.01.15]:

Ficheiro mi0203ln1.pdf - transparentes An Introduction to Formal Modelling.

Ficheiro mi0203ln2.pdf - transparentes Relational Formal Modelling.

Ficheiro mi0203ln3.pdf - transparentes An Introduction to Relational Hylomorphisms.

Ficheiro mi0203ln4.pdf - adenda aos apontamentos (pontos-fixos, recursividade múltipla, paramorfismos).

Ficheiro _.pdf - extensão de mi0203ln2.pdf com demonstrações.

Ficheiro ercook.pdf - transparentes ERA diagram semantics in VDM-SL.

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

Ficheiro rel.pdf - contendo tabela de leis de cálculo relacional.

  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

• Período de exames: 2003.01.06 a 2003.02.22.
• Lançamento das notas no livro de termos: 2003.03.05
• Calendário:

  Época	Chamada	Data	Hora	Salas	Inscritos	Prova
  Normal	1.ª	5.ª-feira, 16 de Janeiro 2003	14h00	2111	24+0	pdf
  Normal	2.ª	6.ª-feira, 31 de Janeiro 2003	14h00	2110,2111	37 + 10	pdf
  Recurso	-	6.ª-feira, 21 de Fevereiro 2003	9h30	2302	...	pdf
  Especial	-	[NOVO] 3.ª-feira, 9 de Setembro 2003	14h00	1301	1+10	...

• Alunos inscritos por chamadas.

  Classificações

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

Voltar à página principal de MFP-I.

Outras disciplinas leccionadas pelo DIUM