Verification of an In-place Quicksort in ACL2

S. Ray and R. Sumners

In D. Borrione, M. Kaufmann, and J S. Moore, editors, Proceedings of the 3rd International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2002), Grenoble, France, April 2002, pages 204-212

Abstract

We present a proof of an efficient, in-place Quicksort implementation using single-threaded objects (stobjs) in ACL2. We demonstrate that the Quicksort implementation is equivalent to a simple insertion-sort function that is shown to produce an ordered permutation of its input. For ease of reasoning, the demonstration is carried out by verifying a series of "intermediate" sorting functions. The intermediate functions are equivalent to the efficient Quicksort implementation, but written in a more applicative style, and hence easier to reason about. We then decompose the proof into a verification of the equivalence of the efficient implementation with an intermediate implementation, and a proof of correctness of the intermediate implementation. We show how this decomposition allows us to simplify our reasoning about stobjs and obtain a cleaner proof of the implementation.

Relevant files

Paper (ps, pdf)
Slides for ACL2 2002 (ps, pdf)
Supporting materials: See the directory books/workshops/2002/ray-sumners/support/ in the current ACL2 distribution. (Note: You need the workshops tarball. See the instructions for installing ACL2 in the ACL2 homepage.)

BibTex

@Inproceedings{ray-verification,
  title     = "{Verification of an In-place Quicksort in ACL2}",
  author    = "S. Ray and R. Sumners",
  editor    = "D. Borrione and M. Kaufmann and J S. Moore",
  booktitle = "{$3$rd International Workshop on the ACL2 Theorem Prover and Its Applications
                (ACL2 2002)}",
  address   = "{Grenoble, France}",
  pages     = "204-212",
  month     = apr,
  year      = "2002"
}