Binary heap with array implementation

Oct 7, 2015 at 11:00 PM

Hi everyone,

I was working on a Binary Heap specification, namely a pretty standard deleteMax operation, but it seems it's more complex than I thought. Dafny tells that loop invariants are not maintained. Any suggestions?

Thanks,
João Pascoal Faria
Assistant Professor, Faculty of Engineering, University of Porto, Portugal
class {:autocontracts} BinaryHeap {
    var heap : array<int>; // heap contents
    var used : int; // number of positions used

    // Auxiliary definitions   
    function method parent(i: int) : int  
    requires i > 0  
    { (i - 1) / 2 }  
    
    function method leftChild(i: int) : int 
    requires i >= 0   
    { 2 * i + 1 }   
    
    function method rightChild(i: int) : int 
    requires i >= 0  
    { 2 * i + 2 }
  
    predicate isMax(a: array<int>, used: int, m: int)
    requires a != null;
    requires 0 < used <= a.Length;
    reads a;
    { 
        (exists i:: 0 <= i < used && a[i] == m)
        && (forall i:: 0 <= i < used ==> a[i] <= m)
    }

    // Heap invariant 
    predicate Valid() 
    {
        heap != null && 0 <= used <= heap.Length  &&
        (forall i:: 0 < i < used ==> heap[parent(i)] >= heap[i])    
    }
 
    // Heap constructor
    constructor(initialCapacity: int)   
    requires initialCapacity >= 0; 
    ensures heap.Length == initialCapacity; 
    ensures used == 0;
  {
        heap := new int[initialCapacity];
    used := 0;
    }   
  
    // Removes the maximum element from the heap (located at front)
    method deleteMax() returns (max: int)
     requires used >  0 ; 
    {
    // takes the maximum from the head 
    max := heap[0];

    // moves the last element to the head
    heap[0] := heap[used - 1];
    used := used - 1;

    // reorganize the heap, moving down the element in position 0 as needed
    var i: int := 0;
    while (true)
     decreases used - i
     invariant 0 <= i <= used < heap.Length
     invariant heap != null 
     invariant forall k :: 0 < k < used && parent(k) != i ==> heap[parent(k)] >= heap[k]
     invariant i > 0 && leftChild(i) < used ==>  heap[parent(i)] >= heap[leftChild(i)]
     invariant i > 0 && rightChild(i) < used ==> heap[parent(i)] >= heap[rightChild(i)]
     modifies heap
    {
      var child : int := leftChild(i);  // left child
      if (child >= used)
      { break; }
      if (child+1 < used && heap[child+1] > heap[child])
      { child := child + 1; } // right child
            if (heap[i] >= heap[child])
      { break; }
      heap[child], heap[i] := heap[i], heap[child];
      i := child;
    }
  }
}