Quais são as técnicas formais comuns para provar o código funcional correto?

10

Quero fornecer provas para partes de um programa Haskell que estou escrevendo como parte de minha tese. Até agora, porém, não consegui encontrar um bom trabalho de referência.

O livro introdutório de Graham Hutton, Programming in Haskell ( Google Books ) - que li enquanto aprendia Haskell - aborda algumas técnicas para raciocinar sobre programas como

  • raciocínio equacional
  • usando padrões não sobrepostos
  • lista de indução

no capítulo 13, mas não é muito aprofundado.

Você pode recomendar livros ou artigos que forneçam uma visão geral mais detalhada das técnicas formais de prova para Haskell, ou outro código funcional?

reference-request proof-techniques functional-programming books software-verification FK82
fonte

Respostas:

5

Um dos métodos de fato para provar resultados em programação funcional é através do grupo de Richard Bird.

Em particular, você solicita uma abordagem aprofundada ou pelo menos mais abrangente ao raciocínio equacional e à indução de lista, e isso é fornecido em Palestras sobre Programação Funcional Construtiva .

De maneira mais geral, o texto "Álgebra de programação", de Bird e de Moor, também lida com a correção de algoritmos funcionais, como otimização e problemas de programação dinâmica.

Se você encontrar outros recursos úteis para esse problema, mencione-os e talvez possamos transformar esta postagem em um wiki.

Musa Al-hassy
fonte
Obrigado! Claro, se eu encontrar mais recursos, terei certeza de adicioná-los à minha postagem.
FK82 12/09/16
6

Você pode começar com

Os tópicos incluem conceitos básicos de lógica, prova de teorema assistido por computador, assistente de prova Coq, programação funcional, semântica operacional, lógica Hoare e sistemas de tipo estático. A exposição é destinada a uma ampla gama de leitores, de graduandos avançados a estudantes de doutorado e pesquisadores. Nenhum background específico em lógica ou linguagem de programação é assumido, embora um certo grau de maturidade matemática seja útil.

Você pode pular (ou pular) as partes da teoria da linguagem de programação e aprender apenas como lidar com provas formais, começando do Prefácio até os IndPrinciples. O livro é realmente bem escrito e esclarecedor.

Então você pode continuar com

Neste volume, você aprenderá como especificar e verificar (provar a exatidão de) algoritmos de classificação, árvores de pesquisa binária, árvores de pesquisa binária equilibrada e filas prioritárias. Antes de usar este livro, você deve ter alguma compreensão desses algoritmos e estruturas de dados, disponíveis em qualquer manual de algoritmos de graduação padrão. Você deve entender todo o material do Software Foundations Volume 1 (Logic Foundations)

Uma observação: o VFA ainda está na versão beta!

Anton Trunov
fonte
(Seu segundo link direciona para o lugar errado.) Além disso, há Programação Funcional Verificada no Agda ; que usa Agda, formalmente uma linguagem de programação, mas usa unicode e, portanto, está mais próximo da notação matemática.
Musa Al-hassy
Corrigido, obrigado. Sim, eu li VFPiA, mas não é do meu gosto.
Anton Trunov
Obrigado pela sua resposta! Eu acho que há um equívoco. Não estou procurando técnicas funcionais para provar algoritmos (como um assistente de prova), mas técnicas para provar código funcional (por exemplo, para provar uma implementação funcional de um determinado algoritmo correto). resposta desejada. Caso eu tenha perdido, e os livros que você citou também abrangem esse aspecto, você se importaria de adicionar os capítulos relevantes?
FK82 17/09/16
@ FK82 Aqui está um capítulo Theorem app_assoc : ∀ l1 l2 l3 : natlist, (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)do Lists . Este exemplo é parecido com o que você está interessado? Eles começam com a programação funcional no Coq, mas depois passam a raciocinar sobre as propriedades dos programas funcionais. Os capítulos de Prefácio até IndPrinciples cobrem os dois, e eu diria que programação e raciocínio estão entrelaçados lá.
Anton Trunov
11
@ FK82 (1) Concordo totalmente com este comentário. (2) Você pode consultar o livro "Pensando funcionalmente com Haskell" (2015), de R. Bird. O livro tem vários exemplos de raciocínio sobre Haskell. (3) Além disso, "Pearls of Functional Algorithm Design" (2010) do mesmo autor pode ser de alguma ajuda para você.
Anton Trunov
5

Acontece que uma excelente fonte de técnicas de prova e exemplos para provar coisas sobre linguagens funcionais puras são assistentes de prova que geralmente incluem como parte de sua linguagem de especificação uma linguagem funcional pura na qual é possível raciocinar de maneira equitativa.

Pode-se consultar um livro como Programação Certificada com Tipos Dependentes para obter uma introdução detalhada a esse tipo de raciocínio em um assistente de prova específico, chamado Coq.

cody
fonte
Obrigado! Na verdade, estou procurando especificamente técnicas em Haskell . Minha postagem foi editada para incluir todo o código funcional, mas isso está muito acima das minhas intenções.
FK82 17/09/16
11
Não conheço sistemas projetados para verificar Haskell especificamente, mas gostaria de observar que 1) O núcleo funcional da Coq (e Agda) é essencialmente indistinguível do de Haskell (exceto a restrição ao total de funções) e 2) Programas verificados em Coq e Agda pode ser extraída para Haskell (embora acredito extracção de Haskell é melhor suportada em Agda, onde é mais Coq Ocaml-centrada)
Cody
Bom saber! No entanto, isso implicaria que eu reescrevesse meu programa (ou as partes relevantes) no Coq ou no Agda. Eu não acho isso razoável no meu caso.
FK82
Existem alguns "front-ends" muito experimentais que tentam converter Haskell em Isabelle ou provar diretamente equivalências usando Isabelle, mas eu não teria muito estoque em sua maturidade. Acho que reescrever o código acabaria sendo menos trabalhoso.
Cody
4

Eu sugiro usar a lógica do programa. Eles lidam muito melhor com efeitos do que com sistemas de digitação.

Existem inúmeras lógicas de programa para linguagens funcionais. Isso se torna interessante com efeitos. Consulte, por exemplo, Raciocínio lógico para funções de ordem superior com estado local .

O trabalho de Arthur Charguéraud integra a abordagem lógica do programa aos assistentes de prova, consulte, por exemplo, esta página de visão geral .

Martin Berger
fonte