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 Formal: cálculo proposicional, sintaxe, semântica, métodos de prova; cálculo de predicados de primeira ordem, noções intuitivas de correção e completude. Verificação de Programas: 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 algoritmos.

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.
• Z. Manna, R. Waldinger, The Logical Basis for Computer Programming, vol.1 (Deductive Reasoning), Addison-Wesley, 1985.
• K. BrodaBroda, S. Eisenbach, H. Khoshnevisan, S. Vickers, Reasoned Programming, Prentice Hall, 1994.

OBSERVAÇÃO:  Disciplina obrigatória no currículo do BCC.

[Veja dados da disciplina no JúpiterWeb]