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:
- 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.
- 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).
- 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:
- 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).
- 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
jonathan.aldrich@cs.cmu.edu.
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.
References
- Javadoc for the java.sql package
- .NET documentation for the SqlConnection, SqlCommand, and SqlDataReader classes.
-
The Apache Beehive ResultSetIterator implementation
