![]() | M�todos Formais de Programa��o I - 2002/03 |
---|---|
[ DI/UM ] |
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: 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: 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: 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: 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: Aula Laboratorial: Ficha 4 (invariantes); Ficha 5 (tipos indutivos).
Aula Pr�tica de 02.10.18 [Ref:4]:
Sum�rio: 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: Exerc�cios teorico-pr�ticos.
Aula Pr�tica de 02.10.25 [Ref:4]:
Sum�rio: 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: Exerc�cios teorico-pr�ticos.
Aula Pr�tica de 02.11.01 [Ref:4]:
Sum�rio: Não houve aula (feriado).