Инвариант Дафни-цикла не поддерживается циклом - PullRequest
Новая
       6

Инвариант Дафни-цикла не поддерживается циклом

0 голосов
/ 25 ноября 2018

мне нужно создать предварительные и положительные условия для вставки метода класса кучи, куча должна быть minHeap и должна быть завершена, мой инвариант имеет ошибку, которая говорит: «этот инвариант цикла может не поддерживатьсяпо петле. "

    class Heap {
var size: nat
var heap: array<int>
method insert (x: int)
    modifies heap
    requires 0 < size < heap.Length - 1
    requires minHeap(heap, size)
    requires x > 0
    requires isComplete(heap, size)
    ensures minHeap(heap, size + 1)
    ensures isComplete(heap, size + 1)
    ensures exists i :: 0 < i < size + 1 && x == heap[i]
    {
        // Insert the new item at the end of the array 
        var pos:= size + 1;
        // Percolate up
        while pos > 1 && x < heap[pos/2]
        invariant 1 <= pos < heap.Length
        invariant forall i :: pos < i <= size + 1 ==> heap[i] < heap[i/2]
        {

            heap[pos] := heap[pos/2];
            pos:= pos/2;
        }
        heap[pos] := x;
    }

    predicate minHeap(h: array<int>, index: nat)
    reads h
    requires 0 < index < h.Length 
    {
        forall i :: 1 < i < index ==> h[i/2] < h[i]
    } 

    predicate isComplete(h: array<int>, index: nat)
    reads h 
    requires 0 < index < h.Length
    {
        forall i :: 1 <= i <= index ==> h[i] > 0
    }
  }

Кто-нибудь может мне помочь?

1 Ответ

0 голосов
/ 01 декабря 2018

Предположим, что инвариант цикла выполняется в начале итерации, когда pos равно 100.Тогда вы знаете 

forall i :: 100 < i <= size+1 ==> heap[i] < heap[i/2]

в начале итерации цикла.То есть вы знаете что-то о heap[i] для всех i больше, чем 100 (до size+1).Итерация цикла теперь устанавливает heap[100] в значение heap[50] и pos в 50.Чтобы доказать, что инвариант цикла поддерживается, вам нужно будет показать: 

forall i :: 50 < i <= size+1 ==> heap[i] < heap[i/2]

Но это условие определенно не выполняется.Одна из проблем заключается в том, что оно не выполняется для i == 100, поскольку heap[100] равно равно heap[50], не менее строго heap[50] в качестве состояний инварианта вашего цикла.Другая проблема состоит в том, что у вас нет информации о значениях heap[51], ..., heap[99], и ваш инвариант цикла говорит, что вы намерены также удовлетворить каждое из них heap[i] < heap[i/2].

Итак, вам нужно переосмыслитьпрограмма или инвариант, или оба.

...