【问题标题】:What does 'assignable a, a[*];' mean?'assignable a, a[*];' 是什么意思?意思是?
【发布时间】: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


【解决方案1】:

JML 中的 assignable 子句仅允许方法在以下情况下修改位置 loc:

- loc is mentioned in the method’s assignable clause;
- loc is not allocated when the method starts execution; or
- loc is local to the method (i.e., a local variable or a formal parameter)

a[*]的使用是[0 ... a.length-1];¹的简写

More Information | Cited Reference

【讨论】:

  • 澄清一下:“assignable a, a[*]”意味着你们俩都可以做“a = new int[0];”和“a[17] = 42”,而通过省略一个子条款,相应的语句将是非法的。顺便说一句,我会投票选择正确的答案。