 |
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