MAC0239  Introdução à Logica e Verificação de Programas

Até 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.

PRÉ-REQUISITOS:  MAC0121.

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]