key

Clave - Verificador de programa Java deductivo

Este repositorio es el hogar de la clave del teorema interactivo para la verificación y el análisis formales de los programas Java. La clave viene como una aplicación GUI independiente, que le permite verificar la corrección funcional de los programas Java con respecto a las especificaciones formales formuladas en el lenguaje de modelado Java JML. Además, la clave también se puede utilizar como una biblioteca, por ejemplo, para la ejecución del programa simbólico, el razonamiento de primer orden o la generación de casos de prueba.

Para obtener más información, consulte

• La página de inicio clave
• El libro de claves
• La documentación clave del desarrollador
• Historias de éxito de Key:
  • Error severo descubierto en la rutina de clasificación JDK (Timsort),
  • Verificación de java.util.IdentityHashMap ,
  • Premio de Google por analizar un error en LinkedList

La versión actual de la clave es 2.12.2, licenciada bajo GPL V2.

No dude en usar las plantillas del proyecto para comenzar a usar la clave:

• Para proyectos de verificación
• Usando como biblioteca
• Usar como un backend de ejecución simbólica

Requisitos

• Hardware:> = 2 GB de RAM
• Sistema operativo: Linux/Unix, MacOSX, Windows
• Java 17 o más nuevo
• Opcionalmente, la clave puede hacer uso de los siguientes binarios:
  • Solvers SMT:
    • Z3
    • CVC5
    • CVC4
    • Princesa

Contenido de la carpeta de teclas

Esta carpeta proporciona un proyecto administrado por graduados después del diseño de carpeta estándar de Maven. Hay varios subprojects en esta carpeta. En general, cada key.*/ Subproject contiene un componente central de la clave. Los componentes adicionales y opcionales están en keyext.*/ Carpetas. El archivo build.gradle es el script de construcción raíz que describe las dependencias y las tareas de compilación comunes para todos los subproyectos.

key.util , key.core y key.ui son la base del producto "Key Prover". Se necesita especial cuidado si planea hacer cambios aquí.

Compilar y ejecutar la llave

Suponiendo que se encuentre en el directorio de este archivo ReadMe, puede crear una versión ejecutable e implementable con uno de estos comandos:

1. Con ./gradlew key.ui:run Puede ejecutar la interfaz de usuario de la tecla directamente desde el repositorio. Use ./gradlew key.ui:run --args='--experimental' para habilitar las características experimentales.

2. Use ./gradlew classes para compilar la clave, que incluye ejecutar Javacc y ANTLR. Del mismo modo, use ./gradlew testClasses si también desea compilar las clases de prueba JUnit.

3. Pruebe su instalación con ./gradlew test . Tenga en cuenta que esto generalmente tardará varias horas en completarse. Con ./gradlew testFast , puede ejecutar un conjunto de pruebas más liviano que debería completarse en unos minutos.

   Puede seleccionar un caso de prueba específico con el argumento --tests . Se permiten comodines.

   ./gradlew :key. < subproject > :test --tests " <class>.<method> "

   Puede depurar la tecla agregando la opción --debug-jvm , luego adjuntando un depurador en localhost:5005 .

4. Puede crear un solo jar-version, también conocido como jarra de grasa , de clave con

   ./gradlew :key.ui:shadowJar

   El archivo se genera en key.ui/build/libs/key-*-exe.jar .

5. Se construye una distribución con

   ./gradlew :key.ui:installDist :key.ui:distZip

   La distribución se puede probar llamando key.ui/install/key/bin/key.ui y se adhiere a key.ui/build/distributions .

   La distribución le brinda el potencial de usar archivos JAR únicos.

Desarrollo de la llave

• La calidad se evalúa automáticamente utilizando Sonarqube en cada solicitud de extracción. Los resultados de las evaluaciones (aprobación/fallas) pueden inspeccionarse en la sección de comprobaciones de la PR.

  Alexander Weigl [email protected] mantiene las reglas y la calidad de calidad.

• Se puede encontrar más directriz y documentación para el desarrollo clave en Docs de clave.

Problemas e informes de errores

• Para informes de errores, utilice el rastreador de problemas o envíe un correo a [email protected].

• Para las discusiones, es posible que desee suscribirse y utilizar la lista de correo [email protected] o utilizar las discusiones de GitHub.

Contribuyendo a la clave

Siéntase libre de enviar solicitudes de extracción a través de GitHub. Las solicitudes de extracción se evalúan mediante pruebas automáticas, formateo y verificadores de fuente estáticas, así como una revisión manual de uno de los desarrolladores. Se pueden encontrar más pautas y documentación para el desarrollo clave en Key-Docs.

Comentario de la licencia

 This is the KeY project - Integrated Deductive Software Design
Copyright (C) 2001-2011 Universität Karlsruhe, Germany
						Universität Koblenz-Landau, Germany
						and Chalmers University of Technology, Sweden
Copyright (C) 2011-2024 Karlsruhe Institute of Technology, Germany
						Technical University Darmstadt, Germany
						Chalmers University of Technology, Sweden

The KeY system is protected by the GNU General Public License.
See LICENSE.TXT for details.