Llave

La herramienta KeY se utiliza en la verificación formal de programas Java . Acepta especificaciones escritas en el lenguaje de modelado Java en archivos fuente 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 potente ya que admite pruebas de corrección tanto interactivas (es decir, a mano) como totalmente automatizadas. Los intentos de prueba fallidos se pueden utilizar para una depuración más eficiente o una prueba basada en verificación . Ha habido varias extensiones de KeY para aplicarlo a la verificación de programas C o sistemas híbridos . KeY es desarrollado conjuntamente por el Instituto de Tecnología de Karlsruhe , Alemania; la Universidad Técnica de Darmstadt , Alemania; y la Universidad Tecnológica de Chalmers en Gotemburgo, Suecia y tiene licencia GPL .

La entrada habitual del usuario a KeY consiste en un archivo fuente Java con anotaciones en JML. Ambos se traducen a la representación interna de KeY, la lógica dinámica. A partir de las especificaciones dadas, surgen varias obligaciones de prueba que deben cumplirse, 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 por completo, queda una obligación de prueba lógica de primer orden . En el corazón del sistema KeY se encuentra un demostrador de teoremas de primer orden basado en el cálculo de secuencias , 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 los cambios en una secuencia.

La base teórica de KeY es una lógica formal llamada Java Card DL. DL significa lógica dinámica. Es una versión de una lógica dinámica de primer orden adaptada a los programas Java Card. Como tal, por ejemplo, permite declaraciones (fórmulas) como , que dice intuitivamente que la condición posterior debe cumplirse en todos los estados del programa alcanzables al ejecutar el programa Java Card en cualquier estado que satisfaga la condición previa . Esto es equivalente a en el cálculo de Hoare si y son puramente de primer orden. La lógica dinámica, sin embargo, 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 . Esta lógica dinámica puede verse como una lógica multimodal especial (con un número infinito de modalidades) donde para cada bloque de Java hay modalidades y . ${\displaystyle \phi \rightarrow [\alpha ]\psi }$${\estilo de visualización \psi}$${\estilo de visualización \alpha}$${\estilo de visualización \phi}$${\displaystyle \{\phi \}\alpha \{\psi \}}$${\estilo de visualización \phi}$${\estilo de visualización \psi}$${\estilo de visualización [\alfa ]}$${\displaystyle \langle \alpha \rangle }$${\estilo de visualización \alpha}$${\estilo de visualización [\alfa ]}$${\displaystyle \langle \alpha \rangle }$

En el corazón del sistema KeY se encuentra un demostrador de teoremas de primer orden basado en un cálculo de secuentes . Un secuente tiene la forma donde (suposiciones) y (proposiciones) son conjuntos de fórmulas con el significado intuitivo que es verdadero. Por medio de la deducción , se demuestra que un secuente inicial que representa la obligación de prueba es construible a partir de axiomas fundamentales de primer orden (como la igualdad ). ${\displaystyle \Gamma \vdash \Delta }$${\estilo de visualización \Gamma}$${\estilo de visualización \Delta}$${\displaystyle \bigwedge _{\gamma \in \Gamma }\gamma \rightarrow \bigvee _{\delta \in \Delta }\delta }$${\displaystyle e\ {\dot {=}}\ e}$

Durante eso, las modalidades del programa se eliminan mediante ejecución simbólica . Por ejemplo, la fórmula es lógicamente equivalente a . Como muestra este ejemplo, la ejecución simbólica en lógica dinámica es muy similar al cálculo de las precondiciones más débiles . Ambos y denotan esencialmente lo mismo, con dos excepciones: En primer lugar, es una función de algún metacálculo mientras que en realidad es una fórmula del cálculo dado. En segundo lugar, la ejecución simbólica se ejecuta a través del programa hacia adelante tal como lo haría una ejecución real. Para guardar los resultados intermedios de las asignaciones, KeY introduce un concepto llamado actualizaciones , que son similares a las sustituciones pero solo se aplican una vez que se ha eliminado la modalidad del programa. Sintácticamente, las actualizaciones consisten en asignaciones paralelas (sin efectos secundarios) escritas entre llaves delante de una modalidad. Un ejemplo de ejecución simbólica con actualizaciones: se transforma en en el primer paso y en en el segundo paso. La modalidad entonces está vacía y la "aplicación hacia atrás" de la actualización a la poscondición produce una precondición donde podría tomar cualquier valor. ${\displaystyle x\ {\punto {=}}\ 0\rightarrow [x++;]x\ {\punto {=}}\ 1}$${\displaystyle x\ {\punto {=}}\ 0\rightarrow x\ {\punto {=}}\ 0}$${\displaystyle [\alpha ]\psi }$${\displaystyle wp(\alpha,\psi)}$${\estilo de visualización wp}$${\displaystyle [\alpha ]\psi }$${\displaystyle [x=3;x=x+1;]x\ {\punto {=}}\ 4}$${\displaystyle \{x:=3\}[x=x+1;]x\ {\punto {=}}\ 4}$${\displaystyle \{x:=4\}[]x\ {\punto {=}}\ 4}$${\estilo de visualización x}$

Supongamos que uno quiere demostrar que el siguiente método calcula el producto de algunos números enteros no negativos y . ${\estilo de visualización x}$${\estilo de visualización y}$

int foo ( int x , int y ) { int z = 0 ; mientras ( y > 0 ) si ( y % 2 == 0 ) { x = x * 2 ; y = y / 2 ; } de lo contrario { y = y / 2 ; z = z + x ; x = x * 2 ; } devolver z ; }      
       
       
              
              
              
          
              
              
              
        
     

De esta manera, se comienza la demostración con la premisa y la conclusión que se pretende demostrar . Nótese que las tablas de cálculos con secuencias se escriben normalmente "al revés", es decir, la secuencia inicial aparece en la parte inferior y los pasos de deducción van hacia arriba. La demostración se puede ver en la figura de la derecha. ${\displaystyle x\geq 0\land y\geq 0}$${\displaystyle z\ {\punto {=}}\ x\cdot y}$

El depurador de ejecución simbólica visualiza el flujo de control de un programa como un árbol de ejecución simbólica que contiene todas las rutas de ejecución posibles a través del programa hasta un punto determinado. Se proporciona como complemento a la plataforma de desarrollo Eclipse .

KeY se puede utilizar como una herramienta de prueba basada en modelos que puede generar pruebas unitarias para programas Java. El modelo del que se derivan los datos de prueba y el caso de prueba consta de una especificación formal (proporcionada en JML ) y un árbol de ejecución simbólico de la implementación en prueba que se calcula mediante el sistema KeY.

KeY es un software libre escrito en Java y con licencia GPL . Se puede descargar desde el sitio web del proyecto en código fuente; actualmente no hay binarios precompilados disponibles. Como otra posibilidad, KeY se puede ejecutar directamente a través de Java Web Start sin necesidad de compilación e instalación.

KeY-Hoare se basa en KeY y presenta un cálculo de Hoare con actualizaciones de estado. Las actualizaciones de estado son un medio para describir las transiciones de estado en una estructura de Kripke . Este cálculo puede considerarse como un subconjunto del que se utiliza en la rama principal de KeY. Debido a la simplicidad del cálculo de Hoare, esta implementación está destinada esencialmente a ejemplificar métodos formales en clases de pregrado.

KeYmaera [1] (anteriormente llamada HyKeY) es una herramienta de verificación deductiva para sistemas híbridos basada en un cálculo para la lógica dinámica diferencial dL [2]. Amplía la herramienta KeY con sistemas de álgebra computacional como Mathematica y algoritmos y estrategias de prueba correspondientes, de modo que se pueda utilizar para la verificación práctica de sistemas híbridos .

KeYmaera ha sido desarrollado en la Universidad de Oldenburg y la Universidad Carnegie Mellon . El nombre de la herramienta fue elegido como homófono de Quimera , el animal híbrido de la mitología griega antigua.

KeYmaeraX [3], desarrollado en la Universidad Carnegie Mellon , es el sucesor de KeYmaera y ha sido completamente reescrito.

KeY for C es una adaptación del sistema KeY a MISRA C , un subconjunto del lenguaje de programación C. Esta variante ya no recibe soporte.

También existe una adaptación para utilizar KeY para la ejecución simbólica de máquinas de estados abstractos , que se desarrolló en la ETH de Zúrich . Esta variante ya no se admite.

• Verificación de software orientado a objetos: el enfoque KeY. Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt (Eds.). Springer , 2007. ISBN 978-3-540-68977-5 . 
• Verificación deductiva de software: el libro clave: de la teoría a la práctica. Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, Mattias Ulbrich (Eds.). Springer , 2016. ISBN 978-3-319-49812-6 
• Comparación de herramientas para enseñar verificación formal de software. Ingo Feinerer y Gernot Salzer. Springer , 2008
• Programación con pruebas: enfoques basados ​​en el lenguaje para crear software totalmente correcto. Aaron Stump. Software verificado: teorías, herramientas y experimentos, 2005.
• Alta seguridad (para seguridad o protección) y software libre/de código abierto (FLOSS). David Wheeler, 2009

• Página de inicio del proyecto KeY
• Página de inicio de KeYmaera
• Página de inicio de KeYmaeraX