A binary min-heap without duplicated elements is a binary tree which satisfies
two properties:
1. the value of each node is (strictly) greater then the value of its parent,
with the minimum-value element at the root (this is the min-heap
property), and
2. is complete.
Binary heaps have efficient implementations on arrays. There are logarithmic
algorithms to insert an element in a heap and to remove the minimum
element from an heap. We concentrate on the former.
Consider the below class featuring a partial implementation of a binary
min-heap. The root is the second item in the array. We skip the index zero cell
of the array for the convenience of implementation.1
class Heap {
var s ize : nat ;
var heap: array <int >;
method i n s e r t ( x: i nt )
requires minHeap ( )
ensures minHeap ( )
{
/ / I n s e r t the new item at the end of the array
var pos := s ize + 1;
/ / Perco late up
while pos > 1 && x < heap [ pos / 2 ] {
heap [ pos ] := heap [ pos / 2 ] ;
pos := pos / 2 ;
heap [ pos ] := x ;
}
}
Write predicate minHeap() and add the necessary contract and annotations to
method insert () so that Dafny accepts the code. In method insert, assume that
there is enough room in the heap array to contain the new element.
Suggestion: proceed in two steps.
1. Start with the quasi binary heap property.
2. Once this is working proceed to show that the complete binary tree
property is preserved by method insert ().
Hello I am C++, Java and algorithm expert and interested in this project. I have reviewed details and confident to handle the project perfectly. I will keep codes simple and well documented. I can start now. Please share more details so we can discuss further. Regards, anshu