Dafny - Binary min-heap Software Verification

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 ().