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

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

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

arrays verification loop-invariant formal-verification dafny
person vivichrist    schedule 12.01.2016    source источник
comment
Что вы подразумеваете под бесконечным циклом? Вы имеете в виду, что время проверки Dafny истекло? Пробовали ли вы использовать некоторые из аргументов командной строки Dafny, в частности, параметры продолжения разделения?   -  person lexicalscope    schedule 14.01.2016
comment
хм, нет, я понятия не имел, что такой аргумент существует или что он делает, но я просто нуб ... Я имел в виду, что запуск dafny, подобный этому './dafny blah/displace.dfy' из подсказки в Linux, кажется, запускается чертовски долго.   -  person vivichrist    schedule 03.02.2016
comment
Обычно вы должны передать значение опции тайм-аута при запуске Dafny из командной строки. Мой опыт показывает, что почти все процедуры, которые собираются проверить, делают это относительно быстро. Большинство лемм, которые я написал, проверяются в течение 10 секунд, некоторые занимают до 60 секунд, почти никогда они не занимают более 60 секунд, но все равно проверяются в течение времени, которое я готов ждать. Я почти никогда не хочу запускать Дафни без установки тайм-аута.   -  person lexicalscope    schedule 03.02.2016

Ответы (1)


arrow_upward
1
arrow_downward

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

См. также Как 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

person lexicalscope    schedule 13.01.2016