June 22, 2010 – 6 years, 10 months ago, by eifler
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.
Part 2: Verification
Verify an adapter from Apache Beehive that implements an Iterator interface in terms of the JDBC ResultSet.
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.
Solutions for verification 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.
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.
This benchmark was taken from the workshop for Specification and Verification of Component-Based Systems SAVCBS'09
Timo Eifler firstname.lastname@example.org