SAVCBS Logo Challenge Problem for
Workshop at
August 25, 2009

Challenge Problem: Database Library Specification

One session during this year's workshop will be devoted to presenting solutions (full or partial) to the following challenge problem.

Part 1: Specification

Choose either the JDBC (java.sql) library in Java or the ODBC (System.Data and/or System.Data.SqlClient) library in Microsoft ADO.NET. Specify a core subset of the library, e.g. parts of Connection, Statement, and ResultSet for JDBC. Interesting results might address one of the following specification challenges in these libraries:

  1. Coordination among related objects: A Statement cannot be used after its Connection is closed. Likewise, a ResultSet cannot be used after its Statement is closed.
  2. Complex, multi-dimensional, multi-modal interface: The ResultSet JDBC interface supports multiple mode choices in how to access a set of database results. It maintains a cursor which is initially positioned before the first row, is moved by next(), and will eventually be positioned beyond the last row (at which point next() returns false). When at a row, data can be read, but columns should be read in left-to-right order and each column should only be read once. Some ResultSets support scrolling backwards, others do not. Some ResultSets allow updating the current row by calling an update function and then calling updateRow. Updateable ResultSets also have a special "insertion row" in which no data can be read, but data can be written with update functions before calling insertRow() to add the row to the database. There is also an interesting treatment of database null values: if a value is read with getInt() and 0 is returned, this might be due to a 0 in the database or a null in the database. The wasNull() method distinguishes these, but can only meaningfully be called after getInt() (or similar functions).
  3. Asynchrony: The ADO.NET class SqlCommand supports asynchronous queries with methods like BeginExecuteReader, which accepts a callback to be invoked when the query returns. In addition to the challenges of specifying the behavior of the callback argument, the SqlCommand cannot be used in any other way until an asynchronous query returns.

Part 2: Verification

Verify an adapter from Apache Beehive that implements an Iterator interface in terms of the JDBC ResultSet. Solutions may address one or more of the following challenges:
  1. ResultSet is Iterator-like, but the interface mismatches are interesting. In particular, the Iterator interface has a test method to find out if there is another row available, but ResultSet can only be tested for more data by advancing to the next row. This creates more interesting invariants in the implementation than one would expect for a conceptually simple task. More subtly, many specification approaches would specify that Iterator.hasNext() is a pure method (with no effects), but the Apache implementation is actually effectful (and in fact it must be if we want to check lazily for more rows in the ResultSet).
  2. The particular implementation strategy used by ResultSetIterator is also interesting, as the ResultSet is aliased in the RowMapper. There may therefore be interesting aliasing-related challenges in ensuring that the ResultSetIterator uses the ResultSet according to its specification.

Submission Details

Solutions should be clear as to the assumptions made, the level of annotation required, any restrictions (e.g. aliasing) that the technique imposes on code, and the difficulty and amount of automation used in the verification. They should illustrate innovative features of your particular specification or verification techniques. Solutions may be full or partial. The session is open to both presenters and participants of the workshop.

The priority deadline for submission will be 2 weeks before the ESEC/FSE early registration deadline, with responses to authors provided in time for them to register for the workshop. Solutions will continue to be accepted after this date as workshop space permits. Prospective authors should email their solutions to Questions about the challenge problem can be sent to the same address. Submit documents in PDF (or PS) format, with a maximum length of 6 pages. Solutions will be reviewed by 2 PC members, and if accepted, authors will have about 10 minutes (including 3 minutes for questions) to present their solution in the workshop. Solutions will be made available on the SAVCBS web site and will be part of the proceedings. Note that publication at SAVCBS will not preclude submitting the same work elsewhere.


  1. Javadoc for the java.sql package
  2. .NET documentation for the SqlConnection, SqlCommand, and SqlDataReader classes.
  3. The Apache Beehive ResultSetIterator implementation