Specifying and checking method call sequences of Java programs Export

@article{cheon07specifying, abstract = {In a pre and postcondition-style specification, it is difficult to specify the allowed sequences of method calls, referred to as protocols. The protocols are essential properties of reusable object-oriented classes and application frameworks, and the approaches based on the pre and postconditions, such as design by contracts (DBC) and formal behavioral interface specification languages (BISL), are being accepted as a practical and effective tool for describing precise interfaces of (reusable) program modules.We propose a simple extension to the Java Modeling Language (JML), a BISL for Java, to specify protocol properties in an intuitive and concise manner. The key idea of our approach is to separate protocol properties from functional properties written in pre and post-conditions and to specify them in a regular expression-like notation. The semantics of our extension is formally defined and provides a foundation for implementing runtime checks. Case studies have been performed to show the effectiveness our approach. We believe that our approach can be adopted by other BISLs.}, address = {Netherlands}, author = {Yoonsik, Cheon and Ashaveena, Perumandla}, citeulike-article-id = {1124846}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/s11219-006-9001-4}, citeulike-linkout-1 = {http://www.ingentaconnect.com/content/klu/sqjo/2007/00000015/00000001/00009001}, doi = {10.1007/s11219-006-9001-4}, issn = {0963-9314}, journal = {Software Quality Journal}, keywords = {jml, softnet}, month = {March}, number = {1}, pages = {7--25}, posted-at = {2007-07-12 16:43:31}, priority = {5}, publisher = {Springer}, title = {Specifying and checking method call sequences of Java programs}, url = {http://dx.doi.org/10.1007/s11219-006-9001-4}, volume = {15}, year = {2007} }

TY - JOUR ID - cheon07specifying L3 - citeulike-article-id:1124846 N2 - In a pre and postcondition-style specification, it is difficult to specify the allowed sequences of method calls, referred to as protocols. The protocols are essential properties of reusable object-oriented classes and application frameworks, and the approaches based on the pre and postconditions, such as design by contracts (DBC) and formal behavioral interface specification languages (BISL), are being accepted as a practical and effective tool for describing precise interfaces of (reusable) program modules.We propose a simple extension to the Java Modeling Language (JML), a BISL for Java, to specify protocol properties in an intuitive and concise manner. The key idea of our approach is to separate protocol properties from functional properties written in pre and post-conditions and to specify them in a regular expression-like notation. The semantics of our extension is formally defined and provides a foundation for implementing runtime checks. Case studies have been performed to show the effectiveness our approach. We believe that our approach can be adopted by other BISLs. IS - 1 JF - Software Quality Journal SN - 0963-9314 AD - Netherlands EP - 25 TI - Specifying and checking method call sequences of Java programs PB - Springer VL - 15 SP - 7 KW - jml KW - softnet AU - Yoonsik, Cheon AU - Ashaveena, Perumandla PY - 2007/03// UR - http://dx.doi.org/10.1007/s11219-006-9001-4 ER -