¿Hay algún sistema de verificación formal anotado para lenguajes de programación puramente funcionales?

25

ACSL (Ansi C Specification Language), es una especificación para el código C, anotada con comentarios especiales, que permite verificar formalmente el código C.

No lo he investigado , pero imagino que los métodos formales utilizados en los verificadores ACSL serían similares a Hoare Logic. Sin embargo, para los lenguajes funcionales puros, como Haskell, no puedo imaginar qué tipo de formalismo se usaría para la verificación formal.

¿Alguien ha hecho algo similar a ACSL , pero para un lenguaje funcional puro? De no ser así, ¿se ha realizado alguna investigación sobre la verificación formal de estilo con anotaciones de especificación para lenguajes funcionales?

Sé que hay una escritura dependiente, que son compatibles con muchos idiomas (Agda, Idris, etc.), pero en Haskell la escritura dependiente es difícil sin hacer algún tipo de hechicería (¿ilegible?). Con eso en mente, y dado que Haskell tiene un soporte de biblioteca mucho mejor que Agda e Idris, creo que tal sistema para la verificación formal funcional podría ser útil, pero no sé si se ha realizado una investigación sobre esto o no.

Nathan BeDell
fuente

Respuestas:

13

Honda y Yoshida

(probablemente) fue pionero en la lógica de Hoare para lenguajes puramente funcionales. Este trabajo se basa en la lógica de Hennessy-Milner y la codificación de funciones de Milner en procesos, como se describe aquí:

El trabajo de Régis-Gianas et al mencionado en otra respuesta es similar al primer trabajo anterior de Honda / Yoshida. Esto se ha extendido a lenguajes efectivos de estilo ML:

Las lógicas mencionadas son lo que se llama observacionalmente completo, lo que significa que la semántica operativa y la lógica coinciden. Arthur Charguéraud utilizó esta completa para su trabajo en la verificación de programas funcionales al estilo Hoare en Coq.

Martin Berger
fuente
15

F

Parece haber una estrecha correspondencia entre los tipos de refinamiento y las anotaciones de tipo ACSL.

Finalmente, solo puedo sugerir que eche un vistazo más de cerca a Agda e Idris, ya que pueden compilar a Haskell, y tienen como objetivo proporcionar al usuario un lenguaje de programación utilizable (especialmente Idris). Sospecho que es posible integrar las bibliotecas de Haskell en el código Idris sin demasiados problemas.

cody
fuente
sin demasiados problemas , en realidad no. Idris es estricto por defecto, y Haskell es vago; eso solo se plantea como un gran problema. La compatibilidad con Haskell nunca fue una prioridad muy alta para el diseño de Idris.
Bartek Banachewicz
Lo suficientemente justo. Sin embargo, Agda verifica la terminación de forma predeterminada, por lo que cosas como la rigidez no son un problema en teoría . Por supuesto, el tiempo de ejecución podría ser dramáticamente diferente.
cody
8

Hay un artículo en ICFP de este año , tipos de refinamiento para Haskell . El documento trata de la verificación de terminación en lugar de la lógica completa de Hoare, pero es de esperar que sea un comienzo en esta dirección.

La sección de trabajo relacionada en ese documento contiene algunos indicadores, como Xu, Peyton-Jones y la comprobación estática del contrato de Claessen para Haskell , y Sonnex, Drossopoulou y Zeno y Vytiniotis de Eisenbach, Peyton-Jones, Claessen y Halo de Rosen .

Ohad Kammar
fuente
1

Nuestro trabajo en la verificación suave de contratos está relacionado, en OOPSLA 2012 e ICFP 2014 , le permite escribir contratos, que son muy parecidos a las especificaciones de ACSL, y luego verificarlos estáticamente o usarlos una verificación dinámica en tiempo de ejecución.

Sam Tobin-Hochstadt
fuente