### Abstract

Stepwise program refinement techniques can be used to simplify program verification. Programs are better understood since their main properties are clearly stated, and verification of rather complex algorithms is reduced to proving simple statements connecting successive program specifications. Additionally, it is easy to analyze similar algorithms and to compare their properties within a single formalization. Usually, formal analysis is not done in educational setting due to complexity of verification and a lack of tools and procedures to make comparison easy. Verification of an algorithm should not only give correctness proof, but also better understanding of an algorithm. If the verification is based on small step program refinement, it can become simple enough to be demonstrated within the university-level computer science curriculum. In this paper we demonstrate this and give a formal analysis of two well known algorithms (Selection Sort and Heap Sort) using proof assistant Isabelle/HOL and program refinement techniques.

### License

BSD License

### Topics

- Computer science/Algorithms

### Session Selection_Heap_Sort

- Sort
- RemoveMax
- SelectionSort_Functional
- Heap
- HeapFunctional
- HeapImperative

## Cite

×

Selection_Heap_Sort-AFP

    @article{Selection_Heap_Sort-AFP,
      author  = {Danijela Petrovic},
      title   = {Verification of Selection and Heap Sort Using Locales},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/Selection_Heap_Sort.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Feb 18, 2014 : Isabelle2013-2