liquid-java/liquidjava

# LiquidJava - 使用 Liquid Types 扩展 Java [](https://marketplace.visualstudio.com/items?itemName=AlcidesFonseca.liquid-java) [](https://central.sonatype.com/artifact/io.github.liquid-java/liquidjava-api)  ## 欢迎使用 LiquidJava！ LiquidJava 是一个针对 Java 的附加类型检查器，基于 **liquid types** 和 **typestates**，通过编译时的 **refinements** 为 Java 程序提供额外的安全保障。 **示例：** ``` @Refinement("a > 0") int a = 3; // okay a = -8; // type error! ``` 本项目包含 LiquidJava 验证器及其 API，以及一些用于测试的示例。 您可以通过以下资源了解更多关于 LiquidJava 的信息： * [LiquidJava 网站](https://liquid-java.github.io) * [VS Code 扩展 (Marketplace)](https://marketplace.visualstudio.com/items?itemName=AlcidesFonseca.liquid-java) * [VS Code 扩展 (源代码)](https://github.com/liquid-java/vscode-liquidjava) * [LiquidJava 示例](https://github.com/liquid-java/liquidjava-examples) * [LiquidJava 外部库示例](https://github.com/liquid-java/liquid-java-external-libs) ## 快速入门 ### VS Code 扩展 使用 LiquidJava 最简单的方法是通过其 [VS Code 扩展](https://marketplace.visualstudio.com/items?itemName=AlcidesFonseca.liquid-java)，该扩展直接在 VS Code 内部使用 LiquidJava 验证器，提供实时的错误诊断和 refinements 的语法高亮。 ### 命令行 在开发时，您可以从命令行使用 LiquidJava 验证器。 #### 前置条件 在设置 LiquidJava 之前，请确保您已安装以下软件： - Java 20+ - 用于编译和运行 Java 程序的 JDK - Maven 3.6+ - 用于构建和依赖管理 此外，您还需要以下依赖项，其中包含了 LiquidJava API 注解： #### Maven ``` io.github.liquid-java liquidjava-api 0.0.5 ``` #### Gradle ``` repositories { mavenCentral() } dependencies { implementation 'io.github.liquid-java:liquidjava-api:0.0.5' } ``` #### 安装说明 1. 克隆仓库：`git clone https://github.com/liquid-java/liquidjava.git` 2. 构建项目：`mvn clean install` 3. 运行测试以验证安装：`mvn test` 4. 如果导入到 IDE 中，请使用根目录的 `pom.xml` 将项目作为 Maven 项目导入 #### 运行验证 要运行 LiquidJava，请使用下面的 Maven 命令，将 `/path/to/your/project` 替换为您要验证的 Java 文件或目录的路径。 ``` mvn exec:java -pl liquidjava-verifier -Dexec.mainClass="liquidjava.api.CommandLineLauncher" -Dexec.args="/path/to/your/project" ``` 如果您使用的是 Linux/macOS，可以使用 `liquidjava` 脚本（位于仓库根目录）来简化此过程。 **测试正确用例**： ``` ./liquidjava liquidjava-example/src/main/java/testSuite/CorrectSimpleAssignment.java ``` 这应该会输出：`Correct! Passed Verification`。 **测试错误用例**： ``` ./liquidjava liquidjava-example/src/main/java/testSuite/ErrorSimpleAssignment.java ``` 这应该会输出一条描述 refinement 违规的错误信息。 #### 测试 运行 `mvn test` 以执行 LiquidJava 中的所有测试。 初始测试文件是 `TestExamples.java`，它会运行 `liquidjava-example` 下 `testSuite` 目录中的测试套件。 测试套件涵盖以下测试用例： 1. 以 `Correct` 或 `Error` 开头的文件（例如，`CorrectRecursion.java`） 2. 包含单词 `correct` 或 `error` 的目录（例如，`arraylist_correct`） 因此，不遵循此模式的文件和文件夹将被忽略。 对于失败的测试用例，必须按以下方式指定期望的错误： 1. 在单个测试文件中，期望的错误（标题）应作为注释写在文件的第一行 2. 在测试目录中，该目录中应包含一个带有期望错误（标题）的 `.expected` 文件 ## 项目结构 * **docs**：包含用于语言设计的文档。此文件夹包含一个 [README](./docs/design/README.md)，其中包含指向设计过程中使用的完整工件的链接。它还包含在评估期间用于准备 refinements 语言设计的初始文档 * **liquidjava-api**：包含可以在 Java 程序中引入以添加 refinements 的注解 * **liquidjava-example**：包含一些示例和用于测试验证器的测试套件 * **liquidjava-verifier**：包含验证器的实现。其主要包有： * `api`：包含 `CommandLineLauncher`，用于对给定类运行验证，或者在未提供参数时对 `currentlyTesting` 目录运行验证 * `ast`：表示 Refinements Language (RJ) 的抽象语法树 (AST) * `errors`：用于报告错误的包 * `processor`：处理类型检查的包 * `rj_language`：处理将 refinement 字符串解析为 AST 的包 * `smt`：处理向 SMT solver 转换以及处理 SMT solver 生成的结果的包 * `utils`：包含上述所有包的有用方法 * `test/java/liquidjava/api/tests`：包含用于运行测试套件的 `TestExamples` 类

标签：Liquid Types, Maven, SMT求解器, Typestates, 云安全监控, 代码安全, 可配置连接, 域名枚举, 形式化验证, 漏洞枚举, 漏洞预防, 漏洞验证, 程序分析, 类型检查器, 类型状态, 精化类型, 编译器插件, 编译期检查, 静态分析