Lógicas para a Programação e Especificação
Código
11168
Unidade Orgânica
Faculdade de Ciências e Tecnologia
Departamento
Departamento de Informática
Créditos
6.0
Professor responsável
Carla Maria Gonçalves Ferreira, Luís Manuel Marques da Costa Caires
Horas semanais
4
Total de horas
56
Língua de ensino
Português
Objectivos
Saber
Esta unidade ensina conceitos e técnicas avançadas, baseados em lógica construtiva, em que se apoia a produção de software certificado e que suportam o raciocínio rigoroso sobre programas e linguagens de programação. A relação próxima entre programas e demonstrações / provas, chamada a correspondência de Curry-Howard, será revelada e explorada na unidade. Os estudantes conhecerão os modernos fundamentos da teoria de tipos da programação funcional e imperativa, includindo a programação com tipos dependentes, assim como o desenvolvimento integrado de provas de correção.
Fazer
Os estudantes aprendem a desenvolver programas certificados e tipos de dados usando Coq, um assistente de prova de nível industrial, desenvolvido no INRIA, e usado internacionalmente na indústria e academia. Exemplos do tipo de software coberto inclui programas funcionais e imperativos baseados em ADTs, e interpretadores e processadores de linguagens, incluindo verificadores de tipos e compiladores.
Pré-requisitos
Lógica de primeira ordem básica e Teoria de conjuntos básica.
Programação funcional e imperativa.
Algoritmos e estruturas de dados.
Conteúdo
1. Lógica Construtiva Proposições como Tipos/Programas como Provas;A interpretação Curry-Howard;A lógica do Coq. 2. Raciocínio sobre Programas Funcionais com Tipos Dependentes Programas funcionais básicos: listas,ADTs,provas básicas; Tipos dependentes;Tipos indutivos;Propriedades Indutivas; Polimorfismo e funções de ordem superior. Extração de Programas.Táticas em Coq. 3. Raciocínio sobre Interpretadores de Programs Representação de Expressões e Comandos;Especificação da Avaliação: Triplos de Hoare e precondições mais fracas, condições de verificação; Raciocínio sobre programas imperativos que manipulam estruturas de dados. 4. Raciocínio sobre Linguagens de Programação Linguagens funcional simples; Sistemas de tipos; Preservação de Tipos; Linguagem máquina simples; Especificação da Execução; Correção de Compilador. Equivalência; Bisimulação. NB: Todos os capítulos também cobrem noções relevantes do Coq, tais como manipulação de demonstrações, tácicas e automatização de provas.
Bibliografia
Software Foundations, Benjamin C. Pierce, Chris Casinghino, Michael Greenberg, Vilhelm Sjöberg, BrenYorgey, 2012.
The Coq Proof Assistant (http://coq.inria.fr/).
Método de ensino
O ensino está organizado em aulas teóricas (2T) e práticas (2P). Nas aulas teóricas são apresentados os conceitos e discutidas situações problemáticas. Tipicamente, algumas das competências de saber fazer são também exercitadas nas aulas teóricas, de forma a aumentar a ligação entre os conceitos teóricos e a sua aplicação. Nas aulas práticas os alunos discutem e resolvem exercícios propostos pelo docente, usando o assistente de prova Coq de forma intensiva. A avaliação contínua consiste em dois testes (um intermédio, outro no final do semestre) e 1 projeto de desenvolvimento de software, realizado em grupo. São também
apresentados 4 pequenos trabalhos, que deverão ser resolvidos nas aulas laboratoriais (uso de ferramentas). Os alunos que tenham reprovado na avaliação contínua com uma nota igual ou superior a 8 podem tentar fazer o exame final, cuja nota combinada com a dos trabalhos práticos produz a nota final.
Método de avaliação
Componentes de avaliação:
Componente Prática
- TPCs - 30% da nota final
- Para cada aula prática há um conjunto de exercícios propostos. Cada aluno terá que escolher 1 dos exercícios propostos e submeter a resolução até ao final da semana.
- Submeter 9 dos 12 TPCs
- TP - 30% da nota final
- Trabalho prático final (a avaliação inclui a discussão do TP)
Componente Teórica
- Teste Final - 40% da nota final
Nota Final
- O aluno com frequência obtém aprovação se ambas as notas do teste final e do trabalho prático forem iguais ou superiores a 9.5
Frequência
- Obtém frequência à disciplina o aluno que tenha uma nota igual ou superior a 9.5 no trabalho prático.