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

Question

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

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

Вот the code:

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

Вот в errors, что я получаю.

Спасибо.

Answer 1

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

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

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