无法证明仅依赖于实现/内联的基本功能答案

【问题标题】：Cannot prove basic functions relying only on Implementations/Inlining无法证明仅依赖于实现/内联的基本功能
【发布时间】：2021-03-08 17:21:45
【问题描述】：

我有这门课程。当我使用 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;
    }
}

【问题讨论】：

标签： formal-verification jml key-formal-verification

【解决方案1】：

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

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

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

解决方案：

创建课程final。（然后没有覆盖）
创建方法getBarfinal（同样，没有覆盖）
创建方法getBar private（同样，没有覆盖）
在 GUI 中使用Options > Taclet Options 选项将选项methodExpansion 设置为noRestriction。（从“开放程序”更改为“封闭程序”，并允许到处扩展方法。）

【讨论】：