key

Key - Vérificateur du programme Java déductif

Ce référentiel est le domicile de la clé de proverage du théorème interactif pour la vérification formelle et l'analyse des programmes Java. La clé est une application GUI autonome, qui vous permet de vérifier l'exactitude fonctionnelle des programmes Java en ce qui concerne les spécifications formelles formulées dans le langage de modélisation Java JML. De plus, la clé peut également être utilisée comme bibliothèque, par exemple pour l'exécution du programme symbolique, le raisonnement de premier ordre ou la génération de cas de test.

Pour plus d'informations, reportez-vous à

• La page d'accueil clé
• Le livre clé
• La documentation clé du développeur
• Les histoires de réussite de Key:
  • Bug sévère découvert dans la routine de tri JDK (TimSort),
  • Vérification de java.util.IdentityHashMap ,
  • Google Award pour analyser un bogue dans LinkedList

La version actuelle de Key est 2.12.2, sous licence GPL V2.

N'hésitez pas à utiliser les modèles de projet pour commencer à utiliser la clé:

• Pour les projets de vérification
• En utilisant comme bibliothèque
• En utilisant comme backend d'exécution symbolique

Exigences

• Matériel:> = 2 Go de RAM
• Système d'exploitation: Linux / Unix, MacOSX, Windows
• Java 17 ou plus récent
• Facultativement, Key peut utiliser les binaires suivants:
  • SMT SOLVERS:
    • Z3
    • CVC5
    • CVC4
    • Princesse

Contenu du dossier clé

Ce dossier fournit un projet géré par Gradle après la disposition des dossiers standard de Maven. Il y a plusieurs sous-projets dans ce dossier. En général, chaque key.*/ Sous-projection contient un composant central de la clé. Les composants supplémentaires et facultatifs sont dans keyext.*/ Dossiers. Le fichier build.gradle est le script de construction racine décrivant les dépendances et les tâches de construction communes pour tous les sous-projets.

key.util , key.core et key.ui sont la base du produit "Key Prover". Des soins particuliers sont nécessaires si vous prévoyez d'apporter des modifications ici.

Compiler et exécuter la clé

En supposant que vous êtes dans le répertoire de ce fichier ReadMe, vous pouvez créer une version exécutable et déployable avec l'une de ces commandes:

1. Avec ./gradlew key.ui:run vous pouvez exécuter l'interface utilisateur de la clé directement à partir du référentiel. Utiliser ./gradlew key.ui:run --args='--experimental' pour permettre des fonctionnalités expérimentales.

2. Utilisez ./gradlew classes pour compiler Key, qui comprend l'exécution de Javacc et Antlr. De même, utilisez ./gradlew testClasses si vous souhaitez également compiler les classes de test JUnit.

3. Testez votre installation avec ./gradlew test . Sachez que cela prendra généralement plusieurs heures. Avec ./gradlew testFast , vous pouvez exécuter une suite de test plus légère qui devrait se terminer en quelques minutes.

   Vous pouvez sélectionner un cas de test spécifique avec l'argument --tests . Les caractères génériques sont autorisés.

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

   Vous pouvez déboguer la clé en ajoutant l'option --debug-jvm , puis en joignant un débogueur sur localhost:5005 .

4. Vous pouvez créer une seule version de Jar, alias Fat Jar , de Key avec

   ./gradlew :key.ui:shadowJar

   Le fichier est généré dans key.ui/build/libs/key-*-exe.jar .

5. Une distribution est construite avec

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

   La distribution peut être testée en appelant key.ui/install/key/bin/key.ui et est zippé dans key.ui/build/distributions .

   La distribution vous donne le potentiel d'utiliser des fichiers JAR unique.

Clé en développement

• La qualité est automatiquement évaluée à l'aide de Sonarqube sur chaque demande de traction. Les résultats des évaluations (adop / échec) peuvent être inspectés dans la section des chèques du PR.

  Les règles et la porte de qualité sont maintenues par Alexander Weigl [email protected] actuellement.

• Plus de directives et de documentation pour le développement clé peuvent être trouvées dans les clés.

Problèmes et rapports de bogues

• Pour les rapports de bogues, veuillez utiliser le tracker du problème ou envoyer un courrier à [email protected].

• Pour les discussions, vous souhaiterez peut-être vous abonner et utiliser la liste de diffusion [email protected] ou utiliser des discussions GitHub.

Contribuant à Key

N'hésitez pas à soumettre des demandes de traction via GitHub. Les demandes de traction sont évaluées à l'aide de tests automatiques, de formatage et de vérificateurs de source statique, ainsi qu'une revue manuelle par l'un des développeurs. Plus de directives et de documentation pour l'élaboration des clés peuvent être trouvées dans les clés.

Remarque de licence

 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.