Verificação Dedutiva de Programas – 2016.1

Segunda chamada: consulte as regras para a solicitação de prova de segunda chamada.

Aula 1 (2016-03-14, segunda-feira): introdução à disciplina; exemplos de verificação na plataforma Frama-C (máximo de 2 números e busca linear num vetor; arquivos no SIGAA).

EXERCÍCIOS RECOMENDADOS:

1. Tomando como base o exemplo do arquivo busca_linear.c (e extensões óbvias, como \exists), escreva e verifique uma função que calcula o máximo de um vetor.

2. Idem ao exercício anterior, mas com relação a uma versão iterativa do algoritmo de busca binária.

PARA INSTALAR O FRAMA-C:

• Uma maneira trivial é usar o gerenciador de pacotes do Linux e instalar de lá. Ou simplesmente executar sudo apt-get install frama-c-gui.

  A desvantagem é que a versão instalada pode não ser a última, e além disso essa instalação não inclui provadores automáticos de teorema fora o Alt-Ergo (Z3, CVC4, etc). Para tanto, é preciso instalar o Why3 (que eu instalo via OPAM, opção abaixo).

• Outra maneira simples, mas não tão direta quanto essa acima, é instalar o OPAM (que instala programas OCaml compilando o código fonte), e daí instalar o Frama-C, o Why3, etc, todos sendo automaticamente as versões mais recentes.

  A desvantagem é você não conseguir instalar a tempo, e daí não conseguir fazer os exercícios, que são o principal; não perca tempo demais com esses detalhes!

  A instalação do OPAM pode ser trivial (executar eval `opam config env` em seguida, como solicitado ao fim da instalação). Depois disso, basta fazer algo como:

  opam install depext
  opam depext why3
  opam install why3
  opam depext frama-c
  opam install frama-c
  

  Depois disso, basta instalar o Z3 e o CVC4, executar why3 config --detect (para o Why3 reconhecer os provadores instalados) e chamar o Frama-C usando -wp -wp-prover alt-ergo,z3,cvc4 (para ele usar todos os 3 provadores).

Aula 2 (2016-03-17, quarta-feira): introdução à verificação de algoritmos; exemplo 1: máximo de dois números (projeto de pré- e pós-condições; manipulação de estrutura de seleção; prova de terminação); exemplo 2: busca linear (prova de correção total usando variante e invariantes de laço; prova de variante: limite inferior (inicial e ao fim de iteração) e diminuição).

EXERCÍCIOS ESSENCIAIS:

1. Tente provar que os invariantes que escrevemos para o algoritmo de busca linear estão corretos. Como explicado em sala, a prova tem duas partes: validade inicial e preservação. Depois de escrever a sua prova, veja o material citado mais abaixo para conferir.

2. Especifique, via pré- e pós-condições, um algoritmo para calcular o máximo de um vetor v[1..n] (n ≥ 1), e prove, usando variante e invariantes, que o algoritmo atende à especificação. Além disso, você deve provar que o variante e os invariantes estão corretos. ATENÇÃO: o exercício 5-C do material 3 abaixo possui uma solução, mas veja-a APENAS DEPOIS de preparar a sua!

3. Idem ao exercício anterior, mas com relação a uma versão iterativa do algoritmo de busca binária. (Esse exercício é mais trabalhoso, e portanto útil para testar a sua compreensão do assunto e identificar possíveis dúvidas.)

MATERIAL DE ESTUDO: as notas de aula [1], [2] e [3] de CAnA 2015.1 cobrem essencialmente o mesmo conteúdo que vimos nesta aula, e apresentam por escrito as demonstrações que apresentei apenas verbalmente (há diferenças, mas mais em forma que em conteúdo).

Aula 3 (2016-03-21, segunda-feira): prática de verificação na plataforma Frama-C (frama-c-gui -wp -wp-rte codigo.c). Exemplos abordados: teste de igualdade entre dois vetores; identificação do primeiro par de adjacentes iguais num vetor; teste de ordenação de um vetor.

Recursos ACSL utilizados: requires, ensures, assigns, loop invariant, loop variant, loop assigns.

EXERCÍCIOS ESSENCIAIS:

1. Com relação aos exercícios feitos durante a aula, compare as especificações que você escreveu com aquelas disponibilizadas no SIGAA – atenção aos detalhes! Certifique-se de que as suas funções atendem às especificações, e, para garantir a terminação do código, apresente e prove um loop variant para cada laço. (A linguagem ACSL já aceita uma especificação como terminates \true para funções, mas infelizmente ela ainda é ignorada pelo plug-in WP.)

2. Escreva e verifique uma função que receba um vetor "v" de "n" inteiros em ordem crescente (≤) e um um inteiro "x", e que retorne a posição "k" do vetor tal que, se inseríssemos "x" entre v[k-1] e v[k], o vetor continuaria ordenado (em caso de múltiplas opções, retorne a posição mais à esquerda).

3. Escreva e verifique uma função iterativa de busca binária.

MATERIAL DE REFERÊNCIA: manual da linguagem de especificação ACSL.

Aula 4 (2016-03-23, quarta-feira): prova de invariantes de laço: validade inicial e preservação (exemplo: busca linear); variantes e invariantes de laço "Para" (exemplo: primeiro par de adjacentes iguais num vetor).

EXERCÍCIOS ESSENCIAIS:

1. Escreva, especifique e verifique um algoritmo que retorne o índice do segundo menor número de um vetor v[1..n] tal que "n ≥ 2".

2. Escreva, especifique e verifique um algoritmo que receba um vetor de inteiros e que substitua por zero todos os números negativos do vetor (use um laço "para").

MATERIAL DE ESTUDO: os mesmos materiais [1], [2] e [3] mencionados na aula 2.

Aula 5 (2016-03-28, segunda-feira): prática de verificação: busca binária iterativa.

EXERCÍCIOS ESSENCIAIS:

1. Compare a especificação que você escreveu no laboratório com aquela disponibilizada no SIGAA – atenção aos detalhes! Certifique-se de que a sua função atende a toda a especificação, e, para garantir a terminação do código, apresente e prove um variante para o laço do algoritmo.

MATERIAL DE REFERÊNCIA: manual da linguagem de especificação ACSL.

Aula 6 (2016-03-30, quarta-feira): verificação de laços com "break" (exemplo: checar ordenação de vetor); verificação do uso de operadores ([], ÷, etc); verificação do algoritmo iterativo de busca binária.

EXERCÍCIOS ESSENCIAIS:

1. Especifique, escreva e verifique um algoritmo que retorne o índice do primeiro elemento negativo de um vetor de "n ≥ 0" números, ou que retorne "n+1" se não existir tal elemento. Use "break"!

2. Especifique, escreva e verifique um algoritmo de particionamento para o Quicksort (você pode escolher entre a partição de Lomuto, a de Hoare ou ainda outra, se você preferir).

   Atenção: este exercício não pede que você trate do algoritmo de ordenação Quicksort propriamente dito, mas apenas do algoritmo de particionamento, que coloca o pivô à direita dos elementos menores que ele e à esquerda dos elementos maiores que ele.

   Sugestão: receba a posição do pivô como argumento, ao invés de o valor do pivô.