 |
Métodos Formais de Programação I - 1998/99
|
[ DI/UM ]
|
---|
Ref. |
Dia |
Hora |
Tipo |
Sala |
Cursos |
Docente |
1 |
3.ª-feira |
11h00-13h00 |
TP(1) |
DI/2 |
LMCC |
F.L. Neves |
2 |
4.ª-feira |
11h00-13h00 |
T |
C2/321 |
LMCC/LESI |
J.N. Oliveira |
3 |
4.ª-feira |
14h00-16h00 |
TP(1) |
DI/2 |
LESI |
F.L. Neves |
4 |
6.ª-feira |
11h00-13h00 |
TP(2) |
DI/2 |
LESI |
F.L. Neves |
- Em qualquer altura: via email (jno@di.uminho.pt
),
devendo ser colocando no assunto o 'string' MFP-I/9899;
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:
-
Nota teórica, por prova escrita,
de acordo com regulamentação interna em vigor - épocas
normal (1.ª ou 2.ª chamada),
de recurso (Setembro) ou
especial (Dezembro).
-
Os alunos só poderão fazer melhoria de nota na época de recurso.
-
Métodos Formais
- apresentação do conceito e dos
seus antecendentes históricos.
Ciclo de vida do desenvolvimento de software
baseado em Métodos Formais
.
-
Iniciação à teoria dos modelos.
Noções básicas de teoria das categorias úteis em
especificação formal.
Modelos primitivos e derivados.
Propriedades de reflexão, fusão, absorção e cancelamento.
Lei da troca.
-
Parametrização e polimorfismo.
Tipos de dados «são» functores.
Morfismos entre tipos de dados (functores).
Transformações naturais e seus teoremas grátis! .
-
Introdução à especificação recursiva.
Noção de ponto fixo.
Ordens parciais. Cpos. Recticulados. Teoremas de Tarski e de Kleene.
Pontos fixos em Set.
Introdução ao cálculo de isomorfismos.
-
Conversão de gramáticas independentes de
contexto em equações polinomiais.
Recursividade polinomial.
-
Tipos de dados indutivos.
Álgebras de functores.
Esquemas de funcionalidade recursiva:
Catamorfismos, anamorfismos e hilomorfismos.
Functores de tipo.
-
Introdução
-
Métodos Formais
- apresentação do conceito e dos
seus antecendentes históricos.
-
Ciclo de vida do desenvolvimento de sistemas de software
baseado em Métodos Formais
.
-
Iniciação à teoria dos modelos
-
Noções básicas de teoria de conjuntos úteis na
especificação formal de um programa
-
Modelos primitivos:
a categoria Set e seu produto, coproduto e exponenciação.
Objectos iniciais e terminais.
Propriedades de reflexão, fusão, absorção e cancelamento.
Lei da troca.
-
Modelos derivados:
sequências, (sub)conjuntos e funções parciais finitas.
-
Tipos de dados «são» functores.
Noção de functor. Functores polinomais.
-
Transformações entre tipos de dados (functores).
Parametrização e polimorfismo.
Transformações naturais e seus teoremas grátis! .
Método Hindley-Milner para inferência de tipos.
-
Introdução à especificação recursiva
-
Noção de ponto fixo.
Ordens parciais. Cpos. Recticulados. Teoremas de Tarski e de Kleene.
-
Determinação de soluções de equações em Set.
Pontos fixos em Set.
-
Introdução ao cálculo de isomorfismos.
-
Conversão de gramáticas independentes de
contexto em equações polinomiais.
Recursividade polinomial.
-
Tipos de dados indutivos.
-
Álgebras de functores.
Álgebras iniciais e terminais.
-
Esquemas de funcionalidade recursiva:
Catamorfismos, anamorfismos e hilomorfismos.
Politipismo.
Propriedades de reflexão, fusão, absorção e cancelamento.
Functores de tipo.
-
Esquemas funcionais dos modelos derivados.
- BdM97
-
R. Bird and O. de Moor.
Algebra of Programming
.
Series in Computer Science. Prentice-Hall International, 1997.
C. A. R. Hoare, series editor.
- 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.
University of Minho, 4th edition, 1997.
Textbook (489 p. in Portuguese [available as a 846K
gzipped
PS file]). English version under preparation at the time of
writing.
- Oli98
-
J. N. Oliveira.
A data structuring calculus and its application to program
development, May 1998.
Lecture Notes (150 p. [available as a 390K
gzipped
PS file]).
Departamento de Informatica, Facultad de Ciencias Fisico-Matematicas y
Naturales, Universidad de San Luis,
Argentina.
-
Apontamentos auxiliares para a disciplina:
ou ambos os ficheiros em formato *.tar.gz: 137876
bytes.
-
Procure aqui
se estiver interessado em obter módulos CAMILA
que
apoiam a matéria da disciplina.
- Época Normal
- 1.ª chamada - 29 de Janeiro 1999, 09h30, Salas 2319 e 2320 -
Prova
(incluindo correcção)
- 2.ª chamada - 15 de Fevereiro 1999, 14h30, Sala 2211 -
Prova
- Época de Recurso - 8 de Setembro de 1999, 14h30, Sala 2304 -
Prova
Observações:
- À data da Época de Recurso.
- A pauta está 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
1/31/2000
Jose Nuno Oliveira