Home » forums » LtU Forum

The verified heap sort algorithm

The following article describes a verified version of the heapsort algorithm.

The verified heapsort algorithm is another example on how ghost functions/predicates can be used to describe loop invariants in a exact and concise manner.

By hbrandl at 2012-07-31 19:42 | LtU Forum | previous forum topic | next forum topic | other blogs | 2531 reads