Binary Heaps for IMP2

Simon Griebel

June 13, 2019

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

In this submission array-based binary minimum heaps are formalized. The correctness of the following heap operations is proved: insert, get-min, delete-min and make-heap. These are then used to verify an in-place heapsort. The formalization is based on IMP2, an imperative program verification framework implemented in Isabelle/HOL. The verified heap functions are iterative versions of the partly recursive functions found in "Algorithms and Data Structures – The Basic Toolbox" by K. Mehlhorn and P. Sanders and "Introduction to Algorithms" by T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein.

License

BSD License

Topics

Session IMP2_Binary_Heap