KeY

La herramienta KeY se utiliza en la verificación formal de programas Java. Acepta especificaciones escritas en el Java Modeling Language para archivos fuente de Java. Estas se transforman en teoremas de lógica dinámica y luego se comparan con la semántica del programa que también se define en términos de lógica dinámica. KeY es significativamente poderoso en que admite tanto pruebas de corrección interactivas (es decir, manuales) como totalmente automatizadas. Los intentos de prueba fallidos se pueden usar para una depuración o pruebas basadas en verificación más eficientes. Ha habido varias extensiones a KeY para aplicarlo a la verificación de programas C o sistemas híbridos. KeY es desarrollado conjuntamente por el Karlsruhe Institute of Technology, Alemania; Technische Universität Darmstadt, Alemania; y Chalmers University of Technology en Gotemburgo, Suecia, y tiene licencia GPL. Overview La entrada de usuario habitual a KeY consiste en un archivo fuente de Java con anotaciones en JML. Ambos se traducen a la representación interna de KeY, lógica dinámica. A partir de las especificaciones dadas, surgen varias obligaciones de prueba que deben descargarse, es decir, debe encontrarse una prueba. Para ello, el programa se ejecuta simbólicamente y los cambios resultantes en las variables del programa se almacenan en las llamadas actualizaciones. Una vez que el programa se ha procesado completamente, queda una obligación de prueba de lógica de primer orden. En el corazón del sistema KeY se encuentra un demostrador de teoremas de primer orden basado en cálculo de secuentes, que se utiliza para cerrar la prueba. Las reglas de interferencia se capturan en los llamados taclets que consisten en un lenguaje simple propio para describir cambios a un secuente. Java Card DL La base teórica de KeY es una lógica formal llamada Java Card DL. DL significa Dynamic Logic. Es una versión de una lógica dinámica de primer orden adaptada a programas Java Card. Como tal, permite, por ejemplo, afirmaciones (fórmulas) como , que dice intuitivamente que la poscondición debe cumplirse en todos los estados del programa alcanzables ejecutando el programa Java Card en cualquier estado que satisfaga la precondición . Esto es equivalente a en el cálculo de Hoare si y son puramente de primer orden. Sin embargo, la lógica dinámica extiende la lógica de Hoare en que las fórmulas pueden contener modalidades de programa anidadas como , o que es posible la cuantificación sobre fórmulas que contienen modalidades. También existe una modalidad dual que incluye la terminación.