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.
Véase también el trabajo de tesis doctoral de Yann Régis-Gianas con François Pottier: una lógica de Hoare para los programas funcionales de llamada por valor (MPC'08) . Este trabajo se extendió para cubrir los efectos secundarios habituales de ML por Johannes Kanig y Jean-Cristophe Filliatre en 2009: Who: A Verifier for Effective Higher-Order Order Programs .
fuente
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 .
fuente
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.
fuente