Disciplina
Informações da Disciplina

 Preparar para impressão 
Júpiter - Sistema de Graduação

Instituto de Matemática e Estatística
 
Ciência da Computação
 
Disciplina: MAC0239 - Introdução à Lógica e Verificação de Programas

Créditos Aula: 4
Créditos Trabalho: 0
Tipo: Semestral

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.
 
Docente(s) Responsável(eis)
Flavio Soares Correa da Silva
Leliane Nunes de Barros
Marcelo Finger
Renata Wassermann
 
Programa Resumido
 
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.
 
Avaliação
 
      Método
     
 
      Critério
      Provas e exercícios
 
      Norma de Recuperação
     
 
Bibliografia
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.
 
Requisitos
Os Requisitos variam conforme o curso para o qual ela é oferecida.

Clique para consultar o oferecimento para MAC0239.

Créditos | Fale conosco
© 1999 - 2024 - Superintendência de Tecnologia da Informação/USP