while循环中的动态“修改”子句答案

【问题标题】：Dynamic `modifies` clause in while loopwhile循环中的动态“修改”子句
【发布时间】：2020-12-08 10:31:43
【问题描述】：

当第一次进入循环时，while 循环中的modifies 子句只计算一次。例如，如果我有一个对象序列并且我对其进行了扩展，但还修改了我在之前的迭代中创建的新元素，Dafny 不会接受它：

class Foo {
  var x: int;

  constructor()
  {
    x := 0;
  }
}

method main(n: nat)
  requires n > 0
{
  var first := new Foo();
  var arr: seq<Foo> := [first];
  var i := 1;
  while i < n
    modifies set x | x in arr
    invariant 0 <= i <= n
    invariant |arr| == i
  {
    arr[i-1].x := i;
    var next := new Foo();
    arr := arr + [next];
    i := i + 1;
  }
}

我尝试过使用递归并且它可以工作，但我想使用 while 循环来进行说明。有没有其他方法可以克服这个问题？是否有某种“动态”modifies 子句？

【问题讨论】：

标签： loops for-loop dafny

【解决方案1】：

尝试使用fresh，

method main(n: nat)
  requires n > 0 
{
  var first := new Foo();
  var arr: seq<Foo> := [first];
  var i := 1;

  while i < n 
    invariant 0 <= i <= n
    invariant |arr| == i
    invariant fresh(set x | x in arr)
  {
    arr[i-1].x := i;
    var next := new Foo();
    arr := arr + [next];
    i := i + 1;
  }
}

fresh(X) 谓词意味着集合 X 中的对象是从当前方法开始分配的。您始终可以修改新对象，即使它们没有在方法的 modifies 子句中声明。（事实上，fresh 对象甚至不可能出现在 modifies 子句中，因为根据定义，在评估 modifies 子句的时间点没有分配对象。）

请注意，虽然fresh 的意思是“自当前方法开始以来的新鲜事”，而不是当前的while 循环，我已经在这个固定的sn 中完全删除了你的while 循环的modifies 子句-p。我不确定是否可以使您原来的 modifies 子句起作用 - 但您应该能够仅使用方法级别的 modifies 子句和 while-loop 级别的 invariant 子句。

（在这种情况下，没有显式的方法级modifies 子句；因此modifies 子句隐含地是空集。）

【讨论】：