Specifying java iterators with JML and Esc/Java2

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Specifying java iterators with JML and Esc/Java2

Full text

Pdf (147 KB)

Source

International Conference on Software Engineering archive
Proceedings of the 2006 conference on Specification and verification of component-based systems table of contents

Portland, Oregon

SESSION: Challenge problem solutions table of contents

Pages: 71 - 74

Year of Publication: 2006

ISBN:1-59593-586-X

Author

David R. Cok

Eastman Kodak Company, NY

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 15, Downloads (12 Months): 46, Citation Count: 1

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1181195.1181210 What is a DOI?

ABSTRACT

The 2006 SAVCBS Workshop has posed a Challenge Problem on the topic of specifying iterators. This note provides a specification in the Java Modeling Language (JML) [1, 2] for the Java interfaces Iterator and Iterable that captures the interactions between these two interfaces. An example program that uses these interfaces is checked using Esc/Java2 [3, 4, 5], demonstrating by example that the Esc/Java2 tool checks that the interfaces are used only as required by the specifications. The concluding section contains some observations on the limitations of JML for this specification task.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Many references to papers on JML can be found on the JML project website, http://www.cs.iastate.edu/~leavens/JML/papers.shtml.
	2	L. Burdy, et al. An overview of JML tools and applications. In T. Arts and W. Fokkink, editors, Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 03), volume 80 of Electronic Notes in Theoretical Computer Science (ENTCS), pages 73--89. Elsevier, June 2003.
	3	D. R. Cok and J. Kiniry. ESC/Java2: Uniting ESC/Java and JML. Technical report, University of Nijmegen, 2004. NIII Technical Report NIII-R0413.
	4	D. R. Cok and J. Kiniry. ESC/Java2 : Uniting ESC/Java and JML. Progress and issues in building and using ESC/Java2 and a report on a case study involving the use of ESC/Java2 to verify portions of an internet voting tally system. Lecture Notes in Computer Science, 3362:108--128, Jan. 2005.
	5	Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany