Programa

Especificação de Software

Mestrado Bolonha em Engenharia Informática e de Computadores - Alameda

Mestrado Bolonha em Engenharia Informática e de Computadores - Taguspark

Programa

Introdução: Motivação para a utilização de especificações e métodos formais; Métodos formais na indústria; Verificação de modelos vs procura de modelos vs prova de teoremas; Propriedades de segurança e de animação; Razões para usar ferramentas de métodos formais; Linguagens declarativas vs operacionais. O Analisador Alloy (http://alloy.mit.edu/alloy/): Introdução; Vantagens das abstrações; Sintaxe. Lógica no Alloy: Combinação de quantificadores de FOL com operadores de cálculo relacional; Estilo cálculo de predicado, estilo expressão de navegação, estilo cálculo relacional; Átomos e relações. Linguagem: Factos, Asserções, Predicados, Funções. Verificação de modelos e as suas propriedades. Modelação estática e dinâmica. A linguagem Dafny: (https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/): Introdução: Anotações e construção de programas verificados. Linguagem: Classes genéricas, afetação dinâmica, tipos de dados indutivos; Construções da especificação: pré- e pós-condições, invariantes de ciclo, asserções, especificações de enquadramento. Construções fantasma. Tipos coleção. Verificação de anotações e desenvolvimento de provas. Desenvolvimento incremental de programas imperativos verificados.