# 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"
}