Linked-List Implementation of a Queue ADT
Aug. 17, 2010 – 6 years, 8 months ago, by eifler
Based on the benchmark: Sorting a Queue
Verify an implementation of the queue type specified for the benchmark "Sorting a Queue", using a linked data structure for the representation.
Pointers/references may be either built-in types in the programming language or user-defined types. Specifications for their behavior, and verification of linked data structures that use them, raise many interesting questions. Most obvious is that control of aliasing becomes an issue. If this is not addressed carefully, retaining modularity of verification might be difficult.
Variations: A linked data structure might be encoded in an array with integer indices, so issues related to linked data structures are separated from issues related to language-defined pointers/references as a way of introducing indirection. If memory is allocated dynamically, then memory might be assumed to be unbounded or bounded, the latter raising the specter of memory allocation that does not always succeed. The queues themselves might be specified to be unbounded, or bounded in various ways (e.g., uniformly bounded so each queue has the same maximum length, or communally bounded so the sum of the lengths of all queues is bounded).
Here is a link to the paper Full Functional Verification of Linked Data Structures by Karen Zee, Viktor Kuncak and Martin C. Rinard.
The paper from which this benchmark is taken was published in may 2008 by various authors from Clemson University, Clemson and the Ohio State University, Columbus. It contains some more benchmarks which are also included on this site.
Timo Eifler email@example.com