Дафни L oop Инвариант может не держаться - PullRequest
Новая
       56

Дафни L oop Инвариант может не держаться

0 голосов
/ 19 февраля 2020

Это простое разделение 0 и 1 в задаче массива. Я не могу понять, почему инвариант l oop не выполняется. 

method rearrange(arr: array<int>, N: int) returns (front: int)
    requires N == arr.Length
    requires forall i :: 0 <= i < arr.Length ==> arr[i] == 0 || arr[i] == 1
    modifies arr
    ensures 0 <= front <= arr.Length
    ensures forall i :: 0 <= i <= front - 1 ==> arr[i] == 0
    ensures forall j :: front <= j <= N - 1 ==> arr[j] == 1
{
    front := 0;
    var back := N;
    while(front < back)
        invariant 0 <= front <= back <= N
        invariant forall i :: 0 <= i <= front - 1 ==> arr[i] == 0
        // The first one does not hold, the second one holds though
        invariant forall j :: back <= j < N ==> arr[j] == 1
    {
        if(arr[front] == 1){
            arr[front], arr[back - 1] := arr[back - 1], arr[front];
            back := back - 1;
        }else{
            front := front + 1;
        }
    }
    return front;
}

1 Ответ

1 голос
/ 25 февраля 2020

При входе в ваш метод предусловие сообщает вам 

forall i :: 0 <= i < arr.Length ==> arr[i] == 0 || arr[i] == 1

Итак, в то время известно, что все элементы массива либо 0, либо 1. Однако, поскольку массив изменяется с помощью l oop, вы должны упомянуть в инвариантах all то, что вы все еще хотите запомнить о содержимом массива.

Другими словами, чтобы убедиться, что тело l oop поддерживает инвариант, представьте, что тело l oop начинается с произвольного состояния, удовлетворяющего инварианту. Вы можете иметь в виду, что элементы массива остаются 0 или 1, но ваш инвариант этого не говорит. Вот почему вы не можете доказать, что инвариант l oop поддерживается.

Чтобы решить эту проблему, добавьте 

forall i :: 0 <= i < arr.Length ==> arr[i] == 0 || arr[i] == 1

как инвариант al oop.

Rustan

...