MAC0239 Introdução à Logica e Verificação de Programas
Por | EmAté 2014 se chamou MAC0239 Métodos Formais em Programação
OBJETIVOS: Dar ao aluno o primeiro contato com métodos formais. Introduzir conceitos básicos para a verificação formal, assim como técnicas de demonstração de corretude de programas.
PROGRAMA: Lógica Proposicional Clássica: Os conectivos Booleanos e a linguagem da LPC. Semântica clássica. Tabelas da Verdade. Implicação Lógica. Equivalência Lógica e formas normais. Métodos de prova e inferência lógica, tais como Axiomatizações, Dedução Natural e métodos de Tableaux. Noções sobre correção e completude. Algoritmo ingênuo e não-determinístico de decisão da satisfazibilidade (SAT). Lógica de Primeira Ordem: Linguagem, e semântica em termos de estruturas relacionais. Implicação Lógica, Equivalência Lógica e forma normal prenex. Extensão dos Métodos de prova e inferência lógica para LPO, tais como Axiomatizações. Dedução Natural e métodos de Tableaux. Verificação de Programas pelo método Lógica de Hoare extendendo LPO: Semântica axiomática dos comandos básicos de programação. Lógica de Hoare. Pré- e pós-condições. Comandos nulos, atribuição, seleção, iteração; Invariantes. Terminação. Exemplos clássicos de provas de correção parcial e correção total de programas.
RESPONSÁVEIS: Ana Cristina Vieira de Melo, Flávio Soares Correa da Silva, Marcelo Finger, Leliane Nunes de Barros, Renata Wasserman.
PRÉ-REQUISITOS: MAC0110.
CARGA HORÁRIA SEMANAL E NÚMERO DE CRÉDITOS: 4 horas, 4 créditos-aula.
CRITÉRIO DE AVALIAÇÃO DA APRENDIZAGEM: Provas e exercícios.
BIBLIOGRAFIA BÁSICA:
- D. Gries, The Science of Programming, Springer-Verlag, 1981.
- F.S.C. da Silva, M. Finger, A.C.V. de Melo, Lógica para Computação, Cengage Learning, 2006.
- M. Huth, M. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, 2nd ed., Cambridge University Press, 2004.
OBSERVAÇÃO: Disciplina obrigatória no currículo do BCC.
[Veja dados da disciplina no JúpiterWeb]