java - 如何分析上下文外的 Java 方法？

Question

我正在尝试执行以下操作：对于给定的 Java 方法，我想查看该方法是否可以在特定上下文中使用并且在那里是正确的，即是否存在存在的类、字段、方法等的某些定义使这个方法正确。例如，方法

int m() {
    A a = new A();
    return a.value() + 1;
}

例如，当类A被定义，这个类有一个公共方法被调用value并且该方法返回时是正确的int。另一方面，对于

int m() {
    A a1 = new A();
    int n = a1.value();
    A a2 = new A();
    String s = a2.value();
    return s.length() + n;
}

没有上下文可以证明该方法是正确的。我知道这个问题可能有点过于宽泛（而且是理论上的问题），但总的来说，我该如何解决这类问题？一方面，我知道应该进行某种类型检查和控制流分析。不过，我不确定这是否就是必须要做的全部。