| 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.