Дафни, голландский флаг, инвариант цикла может не поддерживаться циклом

в приведенной ниже программе я создаю что-то вроде проблемы с голландским национальным флагом и следую той же логике, которая также представлена ​​здесь программа сортирует массив из 0, 1 и 2 таким образом, что все 1 в начале, 0 в середине и 2 в конце. [1,1,1,0,0,2,2,2]. но в инвариантах цикла я получаю ошибку This loop invariant might not be maintained by the loop.

изначально i и j имеют индекс 0, а k - последний индекс. логика заключается в том, что j перемещается вверх, если он видит 2, меняется местами с k и k уменьшается, если видит 0, просто j перемещается вверх, а если видит 1, меняет местами i и оба i и j увеличиваются.

код также находится здесь, в rise4fun

        method sort(input: array?<int>)
        modifies input
        requires input !=null;
        requires input.Length>0;
        requires forall x::0<=x<input.Length ==> input[x]==0||input[x]==1||input[x]==2;
        ensures sorted(input);
        {
            var k: int := input.Length;
            var i, j: int := 0 , 0;
            while(j != k )
            invariant 0<=i<=j<=k<=input.Length;
/* the following invariants might not be maintained by the loop.*/
            invariant forall x:: 0<=x<i ==> input[x]==1;
            invariant forall x:: i<=x<j ==> input[x]==0;
            invariant forall x:: k<=x<input.Length ==> input[x]==2;
            invariant forall x:: j<=x<k ==> input[x]==0||input[x]==1||input[x]==2;
            decreases if j <= k then k - j else j - k
            {
                if(input[j] == 2){
                    swap(input, j, k-1);
                    k := k - 1;
                } else if(input[j] == 0){
                    j := j + 1;
                } else {
                    swap(input, i, j);
                    i:= i + 1;
                    j := j + 1;
                }
               }
            }

а вот метод swap и предикат sorted

    predicate sorted(input:array?<int>)
    requires input!=null;
    requires input.Length>0;
    reads input;
    {
        forall i,j::0<=i<j<input.Length ==> input[i]==1 || input[i]==input[j] || input[j]==2
    }

    method swap(input: array?<int>, n:int, m:int)
    modifies input;
    requires input!=null;
    requires input.Length>0;
    requires 0<=n<input.Length && 0<=m<input.Length
    {
        var tmp : int := input[n];
        input[n] := input[m];
        input[m] := tmp;
    }

verification z3 dafny
person Amir-Mousavi    schedule 23.05.2018    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Проблема в том, что swap не имеет постусловия. Постусловие по умолчанию — true, поэтому спецификация swap говорит, что оно изменяет массив произвольным образом.

Когда верификатор видит вызов swap в теле метода sort, он обращает внимание только на спецификацию swap, а не на его тело. Таким образом, после вызова swap в массиве могут быть вообще любые значения, по крайней мере, насколько может сказать верификатор. Поэтому неудивительно, что какой-либо инвариант, относящийся к содержимому массива, не может быть доказан.

Следующая спецификация для swap должна работать:

method swap(input: array?<int>, n:int, m:int)
    modifies input;
    requires input!=null;
    requires input.Length>0;
    requires 0<=n<input.Length && 0<=m<input.Length
    ensures n < m ==> input[..] == old( input[0..n] + [input[m]] + input[n+1..m] + [input[n]] + input[m+1..] ) ;
    ensures n==m ==> input[..] == old(input[..])
    ensures n > m ==> input[..] == old( input[0..m] + [input[n]] + input[m+1..n] + [input[m]] + input[n+1..] ) ;

Так должно ли это

method swap(input: array?<int>, n:int, m:int)
    modifies input;
    requires input!=null;
    requires input.Length>0;
    requires 0<=n<input.Length && 0<=m<input.Length
    ensures input[n] == old( input[m] ) ;
    ensures input[m] == old( input[n] ) ;
    ensures forall i | 0 <= i < input.Length && i != n && i != m :: input[i] == old(input[i])
person Theodore Norvell    schedule 23.05.2018
comment
Отлично, спасибо, теперь намного лучше понял, как работает инструмент - person Amir-Mousavi; 23.05.2018