Deriving an Applicative Heapsort Algorithm

This page contains information about the development of the Heapsort algorithm. We have carried out a formal derivation of Heapsort using the program transformation system ULTRA.

To be able to reproduce the results, the version of ULTRA that we used for the derivation is available (only a few corrections have been made to the official version 2.2). That file also contains the complete source code including the derivation protocols (see the directory heapsort).

Technical Report

The derivation of Heapsort is described in the technical report UIB-2002-02 (available as DVI.tar.gz, PS, PDF). There is an extended version of the technical report that contains the derivation protocols (as DVI.tar.gz, PS, PDF). See the section below for the derivation protocol files.

Appendix D: Source code

The source code, as referenced in Appendix D of the technical report, consists of the project file, 10 theory files, and one Haskell file that contains the result:

1. project
2. general.thy
3. general-derived.thy
4. bag.thy
5. bag-derived.thy
6. tree.thy
7. tree-derived.thy
8. tree-added.thy
9. sort.thy
10. sort-derived.thy
11. sort-added.thy
12. heapsort.hs

Appendix E: Derivation Protocols

The derivation protocols, as referenced in Appendix E of the technical report, consist of 30 text files generated by ULTRA:

1. commutativity_transitivity.protocol
2. composetree_recursive.protocol
3. decomposetree_recursive.protocol
4. equals_abstr_some_heap_equals_abstr.protocol
5. equals_empty_nonempty.protocol
6. equals_empty_union_abstr_abstr.protocol
7. heap_composetree.protocol
8. heap_equals_nonempty_abstr_abstr_insert.protocol
9. heap_equals_union_abstr_abstr_abstr_remove.protocol
10. heap_equals_union_union_abstr_abstr.protocol
11. heap_equals_union_union_single_abstr.protocol
12. heap_removemin.protocol
13. heap_sorted_equals_elements_abstr.protocol
14. insert_recursive.protocol
15. introduce_composetree.protocol
16. introduce_removemin.protocol
17. main_development.protocol
18. removemin_recursive.protocol
19. some_heap_equals_empty_abstr.protocol
20. some_heap_equals_nonempty_abstr.protocol
21. some_heap_equals_union_abstr_abstr.protocol
22. some_heap_equals_union_abstr_empty.protocol
23. some_heap_equals_union_empty_abstr.protocol
24. some_heap_insert_1.protocol
25. some_heap_insert_2.protocol
26. some_heap_remove_1.protocol
27. some_heap_remove_2.protocol
28. some_simplification_general.protocol
29. some_sorted_equals_elements_empty.protocol
30. union_union_single.protocol