【发布时间】:2015-03-04 05:18:48
【问题描述】:
我最近在一次旧考试中阅读了以下 JML 代码:
Class L {
/*@non_null*/ int[] a;
/*@ public normal_behaviour
@ requires !(\exists int i; 0 <= i && i < a.length; a[i] == d);
@ ensures a.length == \old(a.length) + 1;
@ ensures a[\old(a.length)] == d;
@ ensures (\forall int i; 0 <= i && i < \old(a.length);
a[i] == \old(a[i]));
@ assignable a, a[*];
@*/
public void st(int d) {
...
}
}
我不明白
assignable a, a[*];
部分。 a[*]
是什么意思?如果只有一个会有什么不同
assignable a;
?
(一个参考链接会很棒。)
【问题讨论】:
-
我猜这意味着你可以改变数组的内容,但这只是一个猜测:)
-
@leppie 这也是我的猜测。但是我不太确定,这就是我问的原因(这也是我希望参考的原因)。
-
您可以尝试违反假设(iow,将
a[*]
删除为assignable
)并确认它失败了。 -
a[*]
表示数组a
中的所有索引。
标签: jml