Dafny：断言未访问的元素保持不变

Question

让我们假设我们有一个元素数组 [e_1, e_2, ..., e_n] 并且一个方法只访问（读取和写入）数组的前 m 个元素，例如该方法将数组的前 m 个元素递增 1。如何在 Dafny 中实现该方法，以便该方法提供形式的后置条件

ensures forall i: int :: m < i <= a.Length ==> old(a[i]) == a[i]

我目前的方法没有用，所以我不在这里展示它们。

Answer 1

这里是实现：

method IncreaseByOne(a: array<int>, idx: int)
  requires 0 <= idx <= a.Length
  modifies a
  ensures forall i ::  0 <= i < idx ==> a[i] == old(a[i]) + 1
  ensures forall i ::  idx <= i < a.Length ==> a[i] == old(a[i])
{
  var t := 0;
  while t < idx
    invariant 0 <= t <= idx
    invariant forall i :: 0 <= i < t ==> a[i] == old(a[i]) + 1
    invariant forall i :: t <= i < a.Length ==> a[i] == old(a[i])
  {
    a[t] := a[t] + 1;
    t := t + 1;
  }
}