liquid-java/vscode-liquidjava

# LiquidJava VS Code 扩展  ### 使用 Liquid Types 扩展你的 Java 代码，并更早地捕获错误！ [LiquidJava](https://github.com/liquid-java/liquidjava) 是一个针对 Java 的附加类型检查器，它基于 **liquid types** 和 **typestates**，在编译时为 Java 程序提供了更强的安全保证。通过此扩展，你可以直接在 VS Code 中使用 LiquidJava，并获得实时诊断报告、refinement 的语法高亮，以及用于显示诊断详情和状态机图表的交互式 webview。 ``` @Refinement("a > 0") int a = 3; // okay a = -8; // type error! ``` ### 安装 要试用该扩展，请从 [VS Code Marketplace](https://marketplace.visualstudio.com/items?itemName=AlcidesFonseca.liquid-java) 或 [Open VSX Marketplace](https://open-vsx.org/extension/AlcidesFonseca/liquid-java) 进行安装。此外，你还需要 [Language Support for Java(TM) by Red Hat](https://marketplace.visualstudio.com/items?itemName=redhat.java) VS Code 扩展，并将 `liquidjava-api` 依赖项添加到你的 Java 项目中： #### Maven ``` io.github.liquid-java liquidjava-api 0.0.5 ``` #### Gradle ``` repositories { mavenCentral() } dependencies { implementation 'io.github.liquid-java:liquidjava-api:0.0.5' } ``` 包含 LiquidJava 示例的代码库可在 [liquidjava-examples](https://github.com/liquid-java/liquidjava-examples) 找到。你可以使用 [GitHub Codespaces](https://codespaces.new/liquid-java/liquidjava-examples) 试用它们，而无需配置本地环境。 ### 什么是 Liquid Types？ Liquid types 通过在基本类型上添加**逻辑谓词**来扩展语言。它们允许开发者限制变量、参数或返回值可以具有的值。这类约束有助于在程序执行前捕获更多错误。例如，它们允许我们在编译时防止诸如数组索引越界或除以零之类的错误。 ### LiquidJava #### Refinements 要 refinement 变量、字段、参数或返回值，请使用 `@Refinement` 注解，并将谓词作为参数传入。该谓词必须是一个布尔表达式，并使用被 refinement 的变量的名称（或 `_`）来引用其值。你还可以提供一条自定义消息，当违反该 refinement 时，该消息将包含在错误消息中。一些示例包括： ``` @Refinement("x > 0") // x must be greater than 0 int x; @Refinement("0 <= _ && _ <= 100") // y must be between 0 and 100 int y; @Refinement(value="z % 2 == 0 ? z >= 0 : z < 0", msg="z must be positive if even, negative if odd") int z; @Refinement("_ >= 0") int absDiv(int a, @Refinement(value="b != 0", msg="cannot divide by zero") int b) { int res = a / b; return res >= 0 ? res : -res; } ``` #### Refinement 别名 为了简化 refinements 的使用，你可以使用 `@RefinementAlias` 注解创建**谓词别名**，并在其他 refinements 中应用它们： ``` @RefinementAlias("Percentage(int v) { 0 <= v && v <= 100 }") public class MyClass { // x must be between 0 and 100 @Refinement("Percentage(x)") int x = 25; } ``` #### 通过 Typestates 进行对象状态建模 除了基本的 refinements 之外，LiquidJava 还支持通过 typestates 进行**对象状态建模**，这允许开发者根据对象的状态指定何时可以或不能调用某个方法。你还可以为违反方法前置条件的情况提供自定义错误消息。例如： ``` @StateSet({"open", "closed"}) public class MyFile { @StateRefinement(to="open(this)") public MyFile() {} @StateRefinement(from="open(this)", msg="file must be open to read") public void read() {} @StateRefinement(from="open(this)", to="closed(this)", msg="file must be open to close") public void close() {} } MyFile f = new MyFile(); f.read(); f.close(); f.read(); // type error: file must be open to read ``` #### Ghost 变量和外部 Refinements 最后，LiquidJava 还提供了 **ghost 变量**，当 typestates 不足以满足需求时，可以使用 `@Ghost` 注解来跟踪有关程序状态的额外信息。此外，你还可以使用 `@ExternalRefinementsFor` 注解来 refinement 外部库。以下是一个使用 LiquidJava 对 `java.util.Stack` 类进行 refinement 的示例，其中使用 `size` ghost 变量来跟踪堆栈中的元素数量： ``` @ExternalRefinementsFor("java.util.Stack") @Ghost("int size") public interface StackRefinements { public void Stack(); @StateRefinement(to="size(this) == size(old(this)) + 1") // increments size by 1 public boolean push(E elem); @StateRefinement(from="size(this) > 0", to="size(this) == size(old(this)) - 1", msg="cannot pop from an empty stack") // decrements size by 1 public E pop(); @StateRefinement(from="size(this) > 0", msg="cannot peek from an empty stack") public E peek(); } Stack s = new Stack<>(); s.push("hello"); s.pop(); s.pop(); // type error: cannot pop from an empty stack ``` 你可以在 [LiquidJava 官网](https://liquid-java.github.io) 上找到更多关于如何使用 LiquidJava 的示例。要学习如何使用 LiquidJava，你还可以跟随 [LiquidJava 教程](https://github.com/liquid-java/liquidjava-tutorial)进行学习。 欲了解更多信息，请查看以下代码库： - [liquidjava](https://github.com/liquid-java/liquidjava)：包含 API、验证器和一些示例 - [vscode-liquidjava](https://github.com/liquid-java/vscode-liquidjava)：此 VS Code 扩展的源代码 - [liquidjava-examples](https://github.com/liquid-java/liquidjava-examples)：关于如何使用 LiquidJava 的示例 - [liquid-java-external-libs](https://github.com/liquid-java/liquid-java-external-libs)：关于如何使用 LiquidJava 对外部库进行 refinement 的示例

标签：JS文件枚举, LSP, 后台面板检测, 类型检查, 自动化攻击, 错误基检测, 静态代码分析