Typestate protocol specification in JML

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Typestate protocol specification in JML

Full text

Pdf (535 KB)

Source

Foundations of Software Engineering archive
Proceedings of the 8th international workshop on Specification and verification of component-based systems table of contents

Amsterdam, The Netherlands

SESSION: Session 1 table of contents

Pages 11-18

Year of Publication: 2009

ISBN:978-1-60558-680-9

Authors

Taekgoo Kim	Carnegie Mellon University, Pittsburgh, PA, USA
Kevin Bierhoff	Carnegie Mellon University, Pittsburgh, PA, USA
Jonathan Aldrich	Carnegie Mellon University, Pittsburgh, PA, USA
Sungwon Kang	KAIST, Daejon, South Korea

Sponsors

ACM: Association for Computing Machinery
SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 7, Downloads (12 Months): 19, Citation Count: 0

Additional Information:

abstract references index terms

Tools and Actions:	Request Permissions 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/1596486.1596490 What is a DOI?

ABSTRACT

The Java Modeling Language (JML) is a language for specifying the behavior of Java source code. However, it can describe the protocols of Java classes and interfaces only implicitly. Typestate protocol specification is a more direct, lightweight and abstract way of documenting usage protocols for object-oriented programs. In this paper, we propose a technique for incorporating the typestate concept into JML for specifying protocols of Java classes and interfaces, based on our previous research on typestate protocol specifications [4]. This paper presents a set of formal translation rules for encoding typestate protocol specifications into pre/post-condition specifications. It shows how typestate protocol specifications can be mixed with pre/post-condition specifications and how violations of code contracts in inheritance can be handled. Finally, our proposed technique is demonstrated within the Java/JML environment to show its effectiveness.

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	G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06-rev28, Iowa State University Department of Computer Science, July 2005.
	2	Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, and Daniel M. Zimmerman. JML reference manual. Available at http://www.eecs.ucf.edu/~leavens/JML/jmlrefman/, retrieved June 2009.
	3	Jean-Raymond Abrial, Stephen A. Schuman and Bertrand Meyer. A Specification Language. In On the Construction of Programs, Cambridge University Press, 1980.
	4	Kevin Bierhoff and Jonathan Aldrich, Lightweight Object Specification with Typestates. In Foundations of Software Engineering, September 2005.
	5	Edmund M. Clarke, Jeannette M. Wing, et al., Formal Methods: State of the Art and Future Directions. ACM Computing Surveys, Vol. 28, No. 4, December 1996.
	6	R. E. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering, 12:157--171, 1986
	7	R. DeLine and M. Fähndrich. Typestates for objects. In European Conference on Object-Oriented Programming. Springer-Verlag, 2004.
	8	C. A. R. Hoare. "An axiomatic basis for computer programming". Communications of the ACM, 12(10):576--580, 1969.
	9	Gary T. Leavens. JML's Rich, Inherited Specifications for Behavioral Subtypes. In International Conference on Formal Engineering Methods, pp. 2--34, 2006.
	10	S. Butkevich, M. Renedo, G. Baumgartner, and M. Young. Compiler and tool support for debugging object protocols. In Foundations of Software Engineering, 2000.
	11	B. Meyer. Eiffel: The Language. Prentice Hall, 1992.
	12	R. Duke, G. Rose, and G. Smith. Object-z: A specification language advocated for the description of standards. Computer Standards and Interfaces, 17:511--533, 1995.
	13	D. Harel. Statecharts: A visual formalism for complex systems. Sci. Comput. Programming, 8:231--274, 1987.
	14	Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. The Spec# programming system: An overview. In Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, 2004.
	15	Cheon, Y., Perumendla, A. 2005. Specifying and checking method call sequences in JML. In: Arabnia, H. R., Reza, H. (eds.), Proceedings of the 2005 International Conference on Software Engineering Research and Practice (SERP'05). vol. II, June 27-29, 2005, Las Vegas, Nevada, CSREA Press, pp. 511--516.
	16	Kevin Bierhoff, Nels E. Beckman, and Jonathan Aldrich. Practical API Protocol Checking with Access Permissions. In Proceedings of the 23rd European Conference on Object-Oriented Programming (ECOOP'09) (Genova, Italy, July 2009). to appear.