Метод вставки Dafny, постусловие может не выполняться на этом пути возврата

У меня есть массив "line", в котором содержится строка длины "l", и массив "nl", в котором содержится строка длины "p". Примечание: «l» и «p» не обязательно должны быть длиной каждого соответствующего массива. Параметр «at» будет позицией, в которой будет производиться вставка внутри «строки». Возобновление: Массив длины «p» будет вставлен в «строку», перемещая все символы «строки» между позициями (at,i,at+p), 'p' вправо, чтобы выполнить вставку.

Моя логика для обеспечения состоит в том, чтобы проверить, имеют ли элементы, вставленные в «строку», тот же порядок и те же символы, что и символы, содержащиеся в «nl».

Вот код:

method insert(line:array<char>, l:int, nl:array<char>, p:int, at:int)
  requires line != null && nl != null;
  requires 0 <= l+p <= line.Length && 0 <= p <= nl.Length ;
  requires 0 <= at <= l;
  modifies line;
  ensures forall i :: (0<=i<p) ==> line[at+i] == nl[i]; // error
{
  var i:int := 0;
  var positionAt:int := at;
  while(i<l && positionAt < l)
    invariant 0<=i<l+1;
    invariant at<=positionAt<=l;
  {
    line[positionAt+p] := line[positionAt];
    line[positionAt] := ' ';
    positionAt := positionAt + 1;
    i := i + 1;
  }

  positionAt := at;
  i := 0;
  while(i<p && positionAt < l)
    invariant 0<=i<=p;
    invariant at<=positionAt<=l;
  {
    line[positionAt] := nl[i];
    positionAt := positionAt + 1;
    i := i + 1;
  }
}

Вот ошибки, которые я получаю.

Спасибо.


insert induction loop-invariant formal-verification dafny
person pmpc    schedule 05.04.2016    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Я подозреваю, что ваш алгоритм неверен, потому что он, кажется, не учитывает тот факт, что сдвиг символов, начинающихся с позиции at, на p места, может привести к их записи через конец строки в line.

Мой опыт показывает, что для успешной проверки

  1. Хорошие стандарты разработки кода имеют решающее значение. Правильные имена переменных, форматирование кода и другие правила кодирования еще важнее, чем обычно.
  2. Написание логически простого кода действительно полезно. Старайтесь избегать посторонних дополнительных переменных. Старайтесь упрощать арифметические и логические выражения везде, где это целесообразно.
  3. Если начать с правильного алгоритма, проверка будет проще. Конечно, это легче сказать, чем сделать!
  4. Часто бывает полезно записать самые сильные инварианты циклов, какие только можно придумать.
  5. Работа в обратном направлении от постусловия часто бывает полезной. В вашем случае возьмите постусловие и отрицание условия конечного цикла - и используйте их, чтобы выяснить, каким должен быть инвариант конечного цикла, чтобы подразумевать постусловие. Затем работайте в обратном направлении от этого к предыдущему циклу и т. д.
  6. При манипулировании массивами использование призрачной переменной, которая содержит исходное значение массива в виде последовательности, очень часто является эффективной стратегией. Переменные-призраки не отображаются в выводе компилятора, поэтому не влияют на производительность вашей программы.
  7. Часто полезно записывать утверждения для точного состояния массива, даже если постусловие требует только некоторого более слабого свойства.

Вот проверенная реализация желаемой процедуры:

// l is length of the string in line
// p is length of the string in nl
// at is the position to insert nl into line
method insert(line:array<char>, l:int, nl:array<char>, p:int, at:int)
  requires line != null && nl != null
  requires 0 <= l+p <= line.Length // line has enough space
  requires 0 <= p <= nl.Length // string in nl is shorter than nl
  requires 0 <= at <= l // insert position within line
  modifies line
  ensures forall i :: (0<=i<p) ==> line[at+i] == nl[i] // ok now
{
  ghost var initialLine := line[..];

  // first we need to move the characters to the right
  var i:int := l;
  while(i>at)
    invariant line[0..i] == initialLine[0..i]
    invariant line[i+p..l+p] == initialLine[i..l]
    invariant at<=i<=l
  {
    i := i - 1;
    line[i+p] := line[i];
  }

  assert line[0..at] == initialLine[0..at];
  assert line[at+p..l+p] == initialLine[at..l];

  i := 0;
  while(i<p)
    invariant 0<=i<=p
    invariant line[0..at] == initialLine[0..at]
    invariant line[at..at+i] == nl[0..i]
    invariant line[at+p..l+p] == initialLine[at..l]
  {
    line[at + i] := nl[i];
    i := i + 1;
  }

  assert line[0..at] == initialLine[0..at];
  assert line[at..at+p] == nl[0..p];
  assert line[at+p..l+p] == initialLine[at..l];
}

http://rise4fun.com/Dafny/ZoCv

person lexicalscope    schedule 06.04.2016