| M�todos Formais de Programa��o II - 2000/01 |
|---|---|
| [ DI/UM ] |
| Aula Pr�tica de 2001.02.12 [Ref:1]: |
Sum�rio: Revis�o de M.F.P.-I: M�todos indutivos de prova. Indu��o natural ( Nat0 =1 + Nat0) e indu��o sobre sequ�ncias (A* =1 + A � A*). Resolu��o dos exerc�cios 3.3, 3.4 e 3.5.
Aula Te�rica de 2001.02.14 [Ref:2]:
Sum�rio: Apresenta��o da disciplina. Equipa docente. Programa da disciplina e seu enquadramento no plano de estudos. Regime de avalia��o. Bibliografia.
Informa��o electr�nica sobre a disciplina: www.di.uminho.pt/~jno/html/mii.html.
Introdu��o �s t�cnicas de refinamento (reifica��o) de especifica��es formais. Antecendentes hist�ricos.
Aula Pr�tica de 2001.02.14 [Ref:3]:
Sum�rio: M�todos indutivos de prova. Indu��o natural ( Nat0 =1 + Nat0) e indu��o sobre sequ�ncias (A* =1 + A � A*). Resolu��o dos exerc�cios 3.3, 3.4 e 3.5.
Aula Pr�tica de 2001.02.19 [Ref:1]:
Sum�rio: Resolu��o dos exerc�cios 3.3, 3.4 e 3.5 (cont.). M�todos indutivos de prova. Indu��o sobre conjuntos (PA <=1 + A � PA). Resolu��o de exerc�cios.
Aula Te�rica de 2001.02.21 [Ref:2]:
Sum�rio: Introdu��o �s t�cnicas de refinamento (cont.) : Valida��o vs verifica��o formal. Verifica��o est�tica vs din�mica. Sem�ntica denotacional de linguagens de programa��o. O porqu� da programa��o estruturada. Verifica��o vs c�lculo de programas.
Aula Pr�tica de 2001.02.21 [Ref:3]:
Sum�rio: Resolu��o dos exerc�cios 3.3, 3.4 e 3.5 (cont.). M�todos indutivos de prova. Indu��o sobre conjuntos (PA <=1 + A � PA). Resolu��o de exerc�cios.
Aula Pr�tica de 2001.02.26 [Ref:1]:
Sum�rio: Rela��es bin�rias e fun��es finitas. Resolu��o de exerc�cios: defini��o das fun��es dom, rng, A -> f, |s, , pap e ++ sob a forma de morfismos sobre A -> B. Resolu��o dos exerc�cios 3.7 e 3.8.
Aula Te�rica de 2001.02.28 [Ref:2]:
Sum�rio: Introdu��o �s t�cnicas de refinamento (cont.) : Especifica��o directa e reversa. Compreens�o de programas. Exemplo de an�lise de um programa em C++ e conjectura da sua especifica��o formal recorrendo a catamorfismos.
Aula Pr�tica de 2001.02.28 [Ref:3]:
Sum�rio: Rela��es bin�rias e fun��es finitas. Resolu��o de exerc�cios: defini��o das fun��es dom, rng, A -> f, |s, , pap e ++ sob a forma de morfismos sobre A -> B. Resolu��o dos exerc�cios 3.7 e 3.8.
Aula Pr�tica de 2001.03.05 [Ref:1]:
Sum�rio: Combina��o de fun��es mutuamente dependentes. A lei de Fokkinga. A lei de Banana-Split. Resolu��o de exerc�cios.
Aula Te�rica de 2001.03.07 [Ref:2]:
Sum�rio: T�cnicas de refinamento algor�tmico : Leis de fus�o �horizontal� de processos algor�tmicos. Lei da recursividade m�tua de Fokkinga. Lei de �banana-split� e sua utiliza��o na intercombina��o de ciclos. Elimina��o de estruturas de dados interm�dias (�desfloresta��o�).
Aula Pr�tica de 2001.03.07 [Ref:3]:
Sum�rio: Combina��o de fun��es mutuamente dependentes. A lei de Fokkinga. A lei de Banana-Split. Resolu��o de exerc�cios.
Aula Pr�tica de 2001.03.12 [Ref:1]:
Sum�rio: Não houve aula (participa��o do docente em congresso internacional).
Aula Te�rica de 2001.03.14 [Ref:2]:
Sum�rio: Não houve aula (participa��o do docente em congresso internacional).
Aula Pr�tica de 2001.03.14 [Ref:3]:
Sum�rio: Não houve aula (participa��o do docente em congresso internacional).
Aula Pr�tica de 2001.03.19 [Ref:1]:
Sum�rio: Aula laboratorial. Defini��o das fun��es dom, rng, A -> f, |s, , pap e ++, escritas sob a forma de morfismos sobre A -> B, em VDM-SL.
Aula Te�rica de 2001.03.21 [Ref:2]:
Sum�rio: T�cnicas de refinamento algor�tmico : Leis de fus�o �vertical� de processos algor�tmicos (leis functoriais, de fus�o e de absor��o).
Introdu��o �s t�cnicas de refinamento dos dados : Transforma��es isomorfas. Transforma��es sobrejectivas e injectivas. Invertibilidade � direita e � esquerda. No��es de abstrac��o e de representa��o. Inequa��es da forma A <=B . Exemplos. Diagramas de refinamento de opera��es. Abstra��o dos argumentos e representa��o dos resultados. Esquema de s�ntese de uma implementa��o como solu��o de um diagrama de refinamento.
Aula Pr�tica de 2001.03.21 [Ref:3]:
Sum�rio: Aula laboratorial. Defini��o das fun��es dom, rng, A -> f, |s, , pap e ++, escritas sob a forma de morfismos sobre A -> B, em VDM-SL.
Aula Pr�tica de 2001.03.26 [Ref:1]:
Sum�rio: Aula laboratorial. Defini��o, em VDM-SL, de fun��es param�tricas que permitem realizar catamorfismos e anamorfismos sobre A*.
Aula Te�rica de 2001.03.28 [Ref:2]:
Sum�rio: Refinamento formal de dados : Propriedades da rela��o A <=B: reflexividade, transitividade e monotonicidade.
Leis de representa��o (ou de refinamento) envolvendo tipos de dados quasi-indutivos (PA e A -> B):
PA =A -> 1
0 -> A =1
1 -> A =1 + A
(C+B) -> A =(C -> A) � (B -> A)
Aula Pr�tica de 2001.03.28 [Ref:3]:
Sum�rio: Aula laboratorial. Defini��o, em VDM-SL, de fun��es param�tricas que permitem realizar catamorfismos e anamorfismos sobre A*.
Aula Pr�tica de 2001.04.02 [Ref:1]:
Sum�rio: C�lculo de simula��es. Resolu��o de exerc�cios: simula��o de ina e de card. Refinamento algor�tmico. Algoritmos de pesquisa e sua efici�ncia. Padr�es de recursividade lineares vs bi-lineares. Resolu��o de exerc�cios: altera��o do padr�o de recursividade da fun��o belongsa.
Aula Te�rica de 2001.04.04 [Ref:2]:
Sum�rio: Refinamento formal de dados (cont.) : Repert�rio de leis e suas fun��es de abstrac��o e de representa��o.
A -> B � C <=(A -> B) � (A -> C)
A -> D � (B -> C) <= (A -> D) � ((A � B) -> C)
Aula Pr�tica de 2001.04.04 [Ref:3]:
Sum�rio: C�lculo de simula��es. Resolu��o de exerc�cios: simula��o de ina e de card. Refinamento algor�tmico. Algoritmos de pesquisa e sua efici�ncia. Padr�es de recursividade lineares vs bi-lineares. Resolu��o de exerc�cios: altera��o do padr�o de recursividade da fun��o belongsa.
Aula Te�rica de 2001.04.18 [Ref:2]:
Sum�rio: Refinamento formal de dados (cont.) : Invariantes (�concretos�) induzidos por representa��o. Exemplos. C�lculo de invariantes concretos.
Modela��o formal versus modela��o em sistemas de informa��o de base relacional. Sem�ntica formal de diagramas E-R (entidade rela��o) e seus invariantes.
Aula Pr�tica de 2001.04.18 [Ref:3]:
Sum�rio: Representa��o de dados e refinamento. Invertibilidade � direita e � esquerda. O c�lculo de isomorfismo. Resolu��o de exerc�cios: defini��o de fun��es de abstrac��o e suas inversas. Invertibilidade apenas � direita. O c�lculo inequacional. Resolu��o de exerc�cios. Defini��o de fun��es de abstrac��o e de representa��o.
Aula Pr�tica de 2001.04.23 [Ref:1]:
Sum�rio: Representa��o de dados e refinamento. Invertibilidade � direita e � esquerda. O c�lculo de isomorfismo. Resolu��o de exerc�cios: defini��o de fun��es de abstrac��o e suas inversas. Invertibilidade apenas � direita. O c�lculo inequacional. Resolu��o de exerc�cios. Defini��o de fun��es de abstrac��o e de representa��o.
Aula Pr�tica de 2001.04.30 [Ref:1]:
Sum�rio: O c�lculo inequacional (cont.). Introdu��o � reengenharia formal de bases de dados relacionais. Resolu��o dos exerc�cios 4.1, 4.2, 4.3 e 4.4.
Aula Te�rica de 2001.05.02 [Ref:2]:
Sum�rio: Sem�ntica formal de diagramas E-R (conclus�o) : Exemplo - o problema PPD (�rvores de produ��o e planeamento da produ��o).
Lei do refinamento estrutural de tipos indutivos. Exemplo: rela��es de refinamento entre listas (morfismos blast e embed).
Aula Pr�tica de 2001.05.02 [Ref:3]:
Sum�rio: O c�lculo inequacional (cont.). Introdu��o � reengenharia formal de bases de dados relacionais. Resolu��o dos exerc�cios 4.1, 4.2, 4.3 e 4.4.
Aula Pr�tica de 2001.05.07 [Ref:1]:
Sum�rio: Apresenta��o da ferramenta de invers�o formal de bases de dados K-RF. Anima��o do c�lculo de refinamento aplicado � engenharia reversa de bases de dados.