Verificação Dedutiva de Programas

Nesta disciplina nós aprendemos a demonstrar matematicamente a corretude de algoritmos estruturados, incluindo manipulação de ponteiros. A regulamentação oficial contém informações importantes como justificativa, objetivos, ementa e bibliografia; algumas dessas informações estão também no PPC do curso (página 139).

O conteúdo da disciplina está detalhadamente descrito no plano de atividades, que também contém as datas estimadas de cada uma delas.

As fontes de estudo da disciplina estão todas online, e elas estão listadas na bibliografia.

As atividades práticas da disciplina serão feitas na ferramenta Dafny, que pode ser executada diretamente pelo navegador.

Plano de Atividades

Média das Avaliações	≥ 7	7 > média ≥ 4	< 4
Situação	Aprovado	AF	Reprovado

Aula	Data	Descrição
01 - P01	13/03	Introdução e Prática em Dafny: Pré- e Pós-condições, Asserções, etc.
	15/03	Aula Cancelada pelo Professor
02 - P02	20/03	Dafny: Laços, Vetores, Funções Puras, Predicados.
03 - T01	22/03	Floyd: Assigning Meanings to Programs – Parte 1 / 2
04 - P03	27/03	Dafny: Conjuntos, Sequências, Multiconjuntos, Mapeamentos.
	29/03	Encontros Universitários 2016
05 - P04	03/04	Dafny: Provas via Lemas e Indução
06 - T02	05/04	Floyd: Assigning Meanings to Programs – Parte 2 / 2
07 - P05	10/04	Dafny: Algoritmos de Ordenação – Parte 1 / 2
08 - T03	12/04	Hoare: An Axiomatic Basis for Computer Programming – Teoria
09 - P06	17/04	Dafny: Algoritmos de Ordenação – Parte 2 / 2
10 - T04	19/04	Hoare: An Axiomatic Basis for Computer Programming – Exercícios
*	24/04	Avaliação Prática 1
11 - T05	26/04	Dijkstra: Guarded commands, nondeterminacy etc. – Parte 1 / 2
	01/05	Feriado: Dia do Trabalho
12 - T06	03/05	Dijkstra: Guarded commands, nondeterminacy etc. – Parte 2 / 2
13 - P07	08/05	Dafny: Pilha via Vetor, Versão Explícita – Parte 1 / 3.
14 - T07	10/05	Revisão sobre os artigos de Floyd, Hoare e Dijkstra.
15 - P08	15/05	Dafny: Pilha via Vetor, Versão Explícita – Parte 2 / 3.
*	17/05	Avaliação Teórica 1
16 - P09	22/05	Dafny: Pilha via Vetor, Versão Explícita – Parte 3 / 3.
17 - P10	24/05	Dafny: Pilha via Vetor, Versão com Interface – Parte 1 / 3.
18 - T08	29/05	Memória na Lógica de Hoare – Parte 1 / 3
19 - T09	31/05	Memória na Lógica de Hoare – Parte 2 / 3
20 - P11	05/06	Dafny: Pilha via Vetor, Versão com Interface – Parte 2 / 3.
21 - T10	07/06	Memória na Lógica de Hoare – Parte 3 / 3
22 - P12	12/06	Dafny: Pilha via Vetor, Versão com Interface – Parte 3 / 3.
23 - P13	14/06	Dafny: Pilha via Lista Encadeada – Parte 1 / 2.
24 - P14	19/06	Dafny: Pilha via Lista Encadeada – Parte 2 / 2.
25 - P15	21/06	Dafny: Pilha Extensível via Vetor.
26 - P16	26/06	Dafny: Pilha Extensível via Lista Encadeada.
*	28/06	Avaliação Prática 2: Apresentação das Tarefas de Verificação.
27 - T11	03/07	Embutimentos de Linguagens
28 - T12	05/07	Lógica de Separação – Parte 1 / 2
29 - T13	10/07	Lógica de Separação – Parte 2 / 2
*	12/07	Avaliação Teórica 2
*	17/07	AF
	19/07	Notas Finais da Disciplina

Aulas: Conteúdos e Exercícios

Aula 1, Prática 1 (2017-03-13, Segunda-feira):
- Visão Geral da Disciplina e do Conteúdo a ser ministrado.
- Introdução à Verificação Dedutiva de Programas: vídeo de palestra (ver até minuto 18).
- Tutorial Getting Started with Dafny (estudo individual, não sincronizado).
EXERCÍCIOS ESSENCIAIS:
1. Continue o estudo do tutorial.
2. Comece a leitura do artigo de Floyd: você provavelmente gostará da experiência de começar a lê-lo antes das explicações da próxima aula.
Aula 2, Prática 2 (2017-03-20, Segunda-feira):
- Visão Geral dos Conceitos do tutorial Getting Started with Dafny.
- Conclusão do Estudo do Tutorial.
EXERCÍCIOS ESSENCIAIS:
1. (Sorted Array) Escreva um método "ordenado" que receba um vetor de inteiros e retorne um booleano indicando se o vetor está ordenado. Forneça e verifique uma ou mais pós-condições que dêem as garantias devidas sobre o vetor em ambos os casos de retorno da função.
  Observação: você não precisa escrever as pós-condições desde o início. Se preferir, você pode primeiramente escrever o conteúdo computacional do método, e só depois ir adicionando as asserções para verificação, até completar o processo.
2. (GCD Function) Escreva e verifique uma função (function) que calcule o maior divisor comum de dois números naturais positivos. A função deve ter pós-condições garantindo que:
  - O valor retornado é de fato um divisor comum.
  - Todo divisor comum é menor ou igual ao valor retornado.
  Observação: você pode definir funções auxiliares, caso deseje. (Além disso, a observação do exercício anterior continua valendo.)
Aula 3, Atividade Teórica 1 (2017-03-22, Quarta-feira):
- Introdução do Artigo de Floyd: base da abordagem.
- Definições Iniciais: Fluxograma, Interpretação, Verificação, etc.
- Propriedades ("axiomas") de Definições Semânticas Corretas e Completas.
- Motivação da Condição de Verificação da Atribuição.
EXERCÍCIOS ESSENCIAIS:
1. (Interpretação Euclides) Usando a linguagem de fluxograma do artigo de Floyd, escreva o algoritmo de Euclides para o cálculo do MDC de 2 números. (Aqui está um GIF do funcionamento de algoritmo, para lhe lembrar do algoritmo sem mostrar o pseudocódigo.)
  Após escrever o algoritmo, forneça uma interpretação para ele (no sentido técnico do artigo).
2. (Verificação Euclides) Aplique as condições de verificação (CVs) definidas no artigo (págs. 23 e 24) aos programa e interpretação do exercício anterior, e verifique a interpretação mostrando que essas CVs valem.
Aula 4, Prática 3 (2017-03-27, Segunda-feira):
- Estudo do Tutorial Collections.
EXERCÍCIOS ESSENCIAIS:
1. (Sum Array) Escreva uma função (function) que calcule a soma de uma sequência de inteiros. Em seguida, escreva e verifique um método que receba um vetor de inteiros e então retorne a soma dos elementos do vetor. O método deve ter uma pós-condição garantindo que o valor retornado é igual à soma da sequência dos elementos do vetor. A garantia de que o vetor não é alterado também deve estar nas pós-condições (a[..] == old(a[..])).
  IMPORTANTE: caso a sua função de soma de uma sequência funcione adicionando o primeiro elemento à soma dos demais, talvez você facilite a verificação do seu método de soma de um vetor se ele também percorrer o vetor do fim para o início. (Em breve, nós aprenderemos recursos de prova adicionais, que nos permitirão verificar também a soma do início para o fim do vetor.)
2. (Disjoint Arrays) Escreva um método que receba dois vetores de inteiros e que retorne um booleano indicando se os vetores são disjuntos ou não (isto é, se eles não possuem elementos em comum). Esse significado do valor retornado deve estar claro nas pós-condições, as quais também devem garantir que os vetores permanecem inalterados.
  Dica: aproveite as conveniências de notação da linguagem. A pós-condição principal pode ser escrita em uma linha simples.
Aula 5, Prática 4 (2017-04-03, Segunda-feira):
- Lemas e Indução em Dafny: um exemplo para soma de um vetor.
  1. Função para somar os elementos de uma sequência de inteiros.
  2. Método para somar os elementos de um vetor de inteiros.
  3. Invariante para provar a pós-condição do método.
  4. Lema para provar o invariante.
- Estudo do Tutorial Lemmas (seção "Paths In a Directed Graph" opcional).
EXERCÍCIOS ESSENCIAIS:
1. Termine a leitura do tutorial (não é necessário ler a última seção).
2. (GCD Sym) Retomando o seu código de exercício anterior sobre MDC, prove que o MDC de "x" e "y" é igual ao MDC de "y" e "x".
Aula 6, Atividade Teórica 2 (2017-04-05, Quarta-feira):
- Condições de Verificação dos Comandos da Linguagem do artigo de Floyd.
- Interpretação e Verificação, sem terminação, do Algoritmo de MDC de Euclides.
- Argumentação parcial da terminação do Algoritmo de Euclides.
EXERCÍCIOS ESSENCIAIS:
1. Conclua a demonstração de terminação iniciada em sala.
2. (Soma de Matriz) Escreva e verifique um fluxograma que calcule a soma dos elementos de uma matriz.
Aula 7, Prática 5 (2017-04-10, Segunda-feira):
- Verificação de Algoritmo de Ordenação (sugestão: Ordenação por Seleção).
  1. Provar que os elementos do vetor final são os mesmos do vetor inicial.
  2. Provar que o vetor final está ordenado segundo ≤.
EXERCÍCIOS ESSENCIAIS:
1. Conclua a verificação do seu método de ordenação.
2. (Quicksort Lomuto) Escreva e verifique uma versão O(n²) do Quicksort que particione o vetor por meio do algoritmo de Lomuto (que percorre o vetor do início para o fim, ao invés de usar 2 índices que andam das extremidades para o meio).
Aula 8, Atividade Teórica 3 (2017-04-12, Quarta-feira):
- Recapitulação e Conclusão da Técnica de Terminação do artigo de Floyd.
- Contextualização e Relação das Contribuições dos artigos de Floyd e Hoare.
- Lógica de Hoare: Axiomas, Regras de Inferência e Exemplos.
- Prova do Algoritmo de Divisão do Artigo de Hoare.
EXERCÍCIOS ESSENCIAIS:
1. (Fatorial) Usando a Lógica de Hoare conforme apresentada no artigo, escreva e verifique um programa para calcular o fatorial de um número natural "n" qualquer:
```
n! = | 1,          se n = 0
     | n * (n−1)!, se n > 0.
```
```
(
 f := 1 ;
 i := 0
) ;
WHILE i < n DO
  (
   i := i + 1;
   f := f * i
  )
```
2. (Regra do if) Como observamos em sala, o artigo de Hoare não explicita uma regra de inferência para o comando if/else, mas é fácil obtê-la. Assim, tomando como base as outras regras do artigo, escreva uma regra de inferência para o comando if/else, e em seguida uma regra para o comando if. Ao final, você pode checar a sua resposta na Wikipédia (e também compará-la com a regra do artigo de Floyd, Figura 3).
3. (Fibonacci) Escreva e verifique um programa para, dado um natural "n", calcular Fibonacci(n):
```
fib(n) = | n,                   se n ≤ 1
         | fib(n−2) + fib(n−1), se n > 1.
```
```
IF n ≤ 1 THEN
  fib_i := n
ELSE
  (
   i     := 2 ;
   fib_i := 1 ;
   fib_h := 1 ;  // fib_h = fib(i−1)
   WHILE i < n DO
     (
      i     := i + 1         ;
      soma  := fib_h + fib_i ;
      fib_h := fib_i         ;
      fib_i := soma
     )
  )
```
Aula 9, Prática 6 (2017-04-17, Segunda-feira):
- Continuação da Verificação da Ordenação por Seleção.
- Início da Verificação do Algoritmo Quicksort com Particionamento de Lomuto.
EXERCÍCIOS ESSENCIAIS:
1. Conclua a verificação do Quicksort.
2. (Mergesort) Escreva e verifique o algoritmo Mergesort.
Aula 10, Atividade Teórica 4 (2017-04-19, Quarta-feira):
- Observação sobre Atribuição em Vetores:
  como provar "i = j {A[j] := 1} A[i] = 1"?
- Regra para Atribuição em Vetores [Hoare & Wirth, 1973]:
  P[A ↦ A(i: e)] {A[i] := e} P
  onde "A(i: e)" significa [ A[0], ..., A[i−1], e, A[i+1], ..., A[ |A|−1 ] ].
  Observação: acima, a notação "P[x ↦ y]" representa o resultado da substituição em P das ocorrências livres de "x" por "y".
- Axiomas para Acessar "A(i: e)" [Gordon Handouts, p. 189]:
  - A(i: e)[i] = e
  - i ≠ j → A(i: e)[j] = A[j]
- Exemplo 1:
  i = j {A[j] := 1} A[i] = 1
- Exemplo 2:
  A[i] = x ∧ A[j] = y ∧ i ≠ j { código para trocar A[i] e A[j] } A[i] = y ∧ A[j] = x
- Exemplo 3:
  ∀k, 0 ≤ k < n → A[k] = B[k] { código para inverter A (não usa B) } ∀k, 0 ≤ k < n → A[k] = B[n −1 −k]
EXERCÍCIOS ESSENCIAIS:
1. (Trocar Índices Iguais) Verifique que o código para trocar A[i] e A[j] funciona mesmo sem a restrição i ≠ j.
2. (Ordenação) Usando a Lógica de Hoare, escreva e verifique um algoritmo de ordenação simples.
Aula 11, Atividade Teórica 5 (2017-04-26, Quarta-feira):
- Introdução ao Artigo de Dijkstra.
- Estruturas de Seleção e Repetição Não-Determinísticas usando Comandos com Guarda.
- Definição e Propriedades do Transformador de Predicados "wp".
- Definição de "wp" para "skip", ":=" e ";".
- Definição de "wp" para a Estrutura de Seleção.
  - Exemplo em Sala: prova do programa do máximo de 2 números.
- Definição de "wp" para a Estrutura de Repetição.
EXERCÍCIOS ESSENCIAIS:
1. (Ordenar 3) Sendo
  - PRE: x,y,z ∈ Z ∧ a = x ∧ b = y ∧ c = z
  - POST: x,y,z ∈ Z ∧ multiset{a,b,c} = multiset{x,y,z} ∧ a ≤ b ∧ b ≤ c
  escreva um programa "P" e verifique que PRE → wp(P, POST). Importante:
  1. Não use a estrutura de repetição do: a ideia é treinar o if.
  2. A entrada do programa está nas variáveis "a", "b" e "c"; "x", "y" e "z" fazem parte apenas da especificação.
2. Termine de ler sobre a estrutura de repetição no artigo.
Aula 12, Atividade Teórica 6 (2017-05-03, Quarta-feira):
- Recapitulação de "wp" para "if" e "do" (artigo de Dijkstra).
- Teoremas 3 e 1.
- Definição de "wdec" e Teoremas 2 e 4.
- Exemplo de Prova de "wp" para "do": Ordenação de 3 Números.
  - Complemento da prova de wdec.
EXERCÍCIOS ESSENCIAIS:
1. (Invariante do Laço) Termine a prova do exemplo dado em sala, provando que I é de fato um invariante:
```
  * VC1: I && BB ==> wp(IF, I)
```
  As definições das abreviações acima estão no complemento da aula.
2. (Número de Inversões) Redefina a métrica de terminação "t" para o exemplo dado em sala, definindo t(a,b,c) como o número de inversões da sequência "[a, b, c]" (apresente uma definição precisa para essa função em termos mais elementares). Em seguida, refaça a prova de terminação:
```
  * VC2: I && BB ==> wdec(IF, t)

  * VC3: I && BB ==> t >= 0
```
Aula 13, Prática 7 (2017-05-08, Segunda-feira):
- Implementação de Pilha via Vetor usando Classes em Dafny.
  - Descrição da atividade.
EXERCÍCIOS ESSENCIAIS:
1. Conclua a implementação iniciada em sala.
2. (Fila) Experimente implementar uma fila nos mesmos moldes da pilha.
Aula 14, Atividade Teórica 7 (2017-05-10, Quarta-feira):
- Revisão sobre os artigos de Floyd, Hoare e Dijkstra.
Aula 15, Prática 8 (2017-05-15, Segunda-feira):
- Implementação de Pilha via Vetor usando Classes em Dafny.
  - Descrição da atividade.
EXERCÍCIOS ESSENCIAIS:
1. ...
2. ...

Verificação Dedutiva de Programas – 2017.1

Avisos

Informações Gerais

Regras

Bibliografia

Plano de Atividades

Aulas: Conteúdos e Exercícios