| Isabelle | |
|---|---|
| Tipo de | demostrador de teoremas |
| Desarrollador | paulson |
| Escrito en | poli/ML ; Scala |
| Sistema operativo | GNU/Linux [1] , Microsoft Windows [1] y macOS [1] |
| Primera edición | 1 de mayo de 1989 |
| plataforma de hardware | multiplataforma |
| ultima versión | Isabelle2021-1 (diciembre 2021 ) |
| Estado | activo |
| Licencia | BSD |
| Sitio web | isabelle.in.tum.de |
Isabelle es una herramienta de prueba automática interactiva que utiliza una lógica de orden superior . Se implementa con el mismo estilo que una de las primeras herramientas de este tipo: LCF y, al igual que LCF, se escribió originalmente en su totalidad en Standard ML [2] . El sistema contiene un núcleo lógico compacto, que puede aceptarse como verdadero sin evidencia adicional (aunque esto no es necesario). Como herramienta general, implementa una metalógica ( teoría de tipos débiles ) que se utiliza para implementar varias variantes de la lógica de objetos de Isabelle, como la lógica de primer orden (FOL), la lógica de orden superior (HOL) o la teoría de conjuntos de Zermelo-Fraenkel. (ZFC). La variante de lógica de objetos más utilizada es Isabelle / HOL, y se llevaron a cabo desarrollos bastante serios en el campo de la teoría de conjuntos utilizando Isabelle / ZF.
El método principal para implementar la prueba de Isabelle es una variante de resolución de orden superior basada en un algoritmo de unificación de orden superior . Al ser un sistema interactivo, Isabelle también incluye potentes herramientas de razonamiento automático, como un motor de reescritura de términos , un solucionador de tablas analíticas , solucionadores de factibilidad externos para problemas en varias teorías conectadas a través de una interfaz de complemento externa Sledgehammer especializada, así como prueba de teoremas automática externa. herramientas. , como E y SPASS . Isabelle se ha utilizado para formalizar numerosos teoremas de las matemáticas y la informática, como el teorema de completitud de Gödel , la prueba de la independencia del axioma de elección de Gödel , el teorema sobre la distribución de números primos . Isabelle también se ha utilizado para probar la corrección formal de los protocolos criptográficos y las propiedades de la semántica de los lenguajes de programación.
Muchas de las pruebas formales obtenidas con Isabelle están disponibles públicamente y se almacenan en el Archivo de Pruebas Formales , que contiene (a partir de 2019) al menos 500 artículos, incluidas más de 2 millones de líneas de código [3] .
Distribuido libremente bajo la licencia BSD . Autor - Lawrence Paulson ( ing. Lawrence Paulson ), el nombre se le da en honor a la hija de Gerard Huet [4] .
El sistema le permite escribir pruebas en dos estilos: procesal y declarativo . El estilo procesal de prueba especifica la secuencia de aplicación de tácticas y procedimientos de prueba. Esto corresponde al estilo en el que suelen trabajar los matemáticos comunes, pero tales demostraciones suelen ser bastante difíciles de entender, ya que al leerlas, el resultado que se planea obtener como resultado de tal demostración no es obvio.
Las pruebas declarativas implementadas en un lenguaje de prueba incorporado especial, Isar, especifican los procedimientos matemáticos específicos que deben aplicarse. Son más fáciles de leer y comprobar por las personas.
En versiones recientes de Isabelle, el estilo de prueba procedimental ha quedado obsoleto. El Archivo de Pruebas Formales también recomienda que las pruebas se presenten en un estilo declarativo [5] .
Un ejemplo de una prueba declarativa de lo contrario, escrita en Isar (la prueba confirma la irracionalidad de la raíz cuadrada de dos):
teorema sqrt2_not_rational: "sqrt (real 2) ∉ ℚ" prueba sea ?x = "sqrt (real 2)" suponga "?x ∈ ℚ" luego obtenga mn :: nat donde sqrt_rat: "¦?x¦ = real m / real n" y términos_más bajos: "coprime m n" por (regla Rats_abs_nat_div_natE) por lo tanto "real (m^2) = ?x^2 * real (n^2)" por (auto simp add: power2_eq_square) por lo tanto eq: "m^2 = 2 * n^2" usando of_nat_eq_iff power2_eq_square por fastforce por lo tanto "2 dvd m^2" por simp por lo tanto "2 dvd m" por simp tiene "2 dvd n" prueba - de ‹2 dvd m› obtener k donde "m = 2 * k" .. con eq tiene "2 * n^2 = 2^2 * k^2" por simp , por lo tanto, "2 dvd n^2" por simp , por lo tanto, "2 dvd n" por simp qed con ‹ 2 dvd m › tener "2 dvd gcd m n" por (regla gcd_greatest) con términos_más bajos tener " 2 dvd 1" por simp por lo tanto Falso usando odd_one por blast qed
Isabelle se ha utilizado muchas veces para implementar métodos formales en la especificación, desarrollo y verificación de sistemas de software y hardware.
En 2009, los desarrolladores del proyecto L4.verified , que se implementó en el centro de investigación australiano NICTA , proporcionaron por primera vez una prueba formal de la corrección funcional del kernel del sistema operativo de propósito general, a saber, el microkernel seL4. (una versión integrada segura de L4 capaz de trabajar en tiempo real) [6] . La prueba fue construida y verificada por Isabelle/HOL; contiene más de 200 mil líneas de script de verificación para verificar 7500 líneas de código C. La verificación cubre el código, el diseño y la implementación.[ especificar ] . Como parte de la prueba, se demostró que el código C implementa correctamente la especificación formal del kernel. La prueba reveló 144 errores en el código C del kernel seL4 inicial y alrededor de 150 problemas en la arquitectura y la especificación del propio kernel.
Para el lenguaje de programación Java ligero usando Isabelle, se obtuvo una prueba de seguridad de tipos [7] .
El autor del sistema Paulson mantiene una lista de proyectos de investigación [8] que utilizan Isabelle.
Hay una serie de sistemas automáticos de prueba de teoremas similares en capacidades a Isabelle , que incluyen: