Дафни: повернутая область проверки массива методом

Question

Это доказательство дает бесконечный цикл в верификаторе Дафниса:

// 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

Нелинейная арифметика не разрешима. Так что я подозреваю, что используя % Оператор для определения поворота является основной причиной вашей проблемы. Ниже приведена версия, которая проверяет, что определяет вращение, используя только линейную целочисленную арифметику.

См. Также Как Z3 обрабатывает нелинейную целочисленную арифметику?

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