SAVCBS 2009
Last updated November 2009
Taekgoo Kim, Kevin Bierhoff, Jonathan Aldrich, and Sungwon Kang. Typestate Protocol Specification in JML. In Proceedings of the 8th International Workshop on Specification and Verification of Component-Based Systems (SAVCBS '09) at ESEC/FSE 2009, Amsterdam, The Netherlands, August 25, 2009, pages 11-18. ACM Press, New York, August 2009.
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. 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.