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

я должен создать условия pre и pos для метода вставки класса кучи, куча должна быть 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
    }
  }   

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