T (2006.10.21a): Apresentação da Disciplina. Introdução aos métodos formais de especificação e desenvolvimento de software. O binómio especificação-implementação. Objectivos e programa da disciplina; sua integração no plano curricular do curso.

T (2006.10.21b): Introdução à modelação de sistemas computacionais em VDM-SL. Tipos e invariantes. Especificação de operações. Estudo de um caso.

T (2006.11.04a): Conclusão da aula anterior. Apresentação da ferramenta VDMTools.

T (2006.11.04b): A linguagem de especificação VDM-SL: expressão de propriedades em lógica de 1a ordem. Problemas de definição.

T (2006.11.11a e 11b): Não houve aula.

T (2006.12.9a): A linguagem de especificação VDM-SL: modelação de problemas com conjuntos e sequências. Polimorfismo e ordem superior (exemplos). Especificação ímplicita vs explícita. Funções vs operações. Exemplo: cálculo da raíz quadrada (especificação disponível aqui).

T (2006.12.9b): A linguagem de especificação VDM-SL: modelação de problemas com correspondências. O caso do sistema de gestão de contas bancárias. Especificação funcional (BAMS) e orientada ao estado (SBAMS).

T (2006.12.16a): Aula laboratorial em VDMTools.

T (2006.12.16b): Aula laboratorial em VDMTools.

T (2007.01.20a): Estudo de caso em modelação VDM: multiconjuntos.

T (2007.01.20b): Discussão dos projectos individuais de modelação.

T (2007.01.27a): Estudo de caso em modelação VDM: o espaço de endereçamento web.

T (2007.01.27b): Acompanhamento dos projectos individuais de modelação.

-- LuisSoaresBarbosa - 27 Jan 2007