## Binary Heap

*March 3, 2011 – 6 years ago, by sarahgrebing*

### Short Description

Verify properties of a binary heap and a heap sort method.

### Code

class Heap { static Heap create(uint sz); void insert(int e); int extractMin(); } void heapSort(int[] arr, uint len) { uint i; Heap h = create(len); for (i = 0; i < len; ++i) h.insert(arr[i]); for (i = 0; i < len; ++i) arr[i] = h.extractMin(); } void heapSortTestHarness() { int[] arr = { 42, 13, 42 }; heapSort(arr, 3); assert(arr[0] <= arr[1] && arr[1] <= arr[2]); assert(arr[0] == 13 && arr[1] == 42 && arr[2] == 42); }

### Specification

### Long Description

A binary min-heap (see [2], Chapter 6) is a nearly full binary tree, where the nodes

maintain the heap property, that is, each node is smaller than each of its children. The

heap should be stored in an integer-indexed collection (e.g., an array). The following

three operations should be provided create, insert, extract (as given by the class signature).

The create(sz) method creates a new heap of maximum capacity sz (this restriction

is optional). The insert() method should allow inserting an element multiple

times so that extractMin() will return it multiple times.

The test harness consists of two procedures to be verified separately: a simple implementation

of heap sort, and one use case.

Verification Tasks

- Verify the that the heap sort returns an array that is sorted (in particular, verify thefirst assertion in the harness). 40 points.
- Verify that the heap represents a multiset, and thus that the heap sort produces apermutation of the input (in particular, verify the second assertion). 40 points.

### Supplementary Materials

The paper from which this benchmark is taken was published in may 2010 by K. Rustan M. Leino and Michal Moskal. It contains some more benchmarks which are also included on this site.

Information about the scoring system and the pseudo-code description of the programs can be found here.

### Submitted by

Sarah Grebing