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