key

钥匙 - 演绎Java程序验证者

该存储库是对Java程序进行正式验证和分析的交互式定理供应密钥的所在地。 Key是独立的GUI应用程序，它使您可以验证Java程序在Java建模语言JML中提出的正式规格的功能正确性。此外，密钥还可以用作库，例如符号程序执行，一阶推理或测试案例生成。

有关更多信息，请参阅

• 关键主页
• 关键书
• 关键开发人员文档
• 钥匙的成功案例：
  • 在JDK分类常规（Timsort）中发现的严重错误，
  • java.util.IdentityHashMap的验证，
  • Google分析LinkedList中的错误奖

当前版本的KEY为2.12.2，根据GPL V2许可。

随意使用项目模板开始使用密钥开始：

• 用于验证项目
• 用作图书馆
• 用作符号执行后端

要求

• 硬件：> = 2 GB RAM
• 操作系统：Linux/Unix，MacOSX，Windows
• Java 17或更新
• 可选地，钥匙可以利用以下二进制文件：
  • SMT求解器：
    • Z3
    • CVC5
    • CVC4
    • 公主

关键文件夹的内容

该文件夹在Maven的标准文件夹布局之后提供了一个由Gradle管理的项目。该文件夹中有几个子项目。通常，每个key.*/ subproject包含键的核心组件。其他和可选的组件在keyext.*/文件夹。文件build.gradle是root构建脚本，描述了所有子项目的依赖关系和常见的构建任务。

key.util ， key.core和key.ui是产品“密钥供体”的基础。如果您打算在此处进行更改，则需要特殊护理。

编译和运行键

假设您位于此REDME文件的目录中，则可以使用其中一个命令创建可运行且可部署的版本：

1. 使用./gradlew key.ui:run您可以直接从存储库运行键的用户界面。使用./gradlew key.ui:run --args='--experimental'以实现实验特征。

2. 使用./gradlew classes来编译密钥，其中包括运行JavACC和ANTLR。同样，如果您还想编译JUNIT测试类，请使用./gradlew testClasses 。

3. 使用./gradlew test测试安装。请注意，这通常需要几个小时才能完成。使用./gradlew testFast ，您可以在几分钟内运行更轻巧的测试套件。

   您可以选择具有--tests参数的特定测试用例。允许通配符。

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

   您可以通过添加--debug-jvm选项来调试键，然后在localhost:5005 。

4. 您可以使用单个罐子转换，又称fat jar的钥匙

   ./gradlew :key.ui:shadowJar

   该文件是在key.ui/build/libs/key-*-exe.jar中生成的。

5. 分布构建

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

   可以通过调用key.ui/install/key/bin/key.ui进行测试，并在key.ui/build/distributions中进行zy。

   该分布使您有可能使用单个JAR文件。

开发密钥

• 在每个拉的请求下使用Sonarqube自动评估质量。可以在PR的“检查”部分中检查评估结果（通过/失败）。

  目前，Alexander Weigl [email protected]维护了规则和质量大门。

• 有关关键开发的更多指南和文档，可以在密钥内部找到。

问题和错误报告

• 有关错误报告，请使用问题跟踪器或发送邮件到[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.