1

我有这门课。当我使用 getBar() 的合同时，我可以证明 pass(int i) 方法，而不是没有它。除了 getBar() 的合约也被证明。为什么我不能通过内联证明通过？我尝试了 Key 2.8 和 Key 2.7。

public class Course {

    /*@ spec_public @*/ private int bar;
    /*@ spec_public @*/ private int time =100;
    public  boolean strict= true;

    /*@ public  normal_behaviour
      @ requires this!=null;
      @ ensures  \result==bar;
      @ assignable \nothing;
      @*/
    public int getBar() {
        return this.bar;
    }
    /*@ public normal_behaviour
      @ ensures  \result==(getBar()<=i);
      @*/
    public boolean passed(int i) {
        return this.getBar()<= i;
    }
}
4

1 回答 1

1

Key验证引擎可用于验证JML注解的Java 程序。（大部分是自动的，但可以进行交互式定理证明）。

它以模块化方式工作。这意味着每个方法都被单独考虑。您的方法passed调用getBar，但getBar实际上可能在 Course 的子类中被覆盖 - 稍后可能会添加。Key 使用“开放程序”范式验证程序，这意味着程序的任何扩展（添加类）都不能使现有证明无效。

因此：此调用无法进行内联，因为该方法可能被覆盖。

解决方案：

  1. 上课final。（然后没有覆盖）
  2. 制作方法getBar final（同样，没有覆盖）
  3. 制作方法getBar private（同样，没有覆盖）
  4. 在 GUI 中，使用Options > Taclet Options选项将选项设置methodExpansion为noRestriction. （从“开放程序”更改为“封闭程序”，并允许到处进行方法扩展。）
于 2021-03-10T15:01:13.743 回答