FenixEdu™

Conhecer especificações formais e métodos formais para a engenharia de software, assim como as ferramentas/métodos de análise automática das propriedades dos programas. A disciplina fornece conhecimentos em: 1. Desenho e modelação de sistemas de software usando uma linguagem de especificação formal. Verificação automática de modelos e das suas propriedades. Linguagem de especificação declarativa para expressar restrições e comportamento de sistemas de software. Estados e traços. Modelação estática e dinâmica. 2. Verificação automática de programas (funcionais e imperativos) contra especificações. Verificação de propriedades funcionais. Construção de programas verificados através da anotação de código com teoremas, pré- e pós-condições, invariantes de ciclo, asserções, etc.

Programa

Introdução - Motivação para a utilização de especificações e métodos formais; Verificação de modelos vs procura de modelos vs prova de teoremas; Motivação para o uso de ferramentas de métodos formais; Linguagens declarativas vs operacionais. O Analisador Alloy - Introdução: Vantagens das abstrações; Sintaxe. Lógica no Alloy: Combinação de quantificadores de FOL com operadores de 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 - 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.

Metodologia de avaliação

Exame (50%) e dois projectos (25% + 25%)

Pré-requisitos

Esta UC requere familiaridade com programação imperativa e orientada por objectos bem como noções elementares de matemática discreta.

Componente Laboratorial

Exercícios em FOL, escrita de especificações usando o Analisador Alloy, lógica de Hoare, construção de programas verificados usando Dafny. Apoio ao projeto.

Princípios Éticos

Todos os membros de um grupo são responsáveis pelo trabalho do grupo. Em qualquer avaliação, todo aluno deve divulgar honestamente qualquer ajuda recebida e fontes usadas. Numa avaliação oral, todo aluno deverá ser capaz de apresentar e responder a perguntas sobre toda a avaliação.

Componente de Programação e Computação

No curso onde esta UC é oferecida estão asseguradas as componentes de Computação e Programação de acordo com o MEPP 2122.

Componente de Competências Transversais

Explicitar as Competências Transversais a desenvolver de acordo com o definido pela comissão de competências transversais, indicando qual a percentagem das suas componentes de avaliação que contempla a análise de competências transversais.