Razonamiento asistido por ordenador: estudios de caso con ACL2

A free translation by Chema, a Spanish translator working for Ibidem Group, a Spain-based language service provider (LSP)

An original text written by J Strother Moore, originally published in
https://www.cs.utexas.edu/users/moore/publications/acl2-books/acs/index.html

* * *

• Descripción
• Colaboradores
• Índice y extractos (pdf .6Mb) (ps 1.3Mb)
• Erratas
• Material de apoyo para los estudios de caso (incluyendo resúmenes y soluciones a los ejercicios)
• Información para hacer pedidos

Descripción

Este libro muestra cómo el sistema de razonamiento asistido por ordenador ACL2 puede utilizarse de forma productiva e innovadora para diseñar, construir y mantener sistemas de hardware y software. Se incluyen aquí artículos técnicos escritos por veintiún colaboradores que informan sobre estudios de caso, siendo algunos proyectos industriales `”viables”. Tratan de una amplia variedad de ideas, como la aritmética de punto flotante, la simulación de microprocesadores, la comprobación de modelos, la evaluación simbólica de trayectorias, la compilación, la comprobación de pruebas, el análisis real y otros.

El libro se dirige a dos públicos: los que buscan formas innovadoras de diseñar, construir y mantener sistemas de hardware y software de forma más rápida y fiable, y los que desean aprender a hacerlo. El primer grupo incluye a los gestores de proyectos y a los estudiantes de cursos orientados a la investigación. El segundo, incluye a los estudiantes y profesionales que buscan enfoques profundos de la ingeniería de hardware y software o métodos formales. El libro puede utilizarse en cursos de postgrado y de grado superior sobre ingeniería del software, métodos formales, diseño de hardware, teoría de la computación, inteligencia artificial y razonamiento automatizado.

El libro se divide en dos partes. La parte I comienza con una discusión sobre el esfuerzo que supone el uso de ACL2. También contiene una breve introducción a la lógica de ACL2 y a su mecanización, que pretende dar al lector los antecedentes suficientes para leer los estudios de caso. En el libro complementario, Computer-Aided Reasoning: An Approach., se puede encontrar una introducción más completa al ACL2.

ACL2 es una versión mejorada y ampliada de ` “Boyer-Moore theorem prover”, Nqthm, adaptada a Common Lisp. aplicativo. Los editores Kaufmann y Moore son los autores del sistema ACL2. (ACL2 puede obtenerse gratuitamente bajo los términos de la Licencia Pública General de GNU en la página web de ACL2, que incluye el código fuente, una extensa documentación en hipertexto además de muchos artículos sobre ACL2 y sus aplicaciones, visitas guiadas al sistema y listas de correo.

El corazón del libro es la Parte II, donde se presentan los estudios de caso. Los estudios de caso cubren una amplia gama de aplicaciones, desde el hardware (por ejemplo, aritmética de punto flotante, lenguajes de descripción de hardware y análisis simbólico de trayectorias) hasta el software (por ejemplo, búsqueda de grafos, compilación y un algoritmo de comprobación de modelos) y más allá (teoría de números y análisis real). Todo ello se realiza en un único marco matemático con soporte mecánico: ACL2.

La solución completa de cada estudio de caso está disponible aquí. Por ejemplo, cuando decimos que uno de los estudios de caso formaliza un multiplicador en coma flotante y lo demuestra correctamente, queremos decir que no sólo puede leer una descripción en inglés del modelo y de cómo se demostró que es correcto, sino que puede obtener todo el contenido formal del proyecto y reproducir las pruebas, si quieres, con tu copia de ACL2. Así pues, este libro es sólo el principio. Si realmente quieres aprender cómo demostrar que un multiplicador de punto flotante o un compilador son correctos, lee los artículos y luego obtén los scripts para reproducir las pruebas. Luego modifícalos y experimenta.

Los estudios de caso contienen ejercicios cuyas soluciones están en la web. Además, los scripts completos de ACL2 necesarios para formalizar los modelos y demostrar todas las propiedades discutidas están en la Web. Si quieres dominar las técnicas utilizadas para realizar un proyecto concreto, haz los ejercicios de los estudios de caso que se parezcan a tu proyecto.

Colaboradores

Esta es la lista de los colaboradores de este volumen junto con la institución a la que pertenecen:

Material de apoyo para los estudios de estudios de caso, incluidas las soluciones a los ejercicios

Los autores de los estudios de caso han facilitado guiones completos para reproducir los resultados presentados. Este “material de apoyo” también contiene las soluciones a los ejercicios de cada estudio de caso. Hay un directorio separado para el material de apoyo de cada caso práctico, que se encuentra en workshops/1999, que puedes descargar de GitHub. Hay un archivo README de nivel superior, y cada subdirectorio contiene un archivo README que explica su contenido.

5. An Exercise in Graph Theory (J Moore; directorio graph/)
El capítulo formaliza y demuestra la corrección de varios algoritmos sencillos para determinar si existe un camino entre dos nodos de un grafo dirigido finito.

6.
Modular Proof: The Fundamental Theorem of Calculus (Matt Kaufmann; directory calculus/)
El capítulo presenta una metodología de demostración modular descendente y la utiliza para formalizar y demostrar el Teorema Fundamental del Cálculo. La estrategia modular funciona tanto para ACL2 como para “ACL2(r)” (lee el capítulo 18); el Teorema Fundamental se demuestra con ACL2(r).

7.
Mu-Calculus Model-Checking (Panagiotis Manolios; directorio mu-calculus/)
El capítulo presenta un desarrollo formal de la sintaxis y la semántica para el Mu-calculus, un verificador de modelos para éste en ACL2, y una discusión de la traducción de otras lógicas temporales al Mu-calculus. Se demuestra que el verificador de modelos es correcto.

8. High-Speed, Analyzable Simulators (David Greve, Matthew Wilding, David Hardin; directory simulator/)

Los modelos de simulación de alta velocidad se desarrollan habitualmente durante el diseño de sistemas de hardware complejos para predecir el rendimiento, detectar fallos de diseño y permitir el codiseño de hardware y software. Escribir un modelo ejecutable de este tipo en ACL2 aporta la ventaja adicional del análisis formal; sin embargo, hay que tener mucho cuidado para construir un modelo ACL2 que sea rápido y analizable. En este capítulo, se describen técnicas para la construcción de simuladores analizables formalmente de alta velocidad en ACL2. Se demuestra su utilidad en un modelo de procesador sencillo.

9. Verification of a Simple Pipelined Machine Model (Jun Sawada; directory pipeline/)
Se define un modelo ACL2 de una máquina canalizada de tres etapas, junto con un modelo de la máquina secuencial correspondiente. A continuación se presenta una prueba de la equivalencia entre ambas máquinas. Y lo que es más importante, el método de descomposición de la prueba se aplica a arquitecturas de canalización mucho más complicadas.

10. The DE Language (Warren Hunt, Jr.; directorio de-hdl/)
El lenguaje DE es un lenguaje de descripción orientado a las ocurrencias que permite la definición jerárquica de máquinas de estado finito al estilo de un lenguaje de descripción de hardware. La sintaxis y la semántica del lenguaje están formalizadas y la formalización se utiliza para demostrar la corrección de un circuito de hardware simple. Estos HDL formales se han utilizado para demostrar las propiedades de diseños mucho más complejos.

11. Using Macros to Mimic VHDL  (Dominique Borrione, Philippe Georgelin, Vanderlei Rodrigues; directorio vhdl/)
El objetivo de este proyecto era formalizar un pequeño subconjunto de comportamiento sintetizable de VHDL, manteniendo en lo posible el valor sintáctico de VHDL y facilitando la verificación mediante simulación simbólica y demostración de teoremas.

12. Symbolic Trajectory Evaluation (Damir A. Jamsek; directorio ste/)
La evaluación simbólica de trayectorias (STE) es una forma de comprobación de modelos basada fundamentalmente en la simulación simbólica. Este capítulo presenta un tratamiento formal de STE, incluyendo pruebas ACL2 de los resultados presentados en el artículo de Seger y Joyce “”A Mathematically Precise Two-Level Formal Hardware Verification Methodology”.

13. RTL Verification : A Floating-Point Multiplier (David M. Russinoff, Arthur Flatau; directory multiplier/)
Este capítulo describe un sistema de verificación mecánica para diseños representados en el lenguaje RTL de Advanced Micro Devices. El sistema consiste en un traductor a ACL2 y una metodología para verificar las propiedades de los programas resultantes utilizando el prover de ACL2. Se demuestra la corrección de un simple multiplicador de punto flotante.

14. Design Verification of a Safety-Critical Embedded Verifier (Piergiorgio Bertoli, Paolo Traverso; directorio embedded/)
Este capítulo muestra el uso de ACL2 para la verificación del diseño de una pieza de software de seguridad crítica, el verificador embebido. El verificador embebido comprueba en línea que cada ejecución de un traductor de seguridad crítica es correcta. El traductor es un componente de un sistema de software utilizado por Union Switch and Signal para construir sistemas de control de trenes.

15. Compiler Verification Revisited (Wolfgang Goerigk; directorio compiler/)
Este estudio ilustra un hecho observado por Ken Thompson en su conferencia del Premio Turing: el código máquina de un compilador correcto puede ser alterado para contener un Caballo de Troya de manera que el compilador pase casi todas las pruebas, incluyendo la llamada “prueba de arranque” en la que compila su propio código fuente con resultados idénticos, y seguir siendo capaz de generar código “malo”. El compilador, la máquina de código objeto y los experimentos se formalizan en ACL2.

16. Ivy: A Preprocessor and Proof Checker for First-Order Logic (William McCune, Olga Shumsky; directory ivy/)
En este estudio de caso, se demuestra que un comprobador de pruebas para la lógica de primer orden es sólido para interpretaciones finitas. Además, el estudio muestra cómo se pueden combinar programas no ACL2 con funciones ACL2 de manera que se puedan demostrar propiedades útiles sobre los programas compuestos. No se demuestra nada sobre los programas no ACL2. En cambio, los resultados de los programas no ACL2 se comprueban en tiempo de ejecución mediante funciones ACL2, y se demuestran las propiedades de estas funciones de comprobación.

17. Knuth’s Generalization of McCarthy’s 91 Function (John Cowles; directorio knuth-91/)
Este capítulo trata de un reto de Donald Knuth para una “prueba por ordenador” de un teorema sobre su generalización de la famosa “función 91” de John McCarthy. La generalización tiene que ver con los números reales, y el caso de estudio utiliza el ACL2 para responder al desafío de Knuth verificando mecánicamente resultados no sólo sobre el campo de todos los números reales, sino también sobre cada subcampo de ese campo.

18. Continuity and Differentiability (Ruben Gamboa; directorio análisis/)
Este capítulo muestra cómo una versión extendida de ACL2 (llamada ACL2(r)) y descrita puede ser utilizada para razonar sobre los números reales y complejos, utilizando un análisis no estándar. Describe algunas modificaciones de ACL2 que introducen los números reales y complejos irracionales en el sistema numérico de ACL2. A continuación, muestra cómo el ACL2 modificado puede demostrar teoremas clásicos del análisis, como los teoremas del valor intermedio y del valor medio.