0

所以我正在尝试使用检查器框架（来自https://checkerframework.org/），并且我有以下代码：

import org.checkerframework.checker.index.qual.Positive;

public class Ceker {


  public static void main(String[] args) {
    double a = Double.parseDouble(args[0]);
    System.out.println(new Ceker().preconditions(a));
  }

  public int preconditions(@Positive double a){
    return (int) a;
  }

}

我如何理解这是有效的，是我可以运行类似的东西

javacheck -processor positiveness Ceker.java

然后检查器会告诉我，我没有规则来测试是否double a总是积极的 - 所以我转到 main 方法并将其更改为：

public static void main(String[] args) {
    double a = Double.parseDouble(args[0]);
    if(a<0){
      throw new IllegalArgumentException("a is not positive!");
    }
    System.out.println(new Ceker().preconditions(a));
  }

现在，我的问题是 - 我可以不添加额外的检查代码，@Positive如果违反合同，让该注释在运行时自动抛出异常吗？

4

1 回答 1

0

简单来说：

  • 代码行为修改超出了 Checker Framework 的范围。
  • 您提出的更改通常是不可取的。
  • 运行时检查有时是不可能的。

这里有更多细节。

  1. Checker Framework 是一个在编译时工作的验证工具。它不会改变您的代码行为——它只是告诉您该行为是否可能是错误的。您可以使用按照您描述的方式更改代码行为的工具，但这样的工具与 Checker Framework 不同。

  2. 更改代码以引发异常是公共 API 方法的理想行为，例如main：它提供用户友好的错误消息。但是，对于代码中的大多数方法，这种更改并没有什么好处：它只是将一个导致程序崩溃的异常更改为另一个导致程序崩溃的异常。（提前抛出异常可能是一个调试好处，但这对用户来说并不是安慰。）检查器框架的目标是防止错误，而不是改变它们的表现方式。

  3. 对于许多类型的系统，没有可能的运行时测试。Checker Framework Manual 中的运行时测试和类型改进部分提供了十几个示例。

于 2021-07-06T16:12:27.757 回答