key
KeY-2.12.2 (2023-11-10)
Этот репозиторий является домом интерактивного ключа Phorem Prover для формальной проверки и анализа программ Java. Ключ поступает как автономное приложение с графическим интерфейсом, которое позволяет проверить функциональную правильность программ Java в отношении формальных спецификаций, сформулированных на языке моделирования Java JML. Кроме того, ключ также может использоваться в качестве библиотеки, например, для символической программы выполнения, рассуждения первого порядка или генерации тестовых случаев.
Для получения дополнительной информации обратитесь к
java.util.IdentityHashMap ,LinkedListТекущая версия ключа составляет 2.12.2, лицензирована в соответствии с GPL V2.
Не стесняйтесь использовать шаблоны проекта, чтобы начать использовать ключ:
Эта папка предоставляет проект, управляемый градл, после стандартной макета папки Maven. В этой папке есть несколько подпроектов. В целом, каждый key.*/ Подпроект содержит основной компонент ключа. Дополнительные и дополнительные компоненты находятся в keyext.*/ Папки. File build.gradle - это скрипт корневой сборки, описывающий зависимости и общие задачи сборки для всех подпроектов.
key.util , key.core и key.ui являются основой для продукта «Prover Key Prover». Особая помощь необходима, если вы планируете внести изменения здесь.
Предполагая, что вы находитесь в каталоге этого файла README, вы можете создать выполняемую и развернутую версию с одной из этих команд:
С ./gradlew key.ui:run вы можете запустить пользовательский интерфейс ключа непосредственно из репозитория. Используйте ./gradlew key.ui:run --args='--experimental' чтобы включить экспериментальные особенности.
Используйте ./gradlew classes для компиляции, который включает в себя запуск JAVACC и ANTLR. Аналогичным образом, используйте ./gradlew testClasses если вы также хотите собрать классы тестирования JUNIT.
Проверьте свою установку с помощью ./gradlew test . Имейте в виду, что это обычно занимает несколько часов. ./gradlew testFast
Вы можете выбрать конкретный тестовый пример с аргументом --tests . Подстановочные знаки разрешены.
./gradlew :key. < subproject > :test --tests " <class>.<method> " Вы можете отлаживать ключ, добавив опцию --debug-jvm , а затем подключив отладчика по адресу localhost:5005 .
Вы можете создать одну баночную версию, он же Fat Jar , ключ с
./gradlew :key.ui:shadowJar Файл генерируется в key.ui/build/libs/key-*-exe.jar .
Распределение строится с
./gradlew :key.ui:installDist :key.ui:distZip Распределение может быть проверено, вызывая key.ui/install/key/bin/key.ui и застегнута в key.ui/build/distributions .
Распространение дает вам возможность использования отдельных файлов JAR.
Качество автоматически оценивается с использованием Sonarqube по каждому запросу. Результаты оценок (Pass/Fail) могут быть проверены в разделе чеков PR.
Правила и качественные ворота поддерживаются в настоящее время Александром Вейглом Вейглом@kit.edu.
Больше руководств и документации для ключевой разработки можно найти под ключевыми данными.
Для отчетов об ошибках, пожалуйста, используйте The Tracker или отправьте почту по адресу [email protected].
Для обсуждения вы можете подписаться и использовать список рассылки [email protected] или использовать дискуссии GitHub.
Не стесняйтесь отправлять запросы на привлечение через GitHub. Запросы на вытягивание оцениваются с использованием автоматических тестов, форматирования и статических шашек источников, а также ручного обзора одного из разработчиков. Больше руководящих принципов и документации для ключевой разработки можно найти под ключевыми данными.
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.
