Existem sistemas de verificação formal anotados para linguagens de programação funcionais puras?

25

ACSL (Ansi C Specification Language), é uma especificação para código C, anotada com comentários especiais, que permite que o código C seja formalmente verificado.

Ainda não examinei, mas imagino que os métodos formais usados ​​nos verificadores ACSL seriam semelhantes ao Hoare Logic. Porém, para linguagens funcionais puras, como Haskell, não consigo imaginar que tipo de formalismo seria usado para verificação formal.

Alguém já fez algo semelhante ao ACSL , mas para uma linguagem funcional pura? Caso contrário, houve alguma pesquisa sobre a verificação formal de estilo anotado por especificação para linguagens funcionais?

Eu sei que há digitação dependente, suportada por muitos idiomas (Agda, Idris, etc ...), mas na digitação dependente de Haskell é difícil sem fazer alguma tipo de magia (ilegível?). Com isso em mente, e como Haskell tem um suporte de biblioteca muito melhor do que Agda e Idris, acredito que esse sistema de verificação formal funcional possa ser útil, mas não sei se foram feitas pesquisas sobre isso ou não.

Nathan BeDell
fonte

Respostas:

13

Honda e Yoshida

(provavelmente) foi pioneiro nas lógicas Hoare para linguagens puramente funcionais. Este trabalho é baseado na lógica de Hennessy-Milner e na codificação de funções de Milner em processos, conforme descrito aqui:

O trabalho de Régis-Gianas e cols. Mencionado em outra resposta é semelhante ao primeiro trabalho acima de Honda / Yoshida. Isso foi estendido para linguagens eficazes no estilo ML:

As lógicas mencionadas são chamadas de observacionalmente completas, o que significa que a semântica operacional e a lógica coincidem. Arthur Charguéraud usou isso como complemento para seu trabalho na verificação de programas funcionais no estilo Hoare, na Coq.

Martin Berger
fonte
15

F

Parece haver uma correspondência estreita entre os tipos de refinamento e as notações do tipo ACSL.

Finalmente, só posso sugerir uma análise mais detalhada da Agda e do Idris, pois eles podem ser compilados com o Haskell, e visam fornecer ao usuário uma linguagem de programação utilizável (especialmente o Idris). Eu suspeito que é possível integrar bibliotecas Haskell no código Idris sem muitos problemas.

cody
fonte
sem muita dificuldade - na verdade não. Idris é rigoroso por padrão e Haskell é preguiçoso; isso por si só se apresenta como um grande problema. A compatibilidade com Haskell também nunca foi uma prioridade muito alta para o design de Idris.
Bartek Banachewicz 10/10
Justo. A Agda verifica a rescisão por padrão, portanto, coisas como rigor não são um problema em teoria . É claro que o tempo de execução pode ser dramaticamente diferente.
Cody
8

Há um documento no ICFP deste ano , tipos de refinamento para Haskell . O documento trata da verificação de terminação em vez da lógica completa do Hoare, mas espero que seja um começo nessa direção.

A seção de trabalho relacionada nesse documento contém alguns indicadores, como a verificação estática do contrato de Xu, Peyton-Jones e Claessen para Haskell e Sonnex, Drossopoulou e Zeno e Vytiniotis de Eisenbach, Peyton-Jones, Claessen e Halo de Rosen .

Ohad Kammar
fonte
1

Nosso trabalho sobre verificação suave de contratos está relacionado, no OOPSLA 2012 e no ICFP 2014 , permite que você escreva contratos, que são muito parecidos com as especificações do ACSL, e depois os verifique estaticamente ou use uma verificação dinâmica em tempo de execução.

Sam Tobin-Hochstadt
fonte