Loading...
Please wait, while we are loading the content...
Similar Documents
Typestate protocol specification in JML
| Content Provider | ACM Digital Library |
|---|---|
| Author | Kang, Sungwon Aldrich, Jonathan Kim, Taekgoo Bierhoff, Kevin |
| 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. |
| Starting Page | 11 |
| Ending Page | 18 |
| Page Count | 8 |
| File Format | |
| ISBN | 9781605586809 |
| DOI | 10.1145/1596486.1596490 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2009-08-25 |
| Publisher Place | New York |
| Access Restriction | Subscribed |
| Subject Keyword | Behavioral subtyping Usage protocol Typestate Jml |
| Content Type | Text |
| Resource Type | Article |