SAVCBS Logo Challenge Problem
Workshop at
November 10-11, 2006

Challenge Problem: Iterator Specification

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

A common programming pattern is to componentize the mechanism for iterating over the elements of a collection. This concept of an iterator is implemented in Java and C# (among other languages) via a set of interfaces such as IEnumerable and IEnumerator (and their generic brethren). At a minimum, collections must have a method that returns an enumerator; and enumerators must have a method that returns the current element in the iteration and a method that advances the enumerator to the next element.

There may be many iterators in existence for a particular collection, but a common constraint is that modifications to the underlying collection may invalidate an iterator. That is, any further operations on an invalid interator leads to exceptional termination. For instance, in Java when the collection is modified through an iterator, that iterator remains valid but all other iterators are invalidated; in C# iterators are read-only and all iterators are invalidated. Solutions may consider either the C# or the Java semantics, or restrictions or enhancements of either.

For our challenge problem session, we invite participants to illustrate their specification and verification techniques on the problem of specifying the behavior of iterators and clients that use them. Solutions should be clear as to the assumptions made (e.g., sequential programs vs. multi-threaded programs), 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.

Submission Details

Solutions continue to be accepted as workshop space permits.

Prospective authors should submit their solutions by email to Submit documents in PDF or PS format, with a maximum length of 4 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 but will not be part of the proceedings.

Jonathan Aldrich, Mike Barnett, Dimitra Giannakopoulou, Gary T. Leavens, and Natasha Sharygina

$Date: 2008/06/02 21:21:38 $

Valid HTML 4.0!