Razonamiento asistido por computadora: un enfoque

Original en inglés: http://www.cs.utexas.edu/users/moore/publications/acl2-books/car/

Matt Kaufmann, Panagiotis Manolios y J Strother Moore, Kluwer Academic Editores, junio de 2000. (ISBN 0-7923-7744-3)

Descripción

Este libro es una introducción al libro de texto del razonamiento asistido por computadora. Se puede utilizar en cursos de pregrado y de la división superior en ingeniería del software o métodos formales. También es adecuado junto con otros libros en cursos sobre Diseño de hardware, Matemáticas discretas o Teoría, especialmente cursos que enfatizan el formalismo, el rigor o el soporte mecanizado. También es apropiado para cursos sobre Inteligencia Artificial o Razonamiento Automatizado.

Los sistemas actuales de hardware y software a menudo son muy complejos y la tendencia es hacia una mayor complejidad. Al modelar matemáticamente los sistemas, obtenemos modelos que podemos demostrar que se comportan correctamente. Para aumentar aún más la confianza en nuestro razonamiento, que puede ser complejo, podemos utilizar un programa de computadora para verificar nuestras pruebas e incluso automatizar parte de su construcción.

En este libro presentamos:

  • Un lenguaje de programación funcional y práctico estrechamente relacionado con Common Lisp que se usa para definir funciones (que pueden modelar sistemas informáticos) y para hacer afirmaciones sobre funciones definidas.
  • Una lógica formal en la cual las funciones definidas corresponden a axiomas; la lógica es de primer orden, incluye inducción, y nos permite probar teoremas sobre las funciones.
  • El sistema de razonamiento asistido por computadora ACL2, que incluye el lenguaje de programación, la lógica y el soporte mecánico para el proceso de prueba.

Este libro le enseñará cómo formalizar cosas, cómo construir pruebas y cómo usar una herramienta mecánica para verificar esas pruebas.

Usamos un formalismo particular y una mecanización particular de él, a saber, ACL2, que está disponible libremente bajo los términos de una licencia de estilo BSD del Página de inicio de ACL2. ACL2 fue escrito por Kaufmann y Moore y es el sucesor del “ teorema de Boyer-Moore ” Nqthm. (Bob Boyer también hizo importantes contribuciones tempranas a ACL2.) La página de inicio de ACL2 incluye el manual de referencia en línea, que es un gran documento de hipertexto destinado principalmente a los usuarios del sistema. Este libro es la introducción definitiva a ACL2 y cómo usarlo.

Mientras enseñamos el uso del formalismo mecanizado, nos enfocamos en problemas computacionales del tipo que típicamente enfrentan los que usan métodos formales para analizar hardware o software.

ACL2 se usa en la industria. ¿Recuerda el error de Intel FDIV? La primera marca Pentium [Intel, Inc.] no pudo dividir los números de coma flotante correctamente y, según los informes, le costó a Intel $ 500 millones reparar. En ese momento, utilizamos ACL2 para verificar que el microcódigo de división de punto flotante en el microprocesador competidor de AMD, el AMD-K5, era correcto. AMD usó ACL2 para verificar las operaciones elementales de punto flotante para el Athlon lanzado recientemente. [Nota: AMD, el logotipo de AMD y sus combinaciones, AMD-K5, AMD-K7 y AMD Athlon son marcas comerciales de Advanced Micro Devices, Inc.] Volumen acompañante presenta un estudio de caso estrechamente relacionado.

El sistema ACL2 se ha aplicado con éxito a proyectos de interés comercial, incluidos el modelado de microprocesadores, la verificación de hardware, la verificación de microcódigos y la verificación de software. Este libro proporciona una metodología para modelar sistemas informáticos formalmente y para razonar sobre esos modelos con asistencia mecanizada. La practicidad del razonamiento asistido por computadora se demuestra adicionalmente en el libro complementario, Razonamiento asistido por computadora: estudios de caso ACL2.