archives

The verified insertion sort algorithm

The following article describes a verified version of the insertion sort algorithm. The insertion sort is one of the simplest sorting algorithms and efficient for small data sets.

In the article it is shown how ghost functions/predicates can be used to keep the loop invariant expressive and readable.

By hbrandl at 2012-07-01 20:53 | LtU Forum | login or register to post comments | other blogs | 5337 reads