Layered Implementation of a Map ADT

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

Short Description

Verify an implementation of a generic map abstract data type (ADT), where the data representation is layered on other built-in types and/or ADTs.

Code

Specification

Long Description

This benchmark involves issues of proof of correctness of data representation, including representation invariants and abstraction relations. There are many versions of “map” behavior, including impoverished ones that obscure important issues. The map designed for this benchmark should be as useful to clients as, say, maps in the java.util package. If any of the map operations involves relational behavior, a careful definition of correctness might be subtle.

Variations: A simple data representation such as a queue with linear search as the primary algorithm is an obvious starting point. There are many other data structures and algorithms with better performance that are more realistic (e.g., hash tables of various ilks, binary search trees with or without balancing). Each of these alternatives might involve specifying other interesting ADTs as the basis for the data representation. Additional issues might arise from this exercise.

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