Imperative Insertion Sort

Christian Sternagel 📧

September 25, 2014

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

The insertion sort algorithm of Cormen et al. (Introduction to Algorithms) is expressed in Imperative HOL and proved to be correct and terminating. For this purpose we also provide a theory about imperative loop constructs with accompanying induction/invariant rules for proving partial and total correctness. Furthermore, the formalized algorithm is fit for code generation.

License

BSD License

Topics

Session Imperative_Insertion_Sort

Cite

× 
@article{Imperative_Insertion_Sort-AFP,
  author  = {Christian Sternagel},
  title   = {Imperative Insertion Sort},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2014},
  note    = {\url{https://isa-afp.org/entries/Imperative_Insertion_Sort.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: