KeYProject/key
GitHub: KeYProject/key
KeY 是一个用于 Java 程序演绎形式验证的定理证明器，解决代码功能正确性验证问题。
Stars: 77 | Forks: 44
# KeY -- 用于 Java 程序形式验证的演绎验证器
[](https://github.com/KeYProject/key/actions/workflows/tests.yml) [](https://github.com/KeYProject/key/actions/workflows/codeql.yml) [](https://github.com/KeYProject/key/actions/workflows/code_quality.yml)
该仓库是交互式定理证明器 KeY 的所在地，用于对 Java 程序进行形式化验证和分析。KeY 作为一个独立的 GUI 应用程序提供，允许你使用 Java 建模语言（JML）表述的形式规范来验证 Java 程序的功能正确性。此外，KeY 还可以作为库使用，例如用于符号程序执行、一阶推理或测试用例生成。
更多信息请参考
* [KeY 主页](https://key-project.org)
* [KeY 书籍](https://www.key-project.org/thebook2/)
* [KeY 开发者文档](https://keyproject.github.io/key-docs/)
* KeY 的成功案例：
* [在 JDK 排序例程（TimSort）中发现的严重漏洞](http://www.envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/),
* [验证 `java.util.IdentityHashMap`](https://doi.org/10.1007/978-3-031-07727-2_4),
* [Google 奖表彰对 `LinkedList` 漏洞的分析](https://www.key-project.org/2023/07/23/cwi-researchers-win-google-award-for-finding-a-bug-in-javas-linkedlist-using-key/)
当前 KeY 版本为 2.12.2，采用 GPL v2 许可。
欢迎使用项目模板开始使用 KeY：
* [用于验证项目](https://github.com/KeYProject/verification-project-template)
* [作为库使用](https://github.com/KeYProject/key-java-example)
* [作为符号执行后端使用](https://github.com/KeYProject/symbex-java-example)
## 要求
* 硬件：>=2 GB 内存
* 操作系统：Linux/Unix、MacOSX、Windows
* Java 17 或更新版本
* 可选地，KeY 可以使用以下二进制文件：
* SMT 求解器：
* [Z3](https://github.com/Z3Prover/z3#z3)
* [cvc5](https://cvc5.github.io/)
* [CVC4](https://cvc4.github.io/)
* [Princess](http://www.philipp.ruemmer.org/princess.shtml)
## KeY 文件夹内容
此文件夹提供了一个遵循
[Maven 的标准文件夹布局](https://maven.apache.org/guides/introduction/introduction-to-the-standard-directory-layout.html)
的 [gradle](https://gradle.org) 管理项目。
此文件夹包含多个子模块。一般而言，每个 `key.*/` 子模块都包含 KeY 的核心组件。
额外和可选的组件位于 `keyext.*/` 文件夹中。文件 `build.gradle` 是根构建脚本，
描述了所有子项目的依赖关系和通用构建任务。
`key.util`、`key.core` 和 `key.ui` 是产品 “KeY Prover” 的基础。如果计划在此处进行更改，需要特别小心。
## 编译并运行 KeY
假设你当前位于此 README 文件所在目录，可以通过以下命令之一创建可运行且可部署的版本：
1. 使用 `./gradlew key.ui:run` 可以直接从仓库运行 KeY 的用户界面。
使用 `./gradlew key.ui:run --args='--experimental'` 来启用实验性功能。
2. 使用 `./gradlew classes` 来编译 KeY，这将包括运行 JavaCC 和 Antlr。
同样，如果还需要编译 JUnit 测试类，请使用 `./gradlew testClasses`。
3. 使用 `./gradlew test` 测试安装。请注意，这通常需要数小时才能完成。
使用 `./gradlew testFast` 可以运行更轻量级的测试套件，通常在几分钟内完成。
你可以使用 `--tests` 参数选择特定的测试用例。允许使用通配符。
./gradlew :key.<子项目>:test --tests "<类>.<方法>"
你可以通过添加 `--debug-jvm` 参数来调试 KeY，然后在 `localhost:5005` 处附加调试器。
4. 你可以通过以下命令创建 KeY 的单一 jar 版本（亦称 *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` 中。
该分发方式提供了使用单一 jar 文件的可能性。
# 开发 KeY
* 质量通过每次拉取请求自动使用 [SonarQube](https://sonarqube.org) 评估。
评估结果（通过/失败）可在 PR 的检查部分查看。
规则和质量门禁由 Alexander Weigl
维护。
* 更多 KeY 开发指南和文档可以在
[key-docs](https://keyproject.github.io/key-docs/devel/)
下找到。
# 问题与错误报告
* 对于错误报告，请使用 [问题追踪器](https://github.com/KeYProject/key/issues) 或发送邮件至 support@key-project.org。
* 对于讨论，你可以订阅并使用邮件列表 或使用 [GitHub 讨论](https://github.com/KeYProject/key/discussions)。
# 贡献 KeY
欢迎通过 GitHub 提交 [拉取请求](https://github.com/KeYProject/key/pulls)。拉取请求将通过自动测试、代码格式化和静态源码检查，以及由一名开发人员进行人工审查来评估。关于 KeY 开发，更多指南和文档可以在 [key-docs](https://keyproject.github.io/key-docs/devel/) 下找到。
# 许可证说明
```
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.
```
标签：GPL, GUI 验证工具, Java Modeling Language, Java 程序验证, JML, JS文件枚举, KeY, 一阶逻辑推理, 云安全监控, 交互式定理证明器, 代码验证, 功能正确性, 可配置连接, 后台面板检测, 域名枚举, 安全关键系统, 定理证明, 开源定理证明, 形式化验证, 测试用例生成, 程序分析, 程序正确性, 符号执行, 软件验证, 静态分析