Constant Time Sparse Array

March 3, 2011 – 6 years, 1 month ago, by sarahgrebing

Short Description

For this benchmark, the task is to implement and verify an array where all three basic
operations (create, get, and set) take constant time
Verify that the program meets the usual abstract interface of an array.

Code

class SparseArray {
 int val[MAXLEN];
 uint idx[MAXLEN], back[MAXLEN];
 uint n;
 static SparseArray create(uint sz) {
  SparseArray t = new SparseArray();
  n = 0;
 }
 int get(uint i) {
  if (idx[i] < n && back[idx[i]] == i) return val[i];
  else return 0;
 }
 void set(uint i, int v) {
  val[i] = v;
  if (!(idx[i] < n && back[idx[i]] == i)) {
   assert(n < MAXLEN); // (*), see Verification Tasks
   idx[i] = n; back[n] = i; n = n + 1;
  }
 }
}


void sparseArrayTestHarness() {
 SparseArray a = create(10), b = create(20);
 assert(a.get(5) == 0 && b.get(7) == 0);
 a.set(5, 1); b.set(7, 2);
 assert(a.get(5) == 1 && b.get(7) == 2);
 assert(a.get(0) == 0 && b.get(0) == 0);
}

Specification

Long Description

For this benchmark, the task is to implement and verify an array where all three basic
operations (create, get, and set) take constant time (Exercise 2.12 in [0]; see also
[1] p. 271). Any memory requested from the underlying memory allocator (typically
malloc() or new) should be treated as containing arbitrary values. The solution should
use three arrays: one for the actual values stored in the array, and two more for marking
which indices are already initialized, as in the program (class SparseArray).

Verify that the program above meets the usual abstract interface of an array. The
get() and set() methods should require the index to be within bounds, and the create()
method may require that sz <= MAXLEN.
In a language like Java, the internal arrays allocated by the class above would already
be 0-initialized; however, our benchmark stipulates that the implementation is not
allowed to make use of that fact in the verification. One way to ensure that is to make
the constructor take the arrays as input.
The following test harness should be verified without looking at the particular implementation
of the array.

Verification Tasks:

  1. Verify the correctness of the array implementation against your specification, assuming n < MAXLEN at the place marked with (*) in the code. Also, verify thecorrectness of the test harness using the specifications of the array. 50 points.
  2. As above, but without the assumption (*). In other words, verify that the assertionholds (which ensures that the program does not reference the array outside itsbounds). 30 points.

Supplementary Materials

The paper from which this benchmark is taken was published in may 2010 by K. Rustan M. Leino and Michal Moskal. It contains some more benchmarks which are also included on this site.
Information about the scoring system and the pseudo-code description of the programs can be found here.

Submitted by

Sarah Grebing