Plano de Ensino

Ementa:

• • Especificação, desenvolvimento e verificação formal de programas. Provadores de teoremas e assistentes de prova. Lógica de Hoare. Táticas de prova. Automação de provas.

Conteúdo programático:

• • Especificação, desenvolvimento e verificação formal

    • • Desafios da engenharia de software

      • Abordagens formais para engenharia de software

  • Programação funcional em Coq

    • • Tipos enumerados

      • Funções não-recursivas e recursivas

      • Pares, listas e mapeamentos

  • Polimorfismo e funções de alta ordem

    • • Listas e pares polimórficos

      • Função filter, map, e fold

  • Lógica em Coq

    • • Conectivos lógicos

      • Programando com proposições

      • Aplicando teoremas a argumentos

      • Proposições definidas indutivamente

  • Táticas de prova

    • • Prova por simplificação

      • Prova por reescrita

      • Prova por análise de casos

      • Prova por indução

      • Usando evidência em provas

  • Automação de provas

    • • Táticas de alta ordem

      • Definindo novas táticas

  • Formalizando linguagens imperativas

    • • Expressões, variáveis e comandos

  • Lógica de Hoare

    • • Triplas de Hoare

Bibliografia básica:

• • Benjamin Pierce, et al.. Logical foundations.

    • https://softwarefoundations.cis.upenn.edu/lf-current/index.html

  • Benjamin Pierce, et al.. Programming Language Foundations.

    • https://softwarefoundations.cis.upenn.edu/plf-current/index.html

Bibliografia auxiliar:

• • Coq reference manual. https://coq.inria.fr/refman/.