Aug. 17, 2010 – 6 years, 8 months ago, by eifler
Verify a client program that uses an iterator for some collection type, as well as an implementation of the iterator.
There are many proposed designs for iterators, each of which raises a number of interesting specification and verification issues that involve coupling between an underlying collection type and an iterator for it. Specifying iterators (though not verifying anything about them) was a challenge problem issued for the SAVCBS Workshop in 2006.
Variations: Iterators may be active or passive. Each design has its own set of problems. A passive iterator, where an operation is passed to the iterator and the iterator applies it to each entry, starts to raise issues similar to those involved in callbacks.
This benchmark was also proposed as a challenge in the workshop for Specification and Verification of Component-Based Systems SAVCBS'06
The paper from which this benchmark is taken was published in may 2008 by various authors from Clemson University, Clemson and the Ohio State University, Columbus. It contains some more benchmarks which are also included on this site.
Timo Eifler email@example.com