Aqui está, para quem desejar, o plano de atividades (quase) original da turma de Verificação Dedutiva de Programas de 2017-1.
Aulas Teóricas: apresentam alguns dos mais importantes fundamentos teóricos das ferramentas de verificação dedutiva atuais. Estão assim divididas:
Parte 1: artigos clássicos sobre Verificação de Programas. Dão o substrato teórico para a verificação de programas sem ponteiros.
Parte 2: verificação de programas com ponteiros, por meio da mais recente Lógica de Separação, formalizada no Coq.
Parte 3: estudo da teoria das "Dynamic Frames", que é o substrato teórico da manipulação de memória em Dafny.
Aulas Práticas: são realizadas na ferramenta Dafny, e habilitam o aluno à utilização dos principais recursos atualmente disponíveis para a verificação dedutiva no nível de programas. Estão assim divididas:
Parte 1: introdução aos recursos básicos de verificação em Dafny.
Parte 2: verificação de estruturas de dados em Dafny, incluindo estruturas com ponteiros.
Parte 3: realização de um trabalho final de verificação (de uma estrutura mais elaborada, etc).
| 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 | |
| 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 e usando Classe. |
| * | 10/05 | Avaliação Teórica 1 |
| 14 - P08 | 15/05 | Dafny: Pilha separando Interface e Implementação. |
| 15 - T07 | 17/05 | Memória na Lógica de Hoare – Parte 1 / 2 |
| 16 - P09 | 22/05 | Dafny: Heaps. |
| 17 - T08 | 24/05 | Memória na Lógica de Hoare – Parte 2 / 2 |
| 18 - P10 | 29/05 | Dafny: Listas Encadeadas. |
| 19 - T09 | 31/05 | Lógica de Separação – Parte 1 / 3 |
| 20 - P11 | 05/06 | Dafny: Filas e Pilhas via Listas Encadeadas. |
| 21 - T10 | 07/06 | Lógica de Separação – Parte 2 / 3 |
| 22 - P12 | 12/06 | Dafny: Tipos Indutivos; Árvores Binárias de Busca. |
| 23 - T11 | 14/06 | Lógica de Separação – Parte 3 / 3 |
| * | 19/06 | Avaliação Prática 2 |
| * | 21/06 | Avaliação Teórica 2 |
| 24 - P13 | 26/06 | Acompanhamento dos Projetos de Verificação |
| 25 - T12 | 28/06 | The Dynamic Frames Theory |
| 26 - P14 | 03/07 | Acompanhamento dos Projetos de Verificação |
| 27 - T13 | 05/07 | The Dynamic Frames Theory |
| * | 10/07 | Apresentação dos Projetos de Verificação |
| 12/07 | Notas dos Projetos. | |
| * | 17/07 | AF |
| 19/07 | Notas Finais da Disciplina |