Sorting a Queue

Aug. 17, 2010 – 6 years, 8 months ago, by eifler

Short Description

Specify a user-defined FIFO queue abstract data type (ADT) that is generic (i.e., parameterized by the type of entries in a queue). Verify an operation that uses this component to sort the entries in a queue into some client-defined order.

Code

Specification

Long Description

Dealing with a generic collection type is the issue here. In addition, a mathematical theory suitable for specifying and verifying queue behavior may be needed. Parameterizing the sort operation to account for the specification and computation of the ordering among entries is central. Implementations that involve nested loops may require ghost variables to simplify writing loop invariants.

Variations: Some variations that delay the inevitable generic type issues might
keep the problem easier. If the queue entries are a fixed type with a fixed ordering for sorting, the mathematical definitions and/or new theory to address even this simplified version of the benchmark might be troublesome.

Supplementary Materials

The paper from which this benchmark is taken was published in may 2008 by various authors from Clemson University and the Ohio State University. It contains some more benchmarks which are also included on this site.

Submitted by

Timo Eifler verifythis@cost-ic0701.org