U.Minho M�todos Formais de Programa��o I - 2002/03
[ DI/UM ]

Sumários - 2001/2002

J.N. Oliveira 406006

  Aula Te�rica de 02.09.26 [Ref:1]:

Sum�rio: Apresenta��o da disciplina. Equipa docente. Programa da disciplina e seu enquadramento no plano de estudos. Regime de avalia��o. Informa��o electr�nica sobre a disciplina: URL: http://www.di.uminho.pt/~jno/html/mi.html. Bibliografia.

  Aula Te�rica de 02.09.26 [Ref:2]:

Sum�rio: 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. Antevis�o do programa da disciplina:
(a) Adop��o do `standard' ISO/IEC 13817-1 (VDM-SL);
(b) Propriedades, invariantes e obriga��es de prova ;
(c) Tipos colectivos de dados

  Aula Pr�tica de 02.09.26 [Ref:3]:

Sum�rio: Inscri��es.

  Aula Pr�tica de 02.09.26 [Ref:4]:

Sum�rio: Inscri��es.

  Aula Te�rica de 02.10.03 [Ref:1]:

Sum�rio: 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.

  Aula Te�rica de 02.10.03 [Ref:2]:

Sum�rio: 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). [Ol00, pp.79-81] Parcialidade e n�o-determinismo e parcialidade: rela��es versus fun��es.

  Aula Pr�tica de 02.10.03 [Ref:3]:

Sum�rio: (previsto) Introdu��o �s VDMTOOLS�. Exemplo de utiliza��o: modela��o de um sensor de temperatura.

Aula Laboratorial: Ficha 1 (especifica��o vs implementa��o de fun��es)

  Aula Pr�tica de 02.10.04 [Ref:4]:

Sum�rio: (previsto) Introdu��o �s VDMTOOLS�. Exemplo de utiliza��o: modela��o de um sensor de temperatura.

Aula Laboratorial: Ficha 1 (especifica��o vs implementa��o de fun��es)

  Aula Te�rica de 02.10.10 [Ref:1]:

Sum�rio: Opera��es sobre o tipo set of A. Defini��o do morfismo (partes finitas de) como um hilomorfismo. Compreens�o de conjuntos.

  Aula Te�rica de 02.10.10 [Ref:2]:

Sum�rio: 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.

  Aula Pr�tica de 02.10.10 [Ref:3]:

Sum�rio: (previsto) Aula Laboratorial: problema 2 (modela��o com sequ�ncias); problema 3 (modela��o com conjuntos).

  Aula Pr�tica de 02.10.11 [Ref:4]:

Sum�rio: (previsto) Aula Laboratorial: problema 2 (modela��o com sequ�ncias); problema 3 (modela��o com conjuntos).

  Aula Te�rica de 02.10.17 [Ref:1]:

Sum�rio: Não houve aula (dispensa de aulas devida aos festejos acad�micos).

  Aula Te�rica de 02.10.17 [Ref:2]:

Sum�rio: Não houve aula (dispensa de aulas devida aos festejos acad�micos).

  Aula Pr�tica de 02.10.17 [Ref:3]:

Sum�rio: (previsto) Aula Laboratorial: Ficha 4 (invariantes); Ficha 5 (tipos indutivos).

  Aula Pr�tica de 02.10.18 [Ref:4]:

Sum�rio: (previsto) Aula Laboratorial: Ficha 4 (invariantes); Ficha 5 (tipos indutivos).

  Aula Te�rica de 02.10.24 [Ref:1]:

Sum�rio: 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.

  Aula Te�rica de 02.10.24 [Ref:2]:

Sum�rio: Provas de igualdade relacional. Ordens e sua taxonomia. As ordens coreflexivas e a modela��o de predicados.

  Aula Pr�tica de 02.10.24 [Ref:3]:

Sum�rio: (previsto)Exerc�cios teorico-pr�ticos.

  Aula Pr�tica de 02.10.25 [Ref:4]:

Sum�rio: (previsto)Exerc�cios teorico-pr�ticos.

  Aula Te�rica de 02.10.31 [Ref:1]:

Sum�rio: Os operadores ker e img. Sua utiliza��o em especifica��o. Exemplo: isPermutation.

  Aula Te�rica de 02.10.31 [Ref:2]:

Sum�rio: 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.

  Aula Pr�tica de 02.10.31 [Ref:3]:

Sum�rio: (previsto)Exerc�cios teorico-pr�ticos.

  Aula Pr�tica de 02.11.01 [Ref:4]:

Sum�rio: Não houve aula (feriado).

  Aula Te�rica de 02.11.07 [Ref:1]:

Sum�rio: 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.

  Aula Te�rica de 02.11.07 [Ref:2]:

Sum�rio: (previsto) O tipo de dados fun��o parcial finita map A to B e seus operadores b�sicos. Nota��o em compreens�o.

  Aula Pr�tica de 02.11.07 [Ref:3]:

Sum�rio: (previsto)Exerc�cios teorico-pr�ticos.

  Aula Pr�tica de 02.11.07 [Ref:4]:

Sum�rio: (previsto)Exerc�cios teorico-pr�ticos.

  Aula Te�rica de 02.11.14 [Ref:1]:

Sum�rio: Conclus�o da aula anterior.

  Aula Te�rica de 02.11.14 [Ref:2]:

Sum�rio: Diagramas ERA (`Entity-Relationship-Attribute') e sua convers�o para modelos formais de dados baseados em fun��es parciais finitas e respectivos invariantes ([Ol95d], p�g. 328).

  Aula Pr�tica de 02.11.14 [Ref:3]:

Sum�rio: (previsto)Exerc�cios teorico-pr�ticos.

  Aula Pr�tica de 02.11.14 [Ref:4]:

Sum�rio: (previsto)Exerc�cios teorico-pr�ticos.

  Aula Te�rica de 02.11.21 [Ref:1]:

Sum�rio: Conclus�o da aula anterior.

  Aula Te�rica de 02.11.21 [Ref:2]:

Sum�rio: In�cio do estudo de formaliza��o dos morfismos associados aos tipos quasi-indutivos PA e (set of A em VDM-SL).

  Aula Pr�tica de 02.11.21 [Ref:3]:

: Exerc�cios teorico-pr�ticos. Sum�rio(previsto)
  de 02.11.21 [Ref:4]: Aula Pr�tica
: Exerc�cios teorico-pr�ticos. Sum�rio(previsto)
  de 02.11.28 [Ref:1]: Aula Te�rica
: 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). Sum�rio
  de 02.11.28 [Ref:2]: Aula Te�rica
: Fun��es mon�tonas, pr�/p�s-pontos-fixos. Teorema de Tarski. Nota��o . Sum�rioIntrodu��o ao c�lculo de pontos-fixos :�
  de 02.11.28 [Ref:3]: Aula Pr�tica
: Exerc�cios teorico-pr�ticos. Sum�rio(previsto)
  de 02.11.28 [Ref:4]: Aula Pr�tica
: Exerc�cios teorico-pr�ticos. Sum�rio(previsto)
  de 02.12.05 [Ref:1]: Aula Te�rica
: Aplica��o � defini��o indutiva de um tipos de dados com ponto fixo de um functor polinomial . Unicidade do catamorfismo associado. Sum�rioC�lculo de pontos-fixos :�FF
  de 02.12.05 [Ref:2]: Aula Te�rica
: 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. Sum�rio
  de 02.12.05 [Ref:3]: Aula Pr�tica
: Exerc�cios teorico-pr�ticos. Sum�rio(previsto)
  de 02.12.05 [Ref:4]: Aula Pr�tica
: Exerc�cios teorico-pr�ticos. Sum�rio(previsto)
  de 02.12.12 [Ref:1]: Aula Te�rica
: Propriedades de e e sua utilidade na prova construtiva de propriedades. Exemplo: verifica��o da propriedade involutiva da invers�o de listas finitas, . Propriedade de . Exemplo: prova da igualdade . Sum�rioC�lculo de catamorfismos :reflex�o-catafus�o-cata invl �invl = id absor��o-catalength = sum �()*1
  de 02.12.12 [Ref:2]: Aula Te�rica
: 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. Sum�rio
  de 02.12.12 [Ref:3]: Aula Pr�tica
: Exerc�cios teorico-pr�ticos. Sum�rio(previsto)
  de 02.12.05 [Ref:4]: Aula Pr�tica
: Exerc�cios teorico-pr�ticos. Sum�rio(previsto)
  de 02.12.12 [Ref:1]: Aula Te�rica
: Esquemas recursivos 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 ). Preenchimento do question�rio de avalia��o. Sum�rioFokkinga
  de 02.12.19 [Ref:2]: Aula Te�rica
: No��o de paramorfismo e suas propriedades. Exemplos. S�ntese final. Encerramento da disciplina. Sum�rio
  de 02.12.19 [Ref:3]: Aula Pr�tica
: Exerc�cios teorico-pr�ticos. Sum�rio(previsto)
  de 02.12.19 [Ref:4]: Aula Pr�tica
: Exerc�cios teorico-pr�ticos. Sum�rio(previsto)


jno 2003-01-06