Dafny：数组方法验证的旋转区域

Question

这个证明在 Dafnys 的验证器中给出了一个无限循环：

// Status: verifier infinite loop
// rotates a region of the array by one place forward
method displace(arr: array<int>, start: nat, len: nat) returns (r: array<int>)
  requires arr != null
  requires start + len <= arr.Length
  // returned array is the same size as input arr
  ensures r != null && r.Length == arr.Length
  // elements before the start of the region are unchanged
  ensures arr[..start] == r[..start]
  // elements after the end of the rhe region are unchanged
  ensures arr[(start + len)..] == r[(start + len)..]
  // elements in the region are skewed by one in a positive direction and wrap
  // around
  ensures forall k :: 0 <= k < len
                 ==> r[start + ((k + 1) % len)] == arr[start + k]
{
    var i: nat := 0;
    r := new int[arr.Length];
    // just make a copy of the array
    while i < arr.Length
      invariant i <= arr.Length
      invariant forall k: nat :: k < i ==> r[k] == arr[k]
    {
        r[i] := arr[i];
        i := i + 1;
    }

    i := 0;
    // rotate the region
    while i < len
      invariant 0 <= i <= len
      invariant arr[..start] == r[..start]
      invariant arr[(start + len)..] == r[(start + len)..]
      invariant forall k :: 0 <= k < i 
                ==> r[start + ((k + 1) % len)] == arr[start + k]
    {
        r[start + ((i + 1) % len)] := arr[start + i];
        i := i + 1;
    }
}

这是否指向某种不确定性问题？有没有更好的方法来呈现这个问题来避免无限循环？

以前的版本：

method displace(arr: array<int>, start: nat, len: nat) returns (r: array<int>)
  requires arr != null
  requires start + len <= arr.Length
  // returned array is the same size as input arr
  ensures r != null && r.Length == arr.Length
  // elements before the start of the region are unchanged
  ensures arr[..start] == r[..start]
  // elements after the end of the rhe region are unchanged
  ensures arr[(start + len)..] == r[(start + len)..]
  // elements in the region are skewed by one in a positive direction and wrap around
  ensures forall k :: start <= k < (start + len)
                 ==> r[start + (((k + 1) - start) % len)] == arr[k]
{
    var i: nat := 0;
    r := new int[arr.Length];

    while i < arr.Length
      invariant i <= arr.Length
      invariant forall k: nat :: k < i ==> r[k] == arr[k]
    {
        r[i] := arr[i];
        i := i + 1;
    }

    i := start;

    while i < (start + len)
      invariant start <= i <= (start + len)
      invariant arr[..start] == r[..start]
      invariant arr[(start + len)..] == r[(start + len)..]
      invariant forall k :: start <= k < i
                ==> r[start + (((k + 1) - start) % len)] == arr[k]
    {
        r[start + (((i + 1) - start) % len)] := arr[i];
        i := i + 1;
    }
}

Answer 1

Non-linear 算术不可判定。所以我怀疑使用 % 运算符来定义旋转是你问题的根本原因。下面是一个确实验证过的版本，它仅使用线性整数算法定义旋转。

另见 How does Z3 handle non-linear integer arithmetic?

predicate rotated(o:seq<int>, r:seq<int>) 
  requires |o| == |r|
{
  (forall i :: 1 <= i < |o| ==> r[i] == o[i-1]) &&
  (|o| > 0 ==> r[0] == o[|o|-1])  
}

// Status: verifier infinite loop
// rotates a region of the array by one place forward
method displace(arr: array<int>, start: nat, len: nat) returns (r: array<int>)
  requires arr != null
  requires start + len <= arr.Length
  ensures r != null && r.Length == arr.Length
  ensures arr[..start] == r[..start]
  ensures arr[(start + len)..] == r[(start + len)..]
  ensures rotated(arr[start .. start+len], r[start .. start+len])
{
    var i: nat := 0;
    r := new int[arr.Length];
    while i < start
      invariant i <= start
      invariant forall k: nat :: k < i ==> r[k] == arr[k]
    {
        r[i] := arr[i];
        i := i + 1;
    }

    assert arr[..start] == r[..start];

    if len > 0 {
      r[start] := arr[start+len-1];

      assert r[start] == arr[start+len-1];

      i := start+1;
      while i < start+len
        invariant start < i <= start+len
        invariant arr[..start] == r[..start]
        invariant r[start] == arr[start+len-1]
        invariant forall k: nat :: start < k < i ==> r[k] == arr[k-1]
      {
          r[i] := arr[i-1];
          i := i + 1;
      }
    }

    assert rotated(arr[start .. start+len], r[start .. start+len]);

    i := start+len;
    while i < arr.Length
      invariant start+len <= i <= arr.Length
      invariant arr[..start] == r[..start]
      invariant rotated(arr[start .. start+len], r[start .. start+len])
      invariant forall k: nat :: start+len <= k < i ==> r[k] == arr[k]
    {
        r[i] := arr[i];
        i := i + 1;
    }
}

http://rise4fun.com/Dafny/aysI

Dafny：数组方法验证的旋转区域

Dafny: rotated region of an array method verification

arrays

verification

formal-verification

loop-invariant

dafny