1. CONTEÚDO

O conteúdo que estudaremos *não será* Teoria da Prova (http://en.wikipedia.org/wiki/Proof_theory). Eu gostaria que a disciplina tivesse um nome como "Provas Formais Assistidas e Aplicações", mas o currículo da nossa graduação não possui disciplina semelhante. Por essa razão, o código e o nome "CK0130 - TEORIA DA PROVA" estão sendo utilizados para fins formais.

O conteúdo que será de fato estudado será algum trecho inicial do livro "Software Foundations", de Benjamin Pierce et al:

http://www.cis.upenn.edu/~bcpierce/sf/

Como se pode ler no prefácio, trata-se de um livro eletrônico, publicamente disponível, centrado no uso do assistente de provas Coq para a realização de tarefas relacionadas com a obtenção de software confiável.

Como eu nunca ministrei esse conteúdo antes, eu não sei estimar o quanto desse livro nós conseguiremos cobrir durante o semestre letivo. Em princípio, eu estarei satisfeito se conseguirmos atingir o capítulo "Hoare Logic (Part II)".

2. OBJETIVO

O meu projeto de pesquisa de médio prazo é a obtenção de ferramentas (teoria e software) que permitam a verificação formal de software real, isto é, que se possa provar, nos mínimos detalhes, que certo software de fato realiza a tarefa que deveria realizar. Essa tarefa já está bastante adiantada no caso do paradigma da Programação Estruturada (vide plataformas como http://frama-c.com/) e, em todo caso, é atualmente levada à frente por uma ativa comunidade de pesquisa (vide, por exemplo, https://sites.google.com/site/verifiedsoftwareinitiative/vstte).

Na prática, provas formais carregam uma quantidade excessiva de detalhes, de forma que, para se demonstrar resultados significativos em tempo hábil, utiliza-se ferramentas que automatizem a parte mais mecânica do processo, deixando-se a cargo das pessoas a parcela da tarefa que mais demanda o esforço intelectual.

É no contexto acima que se enquadra a disciplina em questão. O livro-texto escolhido fornece uma introdução ao uso do Coq (http://en.wikipedia.org/wiki/Coq), um dos mais importantes assistentes de prova da atualidade, bem como à aplicação dele para fins de verificação de programas.

Eu espero que, ao fim da disciplina, estejamos aptos a utilizar o assistente de provas Coq para o desenvolvimento de provas formais quaisquer. Idealmente, nós teremos aprendido também como ele pode ser utilizado para a verificação de programas imperativos especificados por meio da lógica de Hoare (http://en.wikipedia.org/wiki/Hoare_logic).

3. PRÉ-REQUISITOS

O pré-requisito é a disciplina "Introdução à Lógica Matemática".

4. PÚBLICO-ALVO

Espero receber dois tipos de alunos:

  1. Aqueles interessados em aprender como as provas formais vistas na disciplina de Lógica podem ser escritas e utilizadas na prática, independentemente da aplicação.

  2. Aqueles interessados no assunto específico da verificação de programas, conforme explicado acima.

5. METODOLOGIA

Esse curso conta com a felicidade de poder ser realizado completamente na frente do computador, experimentando-se imediatamente cada funcionalidade nova aprendida. O LEC já foi solicitado para o horário da disciplina, mas, em face das demais disciplinas do curso, não sabemos ainda até que ponto a solicitação será atendida.

Serão realizadas 3 avaliações parciais, e a nota consistirá, em princípio, na média dessas provas. O aluno terá direito a uma segunda-chamada de cada avaliação, mas apenas no caso de impossibilidade real de comparecer a ela, e apenas mediante comprovação dessa impossibilidade.

Eu espero de cada aluno uma postura pró-ativa de aprendizado. Isso implica, em particular, em se ter disposição para participar das aulas, fazer os exercícios solicitados e tirar no tempo correto as dúvidas que surgirem. Como sempre tento fazer, eu pretendo estar amplamente à disposição para ajudar no aprendizado, mas, por outro lado, espero que cada aluno tenha motivação e disposição próprias para estudar, fazer os exercícios, etc.