Construção e Verificação de Software
Objetivos
Saber
Os alunos consolidam as aptidões de construção de desenvolvimento de software confiável, no contexto dos modernos sistemas.
A UC desenvolve o ponto de vista de que a verificação dever ser integrada de forma coesa com os processos de construção de software, orientada pelo uso de ferramentas de análise de código.
São cobertas as técnicas fundamentais de análise estática de código, nomeadamente a verificação de programas funcionais, a utilização de Lógica Hoare e utilização de Lógica da Separação.
Saber Fazer
Usar métodos de programação rigorosos e técnicas de verificação para garantir a fiabilidade de software.
Desenvolver, em trabalho de grupo, projetos de média dimensão que envolvem o desenho de uma especificação e implementação verificada de algoritmos e programas não-triviais.
Usar asserções lógicas para especificar, verificar e raciocinar sobre a correcção de programas, assim como as ferramentas associadas (Coq, Why3, CFML).
Definir fluentemente especificações comportamentais (invariantes, pre-condições e pós-condições) para a implementação de módulos e suas interfaces.
Caracterização geral
Código
11159
Créditos
6.0
Professor responsável
Carla Maria Gonçalves Ferreira, Mário José Parreira Pereira
Horas
Semanais - 4
Totais - 52
Idioma de ensino
Português
Pré-requisitos
A disponibilizar brevemente
Bibliografia
Software Foundations: https://softwarefoundations.cis.upenn.edu/
Coq reference manual: https://coq.inria.fr/distrib/current/refman/
Many books, tutorials and videos about Coq: https://coq.inria.fr/documentation
Why3 reference manual: https://why3.lri.fr/manual.pdf
Many tutorials on Why3: https://why3.lri.fr/
Software Foundations, Volume 6: https://softwarefoundations.cis.upenn.edu/slf-current/index.html
Several classical papers by Liskov, Hoare, Dijkstra, Brinch Hansen, Doug Lea, O’Hearn, Schneider.
Related course at the Parisian Master of Research in Computer Science: https://wikimpri.dptinfo.ens-cachan.fr/doku.php?id=cours:c-2-36-1
Método de ensino
O ensino consiste na exposição da matéria em aulas teóricas e na resolução de problemas em aulas práticas.
As aulas teóricas apresentam os conceitos centrais da disciplina: verificação de programas funcionais, Lógica de Hoare, cálculo de pré-condição mais fraca, Lógica da Separação.
No laboratório, os alunos utilizam ferramentas de verificação formal de software para resolver exercícios e desenhar programas de pequena-média dimensão verificados.
Método de avaliação
Componentes da Avaliação
A avaliação é constituída por duas componentes: a componente laboratorial e a componente teórico-prática.
Componente Laboratorial e Frequência
A componente laboratorial é composta por três trabalhos e tem um peso de 40% da nota final. Cada trabalho consiste num exercício de desenho de um programa formalmente verificado (i.e., especificação mais implementação). Estes trabalhos devem ser realizados em grupo de dois alunos, estando as notas sujeitas a eventuais discussões.
A nota da componente laboratorial (CompL) é a média das notas do aluno nos três trabalhos (P1, P2 e P3):
CompL = (P1 + P2 + P3) / 3.
Para obter frequência, é necessário que CompL >= 9.5.
Componente Teórico-Prática
A componente teórico-prática consiste na realização de dois testes (período das aulas) ou de um exame (na época de recurso). Todas as provas são escritas, individuais, presenciais e com consulta de qualquer material impresso. Esta componente representa um peso de 60% da nota final.
A nota da componente teórico-prática (CompTP) é a média das notas dos testes (T1 e T2) ou a nota do exame (Ex):
CompTP = (T1 + T2) / 2 ou CompTP = Ex.
Para obter aprovação, é necessário que CompTP >= 9.5 .
Nota Final
A nota final (F) dos alunos com frequência é:
- F = CompTP, se CompTP < 9.5;
- F = 0.4 CompL + 0.6 CompTP, se CompTP >= 9.5 .
Todas as notas (P1, P2, P3, T1, T2, Ex, CompL e CompTP) são arredondadas às décimas, exceto a nota final (F) que é arredondada às unidades.
Conteúdo
1. Verificação de programas funcionais
Raciocínio algébrico sobre o comportamento de programas sem estado. Provas por indução. Definição e utilização de proposições indutivas. Princípios de indução. Verificação de estruturas de dados não-triviais usando raciocínio algébrico.
2. Verificação de programas imperativos
Métodos baseados em Asserções e Lógicas de Hoare. Cálculo de pré-condição mais fraca. Programação com arrays. Código ghost. Tratamento de excepções. Modularidade. Especificação de estruturas de dados baseadas em modelos lógicos. Tratamento e controlo estático de aliasing.
3. Verificação de programas com memória heap
Lógica da Separação. Predicados indexados pela heap. Regra de frame. Predicados de representação para listas e árvores. Segmentos de listas. Raciocínio sobre funções. Funções de ordem superior e iteração. Predicados de representação de ordem superior. Introdução ao estudo da concurrência em Lógica da Separação.