Formal verification for a C0 implementation of the heapsort algorithm

In this article we report on formal software verification for the C0 implementation of the heapsort algorithm for an array of an arbitrary data type. The working steps include the development of an algorithm specification, writing a program code, code translation into the Isabelle/HOL environment, performing a correctness proof showing equivalence between the program implementation and its specification.