'assignable a, a[*];'是什么意思？

Question

我最近在一次旧考试中读到了以下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;

（链接到参考文献会很好。）

Answer 1

JML中的可赋值子句只允许方法在以下情况下修改位置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];的缩写

更多信息|引用参考