Reseña: Proof pearl – A mechanized proof of GHC’s mergesort
Se publicado un artículo de verificación en Iabelle/HOL titulado Proof pearl – A mechanized proof of GHC’s mergesort.
Su autor es Christian Sternagel (de la Univ. de la Univ. de Insbruck).
Su resumen es
We present our Isabelle/HOL formalization of GHC’s sorting algorithm for lists, proving its correctness and stability. This constitutes another example of applying a state-of-the-art poof assistant to real-world code. Furthermore, it allows users to take advantage of the formalized algorithm in generated code.
La librería estándard de GHC (The Glasgow Haskell Compiler) tiene un algoritmo de ordenación, que es una variante de la ordenación por mezcla. El objetivo del trabajo es la verificación de dicho algortimo en Isabelle/HOL, demostrando su corrección y estabilidad.
La principal característica de este trabajo es la verificación de programas eficientes. El método empleado tiene tres pasos:
- formalizar variantes del algoritmo que faciliten la demostración y probar todas las propiedades deseadas;
- formalizar variantes eficientes del algoritmo y probar su equivalencia y
- usar la generación de código y obtener un programa eficiente del que se tiene garantía que satisface todas las propiedades que se probaron en la formalización inicial.
La formalización es pequeña (menos de 400 líneas de código) y la mayoría de las demostraciones son automáticas. Este éxito se basa en dos principios: la generalización de los conceptos y la definición de esquemas de inducción.
El código en Isabelle/HOL de la teoría correspondiente al trabajo se encuentra en The Archive of Formal Proofs.