¿Cuáles son las técnicas formales comunes para probar que el código funcional es correcto?

10

Quiero proporcionar pruebas de partes de un programa de Haskell que estoy escribiendo como parte de mi tesis. Hasta ahora, sin embargo, no pude encontrar un buen trabajo de referencia.

El libro introductorio de Graham Hutton Programming in Haskell ( Google Books ), que leí mientras aprendía Haskell, aborda algunas técnicas para razonar sobre programas como

  • razonamiento equitativo
  • utilizando patrones no superpuestos
  • lista de inducción

en el capítulo 13 pero no es muy profundo.

¿Hay algún libro o artículo que pueda recomendar que proporcione una descripción más detallada de las técnicas formales de prueba para Haskell u otro código funcional?

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

Respuestas:

5

Uno de los métodos de facto para probar resultados en la programación funcional es a través del grupo de Richard Bird.

En particular, solicita un enfoque en profundidad o al menos más integral para el razonamiento equitativo y la inducción de listas, y esto se proporciona en Conferencias sobre Programación Funcional Constructiva .

En términos más generales, el texto "Álgebra de programación", de Bird y de Moor, también se ocupa de la corrección de algoritmos funcionales como la optimización y los problemas de programación dinámica.

Si encuentra otros recursos útiles para este problema, menciónelos y quizás podamos convertir esta publicación en una wiki.

Musa Al-hassy
fuente
¡Gracias! Claro, si encuentro más recursos, me aseguraré de agregarlos a mi publicación.
FK82
6

Puedes comenzar con

Los temas incluyen conceptos básicos de lógica, prueba de teoremas asistida por computadora, el asistente de prueba Coq, programación funcional, semántica operativa, lógica de Hoare y sistemas de tipo estático. La exposición está destinada a una amplia gama de lectores, desde estudiantes avanzados hasta estudiantes de doctorado e investigadores. No se asume una formación específica en lógica o lenguajes de programación, aunque será útil un cierto grado de madurez matemática.

Puede omitir (o desglosar) las partes de la teoría del lenguaje de programación y solo aprender a lidiar con las pruebas formales desde el Prefacio hasta los Principios Ind. El libro está muy bien escrito e iluminante.

Entonces es posible que desee continuar con

En este volumen aprenderá cómo especificar y verificar (probar la corrección de) algoritmos de clasificación, árboles de búsqueda binarios, árboles de búsqueda binarios balanceados y colas de prioridad. Antes de usar este libro, debe tener cierta comprensión de estos algoritmos y estructuras de datos, disponibles en cualquier libro de texto de algoritmos de pregrado estándar. Debe comprender todo el material en Software Foundations Volume 1 (Logic Foundations)

Una nota de advertencia: ¡VFA todavía está en versión beta!

Anton Trunov
fuente
(Su segundo enlace dirige al lugar equivocado). Además, hay una programación funcional verificada en Agda ; que usa Agda, formalmente un lenguaje de programación pero usa unicode y, por lo tanto, está más cerca de la notación matemática.
Musa Al-hassy
Corregido, gracias. Sí, he leído VFPiA, pero no es de mi gusto.
Anton Trunov
¡Gracias por su respuesta! Creo que hay una idea falsa. No busco técnicas funcionales para probar algoritmos (como un asistente de prueba), sino técnicas para probar código funcional (por ejemplo, para probar que una implementación funcional de un algoritmo dado es correcta) @ La respuesta MusaAl-hassy está muy cerca de mi respuesta deseada En caso de que me lo perdiera y los libros que citó también cubran este aspecto, ¿le importaría agregar los capítulos relevantes?
FK82
@ FK82 Aquí está una Theorem app_assoc : ∀ l1 l2 l3 : natlist, (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)de la listas capítulo. ¿Este ejemplo se parece a lo que le interesa? Comienzan con la programación funcional en Coq, pero luego continúan con el razonamiento sobre las propiedades de los programas funcionales. Los capítulos desde el Prefacio hasta IndPrinciples cubren ambos, y yo diría que la programación y el razonamiento están entrelazados allí.
Anton Trunov
1
@ FK82 (1) Estoy totalmente de acuerdo con este comentario. (2) Es posible que desee ver el libro "Pensando funcionalmente con Haskell" (2015) de R. Bird. El libro tiene toneladas de ejemplos de razonamiento sobre Haskell. (3) Además, "Perlas de diseño de algoritmo funcional" (2010) del mismo autor puede ser de alguna ayuda para usted.
Anton Trunov
5

Resulta que una excelente fuente de técnicas de prueba y ejemplos para probar cosas sobre lenguajes funcionales puros son los asistentes de pruebas que generalmente incluyen como parte de su lenguaje de especificación un lenguaje funcional puro sobre el cual es posible razonar de manera equitativa.

Es posible que desee consultar un libro como Programación certificada con tipos dependientes para una introducción en profundidad a este tipo de razonamiento en un asistente de prueba específico, a saber, Coq.

cody
fuente
¡Gracias! De hecho, estoy buscando específicamente técnicas en Haskell . Mi publicación fue editada para incluir todo el código funcional, pero eso está muy por encima de mis intenciones.
FK82
1
No conozco los sistemas diseñados para verificar Haskell específicamente, pero me gustaría señalar que 1) El núcleo funcional de Coq (y Agda) es esencialmente indistinguible del de Haskell (excepto por la restricción a las funciones totales ) y 2) Programas verificados en Coq y Agda se pueden extraer a Haskell (aunque creo que la extracción a Haskell se admite mejor en Agda, donde Coq está más centrada en Ocaml)
cody
¡Bueno saber! Sin embargo, esto implicaría que reescribo mi programa (o las partes relevantes) en Coq o Agda. No creo que sea razonable en mi caso.
FK82
Hay un par de "front-end" muy experimentales que intentan convertir a Haskell a Isabelle o probar directamente las equivalencias con Isabelle, pero no mantendría demasiado stock en su madurez. Creo que reescribir el código en última instancia sería menos trabajo.
cody