Paper Info
Title
Specifying and Checking Method Call Sequences in JML
Abstract
In a pre and postconditions style specification, it is difficult to specify allowed sequences of method calls, often called protocols. However, 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 way of describing precise interfaces of (reusable) program modules. We propose a simple extension to JML, a BISL for Java, to specify protocol properties in an intuitive and concise manner. We also define a formal semantics of our extension and provide runtime checks. We believe that our approach can be easily adopted for other BISLs.
Year
Venue
Keywords
2005
SERP '05: PROCEEDINGS OF THE 2005 INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING RESEARCH AND PRACTICE, VOLS 1 AND 2
formal semantics,object oriented,design by contract
Field
DocType
Citations 
Simple extension,Programming language,Computer science,Design by contract,Real-time computing,Interface description language,Java Modeling Language,Java,Semantics of logic
Conference
6
PageRank 
References 
Authors
0.72
6
2
Name
Order
Citations
PageRank
Yoonsik Cheon177056.20
Ashaveena Perumandla2482.89