key
KeY-2.12.2 (2023-11-10)
Dieses Repository ist die Heimat des interaktiven Theorem -Prover -Schlüssels für die formale Überprüfung und Analyse von Java -Programmen. Der Schlüssel kommt als eigenständige GUI -Anwendung, mit der Sie die funktionale Korrektheit von Java -Programmen in Bezug auf formale Spezifikationen überprüfen können, die in der Java -Modellierungssprache JML formuliert sind. Darüber hinaus kann der Schlüssel auch als Bibliotheksbibliothek für symbolische Programmausführung, Argumentation erster Ordnung oder Testfallgenerierung verwendet werden.
Weitere Informationen finden Sie unter
java.util.IdentityHashMap ,LinkedListDie aktuelle Version des Schlüssels ist 2.12.2, lizenziert unter GPL V2.
Fühlen Sie sich frei, die Projektvorlagen zu verwenden, um mit dem Schlüssel zu beginnen:
Dieser Ordner bietet ein abschließendes Projekt nach dem Standard-Ordnerlayout von Maven. In diesem Ordner gibt es mehrere Unterprojekte. Im Allgemeinen enthält jeder key.*/ Subproject eine Kernkomponente des Schlüssels. Zusätzliche und optionale Komponenten befinden sich in keyext.*/ Ordner. Das Datei build.gradle ist das Root -Build -Skript, das die Abhängigkeiten und gemeinsamen Build -Aufgaben für alle Unterprojekte beschreibt.
key.util , key.core und key.ui sind die Basis für das Produkt "Schlüsselprover". Besonderes Sorgfalt ist erforderlich, wenn Sie vorhaben, Änderungen hier vorzunehmen.
Angenommen, Sie befinden sich im Verzeichnis dieser Readme -Datei, können Sie eine runnable und bereitbare Version mit einem dieser Befehle erstellen:
Mit ./gradlew key.ui:run Sie können die Benutzeroberfläche des Schlüssels direkt aus dem Repository ausführen. Verwendung ./gradlew key.ui:run --args='--experimental'
Verwenden Sie ./gradlew classes Ebenso verwenden ./gradlew testClasses .
Testen Sie Ihre Installation mit ./gradlew test . Beachten Sie, dass dies normalerweise mehrere Stunden dauert. Mit ./gradlew testFast
Sie können einen bestimmten Testfall mit dem Argument --tests auswählen. Wildcards sind erlaubt.
./gradlew :key. < subproject > :test --tests " <class>.<method> " Sie können den Schlüssel debuggen, indem Sie die Option --debug-jvm hinzufügen und dann einen Debugger bei localhost:5005 .
Sie können eine einzelne Jar-Version, auch bekannt als Fat Jar , von Schlüssel mit erstellen
./gradlew :key.ui:shadowJar Die Datei wird in key.ui/build/libs/key-*-exe.jar generiert.
Eine Verteilung wird mit gebaut
./gradlew :key.ui:installDist :key.ui:distZip Die Verteilung kann getestet werden, indem Sie key.ui/install/key/bin/key.ui aufrufen und in key.ui/build/distributions geschleudert werden.
Die Verteilung bietet Ihnen das Potenzial, einzelne JAR -Dateien zu verwenden.
Die Qualität wird auf jeder Zuganfrage automatisch mit Sonarqube bewertet. Die Ergebnisse der Bewertungen (Pass/Fail) können im Abschnitt Überprüfungen des PR inspiziert werden.
Die Regeln und das Qualitätstor werden derzeit von Alexander Weigl [email protected] gepflegt.
Weitere Richtlinien und Dokumentation für die Schlüsselentwicklung finden Sie unter Schlüsseldocs.
Für Fehlerberichte verwenden Sie bitte den Ausgabe-Tracker oder senden Sie eine E-Mail an [email protected].
Für Diskussionen möchten Sie möglicherweise die Mailingliste [email protected] verwenden oder GitHub-Diskussionen verwenden.
Fühlen Sie sich frei, Pull -Anfragen per GitHub einzureichen. Pull -Anfragen werden anhand automatischer Tests, Formatierung und statischer Quellprüfer sowie einer manuellen Überprüfung durch einen der Entwickler bewertet. Weitere Richtlinien und Dokumentation für die Schlüsselentwicklung finden Sie unter Schlüsseldocs.
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.
