在 Dafny 中指定修改数组的一部分

Question

我正在 Dafny 中编写分区方法作为快速排序实现的一部分，我想指定此方法仅修改部分后备数组。

这是我的方法的header：

method partitionSegment (a : array<int>, first : int, len : int) returns (p : int)
  modifies a
...

思路是first和len参数指定数组a的一段（元素a[first] ... a[first+len-1]）； partitionSegment 对该数组进行分区，返回枢轴的索引，该索引将介于 first 和 first+len-1 之间。

在我的修改子句中，我想指出只能修改 a[first] ... a[first+len-1]，而不是所有 a。但是，当我尝试使用集合理解时，例如：

method partitionSegment (a : array<int>, first : int, len : int) returns (p : int)
modifies (set x | first <= x < first+len :: a[x])

类型检查器犹豫不决，说这是一组整数而不是一组内存位置。（所以 a[x] 被解释为存储在 a[x] 的值，而不是内存位置 a[x]。）

有什么方法可以在 dafny 中做到这一点：在修改注释中指定数组的一部分？

Answer 1

执行此操作的最佳方法是将修改子句保留为 modifies a，然后添加一个使用 old 的后置条件，以保证只有 a 的预期部分发生变化。

像这样：

ensures forall i | 0 <= i < a.Length :: 
    !(first <= i < first + len) ==> a[i] == old(a[i])

换句话说，这表示所有超出预期范围的索引都等于它们在方法执行之前的值。

一般来说，您应该认为 Dafny 的修饰子句相对 coarse-grained。它们通常限制可以修改哪些对象，而不是这些对象的哪些部分。如果你想指定对象的某些字段不改变，那么你可以使用像 foo.f == old(foo.f).

这样的后置条件来做到这一点

Specifying modification of part of an array in Dafny