无法证明仅依赖 Implementations/Inlining 的基本功能

Question

我有这个 class 课程。当我使用 getBar() 的合同时，我可以证明 passed(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;
    }
}

Answer 1

KeY verification engine can be used to verify JML 个注释了 Java 个程序。（大部分是自动的，但也可以进行交互式定理证明）。

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

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

解决方案:

制作 class final。（然后没有覆盖）
创建方法 getBar final（同样，不要覆盖）
创建方法 getBar private（同样，不要覆盖）
在 GUI 中使用 Options > Taclet Options 选项将选项 methodExpansion 设置为 noRestriction。（从“开放程序”变为“封闭程序”，让方法随处扩展。）

无法证明仅依赖 Implementations/Inlining 的基本功能

Cannot prove basic functions relying only on Implementations/Inlining

formal-verification

jml

key-formal-verification