MENU: [ Avisos | Informações Gerais | Regras | Plano de Atividades ]
Última atualização: 10/12/2015.
Atenção para a data da AP2 e para a especificação da AP3 (me informe a sua preferência de capítulo por e-mail).
Leia toda esta página no início do semestre: ela contém informações importantes, como as regras para solicitação de segunda chamada e para o cálculo da nota na disciplina.
Esta página está em contínua construção. Por favor, entre em contato comigo caso você precise de alguma informação adicional, ou caso acredite ter encontrado um erro aqui. Obrigado!
Caro aluno, na regulamentação desta disciplina você pode acessar as informações básicas sobre ela, incluindo justificativa, objetivos, ementa e bibliografia.
Nesta disciplina, nós aprendemos a usar o assistente de prova Coq, utilizando como livro-texto o excelente Software Foundations.
Todas as atividades da disciplina já possuem data estimada no plano de atividades.
A minha sugestão para a obtenção de um bom desempenho na disciplina é, aula-a-aula, estudar o conteúdo previamente, participar das aulas, fazer os exercícios e tirar as dúvidas. Caso você possua uma dúvida no horário da aula, o ideal é tirá-la na própria ocasião, para que os demais alunos também se beneficiem das explicações. Entretanto, caso necessário, você também pode me contactar fora do horário de aula.
Segunda chamada: consulte as regras para a solicitação de prova de segunda chamada.
Nota da disciplina: Consistirá na média aritmética das notas obtidas pelo aluno nas três avaliações da disciplina:
| Média das Avaliações | ≥ 7 | 7 > média ≥ 4 | < 4 |
|---|---|---|---|
| Situação | Aprovado | AF | Reprovado |
Avaliação 3: será um estudo seguido de apresentação. Mais precisamente, cada aluno deverá:
Estudar um destes capítulos do Coq'Art (material com o professor) (há uma descrição dos capítulos na seção 1.7 do livro):
| Capítulo | Conteúdo | Responsável |
|---|---|---|
| 07 – Tactics and Automation | Mais sobre Automatização de Prova no Coq | Mariana |
| 09 – Functions and Their Specifications | Funções que Recebem Provas como Argumentos | Rafael |
| 10 – Extraction and Imperative Programming | Extração Automática de Programas Certificados do Coq | |
| 12 – The Module System | Recursos para Modularização de Teorias | |
| 14 – Foundations of Inductive Types | Os Fundamentos Teóricos do Coq | Heitor |
| 15 – General Recursion | Recursão Mais Geral no Coq |
Preparar uma aula didática e informativa sobre o conteúdo, incluindo um arquivo .v para a audiência.
Apresentar o conteúdo aos demais membros da turma (em data prevista no plano de atividades; ordem das apresentações: a mesma da numeração dos capítulos).
Até "MoreCoq": Recursos básicos de prova; tipos indutivos e polimórficos.
Até "MoreInd": Lógica; mais recursos de prova.
Até o final: Aplicação à verificação de programas; automatização de provas.
| Aula | Data | Descrição |
|---|---|---|
| 1 | 04/08 | Apresentação da Disciplina; Preface; Basics. |
| 2 | 06/08 | Basics |
| 3 | 11/08 | Induction |
| 4 | 13/08 | Lists |
| 5 | 18/08 | Lists |
| 6 | 20/08 | Poly |
| 25/08 | Sem aula: Professor na UFRN | |
| 27/08 | Sem aula: Professor na UFRN | |
| 7 | 01/09 | Poly |
| 8 | 03/09 | MoreCoq |
| 9 | 08/09 | MoreCoq |
| 10 | 10/09 | Logic |
| 11 | 15/09 | Logic |
| 12 | 17/09 | Prop |
| * | 19/09 | Avaliação 1: até "MoreCoq". (SÁBADO!) |
| 13 | 22/09 | Correção da AP1. |
| 14 | 24/09 | Prop |
| 15 | 29/09 | Prop (Tirando dúvidas) |
| 16 | 01/10 | Rel |
| 17 | 06/10 | Rel (Tirando dúvidas) |
| 18 | 08/10 | MoreLogic |
| 13/10 | Sem aula: Dia do Professor | |
| 19 | 15/10 | ProofObjects |
| 20/10 | Sem aula: Compromisso Pessoal do Professor. | |
| 20 | 22/10 | MoreInd |
| 21 | 27/10 | MoreInd |
| 29/10 | Sem aula: Alunos Viajando. | |
| 22 | 03/11 | MoreInd |
| * | 05/11 | Avaliação 2: até "MoreInd". |
| 23 | 10/11 | Correção da AP2. |
| 24 | 12/11 | Imp |
| 25 | 17/11 | Imp |
| 26 | 19/11 | Imp |
| 27 | 24/11 | Equiv |
| 28 | 26/11 | Equiv |
| 29 | 01/12 | Hoare |
| 30 | 03/12 | Hoare |
| 31 | 08/12 | Hoare |
| 32 | 10/12 | HoareAsLogic |
| 33 | 12/12 | Hoare2 (SÁBADO 10h) |
| 34 | 15/12 | Hoare2 |
| 35 | 16/12 | Hoare2 (QUARTA 16h) |
| 17/12 | Sem aula: Alunos Viajando. | |
| 22/12 | Sem aula: Recesso Natalino | |
| … | ||
| 31/12 | Sem aula: Recesso Natalino | |
| * | 05/01 | Estudo para Avaliação 3. |
| * | 07/01 | Estudo para Avaliação 3. |
| * | 12/01 | Estudo para Avaliação 3. |
| * | 14/01 | Estudo para Avaliação 3. |
| 36 | 19/01 | Avaliação 3: Arquivos .v prontos.
|
| 37 | 21/01 | Avaliação 3: Apresentação Mariana. |
| 38 | 26/01 | Avaliação 3: Apresentação Rafael. |
| 39 | 28/01 | Avaliação 3: Apresentação Heitor. |
| * | 02/02 | Divulgação das notas. |
| * | 04/02 | AF |
| * | 09/02 | Notas Finais da Disciplina. |