如何解决无法证明仅依赖于实现/内联的基本功能
我有这门课。当我使用 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;
}
}
解决方法
KeY 验证引擎可用于验证 JML 带注释的 Java 程序。 (大部分是自动的,但可以进行交互式定理证明)。
它以模块化方式工作。这意味着每种方法都是单独考虑的。您的方法 passed
调用 getBar
,但 getBar
实际上可能会在 Course 的子类中被覆盖——稍后可能会添加一个子类。 Key 使用“开放程序”范式验证程序,这意味着程序的任何扩展(添加类)都不能使现有证明无效。
因此:此调用无法进行内联,因为该方法可能会被覆盖。
解决方案:
- 使类
final
。 (然后没有覆盖) - 使方法
getBar
final
(同样,没有覆盖) - 使方法
getBar
private
(同样,没有覆盖) - 在 GUI 中,使用
Options > Taclet Options
选项将选项methodExpansion
设置为noRestriction
。 (从“打开程序”改为“关闭程序”,并允许随处扩展。)
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。