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

Last changes 2002.12.10, Walter Guttmann