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

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.

Honda e Yoshida

• Uma lógica de programa composicional para funções polimórficas de ordem superior

(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:

• Da lógica de processo à lógica de programa

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:

• Uma lógica de programa observacionalmente completa para funções imperativas de ordem superior

• Uma análise lógica do aliasing em funções imperativas de ordem superior

• Raciocínio lógico para funções de ordem superior com estado local

• Lógicas de programas para controle seqüencial de ordem superior

• Lógicas de programas para metaprogramação homogênea

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.

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

Veja também o trabalho de tese de doutorado de Yann Régis-Gianas com François Pottier: Uma lógica Hoare para programas funcionais de chamada por valor (MPC'08) . Este trabalho foi estendido para cobrir os efeitos colaterais usuais de ML por Johannes Kanig e Jean-Cristophe Filliatre em 2009: Quem: Um Verificador para Programas Efetivos de Alta Ordem .

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 .

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.