| Especifica��o e Desenvolvimento Formal de 'Software' - 2002/03 |
|---|---|
| [ DI/UM ] |
| Aula Te�rica de 02.10.26 [Ref:1]: |
Sum�rio: Apresenta��o da disciplina. Programa e objectivos da disciplina. Regime de avalia��o. Informa��o electrónica sobre a disciplina: URL: http://www.di.uminho.pt/~jno/html/edfs.html. Bibliografia.
Motiva��o: especifica��o formal -- porquê e para quê? Introdu��o à especifica��o formal como m�todo de controlo de qualidade em `software' .
Aula Te�rica de 02.11.02 [Ref:1]:
Sum�rio: Introdu��o ao m�todo de especifica��o VDM e �s VDMTOOLS� da IFAD. Exemplo introdut�rio: sistema de alarmes de uma f�brica qu�mica (alarm.vdm).
In�cio do estudo da linguagem de especifica��o `standard' ISO/IEC 13817-1 (VDM-SL). Defini��o de tipos de dados. Introdu��o ao conceito de invariante de um tipo de dados. Tipos �registo�. Construtores mk_ e selectores.
Aula Te�rica de 02.11.09 [Ref:1]:
Sum�rio: Continua��o da an�lise do exemplo introdut�rio alarm.vdm e sua anima��o em VDMTOOLS� .
Aula Te�rica de 02.11.16 [Ref:1]:
Sum�rio: Estudo da linguagem de especifica��o `standard' ISO/IEC 13817-1 (VDM-SL): modela��o com conjuntos finitos: o tipo set of A em VDM-SL). Extens�o, compreens�o e filtragem. Nota��o-ZF.
Aula Te�rica de 02.11.23 [Ref:1]:
Sum�rio: Estudo da linguagem de especifica��o `standard' ISO/IEC 13817-1 (VDM-SL): modela��o com fun��es finitas: o tipo map A to B em VDM-SL. Extens�o, compreens�o e filtragem. Nota��o-ZF. Diagrama �ADJ� de operadores. Operadores totais, operadores parciais e suas pr�-condi��es.
Aula Te�rica de 02.11.30 [Ref:1]:
Sum�rio: Sequ�ncias
Aula Te�rica de 02.12.07 [Ref:1]:
Sum�rio: Especifica��o de fun��es sobre sequ�ncias. Morfismos de sequ�ncias. Nota��o em compreens�o como caso particular.
Aula Te�rica de 02.12.14 [Ref:1]:
Sum�rio: Especifica��o de fun��es sobre conjuntos e fun��es parciais finitas. Morfismos de conjuntos. Morfismos de fun��es parciais finitas. Nota��o em compreens�o como caso particular.
Aula Te�rica de 02.12.21 [Ref:1]:
Sum�rio: Invariantes, pre-condi��es e p�s-condi��es. A l�gica de predicados como sub-linguagem do ISO/IEC 13817-1 (VDM-SL). L�gica de fun��es parciais. Quantifica��o. Exemplo: modelo de um monitor de temperaturas de um reactor nuclear.
Aula Te�rica de 03.01.11 [Ref:1]:
Sum�rio: Sess�o de demonstra��o das VDMTOOLS� da IFAD. Exemplo: stack.vdm. `Literate programming' em VDM-SL. Integra��o com . Import�ncia das precondi��es e invariantes dos dados. Sua valida��o nas VDMTOOLS� . Obriga��es de prova. Demonstradores de teoremas.
Aula Te�rica de 03.01.18 [Ref:1]:
Sum�rio: Modelos com estado interno em VDM-SL. Opera��es e suas p�s-condi��es. Breve introdu��o ao VDM++. Demonstra��o de stack.vpp.
Aula Te�rica de 03.01.25 [Ref:1]:
Sum�rio: Intercombina��o da modela��o formal com t�cnicas informais. Convers�o de Diagramas ERA (`Entity-Relationship-Attribute') para modelos VDM-SL e respectivos invariantes ([Ol95d], p�g. 328).
S�ntese final. Discuss�o sobre a disciplina e o seu programa. Encerramento da disciplina.