Inorder Traversal of a Binary Heap and its Inversion in Optimal Time and Space

. In this paper we derive a linear-time, constant-space algorithm to construct a binary heap whose inorder traversal equals a given sequence. We do so in two steps. First, we invert a program that computes the inorder traversal of a binary heap, using the proof rules for program inversion by W. Chen and J.T. Udding. This results in a linear-time solution in terms of binary trees. Subsequently, we data-refine this program to a constant-space solution in terms of linked structures. 1 Introduction In [7] an elegant sorting algorithm is presented which exploits the presortedness of the input sequence. The first step of this variant of Heapsort comprises the conversion of the input sequence in a "mintree," i.e., a binary heap whose inorder traversal equals the input sequence. 1 For this conversion, the authors of [7] provide a complicated, yet linear algorithm, consisting of no fewer than four repetitions. In this paper we show that the practical significance of the sorting algorithm can..