
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;
}
}
}

