SAVCBS 2006 challenge: specification of iterators

ABSTRACT

A method for formal specification of iterators, which can be used to verify both clients and implementations, is illustrated with a Set abstraction as the underlying collection.

REFERENCES

• 1: Edwards, S. H., "Common Interface Models for Reusable Software", Intl. J. of Softw. Eng. and Knowledge Eng. 3, 2 (June 1993), 193--206.
• 2: Stephen H. Edwards , Wayne D. Heym , Timothy J. Long , Murali Sitaraman , Bruce W. Weide, Part II: specifying components in RESOLVE, ACM SIGSOFT Software Engineering Notes, v.19 n.4, p.29-39, Oct. 1994 [doi>10.1145/190679.190682]
• 3: G. W. Ernst , R. J. Hookway , W. F. Ogden, Modular Verification of Data Abstractions with Shared Realizations, IEEE Transactions on Software Engineering, v.20 n.4, p.288-307, April 1994 [doi>10.1109/32.277576]
• 4: Joseph E. Hollingsworth , Lori Blankenship , Bruce W. Weide, Experience report: using RESOLVE/C++ for commercial software, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.11-19, November 06-10, 2000, San Diego, California, United States
• 5: java.util Package, Interface Iterator <E>, remove Method Detail, http://java.sun.com/j2se/1.5.0/docs/api/java/util/-Iterator.html, viewed 6 Oct. 2006.
• 6: Resolve/C++, http://www.cse.ohio-state.edu/sce/now, viewed 6 Oct. 2006.
• 7: Bruce W. Weide , William F. Ogden , Stuart H. Zweben, Reusable software components, Advances in computers, Academic Press Professional, Inc., San Diego, CA, 1991
• 8: B. W. Weide , S. H. Edwards , D. E. Harms , D. A. Lamb, Design and Specification of Iterators Using the Swapping Paradigm, IEEE Transactions on Software Engineering, v.20 n.8, p.631-643, August 1994 [doi>10.1109/32.310672]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Design, Verification

Keywords:
formal specification, iterators, resolve, verification