Abstract
This paper presents a syntactic method to check so-called assignable clauses of annotated Java programs. Assignable clauses describe which variables may be assigned by a method. Their correctness is crucial for reasoning about class specifications. The method that we propose is incomplete, as it only makes a syntactic check and it does not take aliasing or expression evaluation into account, but it provides efficient means to find the most common errors in assignable clauses. This is demonstrated by applying the method to the specification of an industrial case study.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
D. Bartetzko, C. Fischer, M. Möller, and H. Wehrheim. Jass — Java with Assertions. In K. Havelund and G. Rosşu, editors, ENTCS, volume 55(2). Elsevier Publishing, 2001.
J. van den Berg and B. Jacobs. The LOOP compiler for Java and JML. In T. Margaria and W. Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001), number 2031 in LNCS, pages 299–312. Springer, 2001.
A. Borgida, J. Mylopoulos, and R. Reiter. On the frame problem in procedure specifications. IEEE Transactions on Software Engineering, 21(10):785–798, 1995.
N. Cataño and M. Huisman. Assignable specifications for the Electronic Purse case study, 2002. http://www-sop.inria.fr/lemme/verificard/modifSpec.
N. Cataño and M. Huisman. Formal specification and static checking of Gemplus’s electronic purse using ESC/Java. In L.-H. Eriksson and P.A. Lindsay, editors, Formal Methods Europe (FME’ 02), number 2391 in LNCS, pages 272–289. Springer, 2002.
Differences between Esc/Java and JML, 2000. Comes with JML distribution, in file esc-jml-diffs.txt.
J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java Language Specification Second Edition. The Java Series. Addison-Wesley, 2000.
The JASS project. http://semantik.informatik.uni-oldenburg.de/~jass/.
G.T. Leavens, A.L. Baker, and C. Ruby. Preliminary Design of JML: a Behavioral Interface Specification Language for Java. Technical Report 98-06, Iowa State University, Department of Computer Science, 1998. http://www.cs.iastate.edu/~leavens/JML/prelimdesign/.
K.R.M. Leino. Data groups: specifying the modification of extended state. In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA’ 98), pages 144–153. ACM Press, 1998.
K.R.M. Leino. Applications of Extended Static Checking. In P. Cousot, editor, Static Analysis (SAS 2001), number 2126 in LNCS, pages 185–193. Springer, 2001.
K.R.M. Leino, G. Nelson, and J.B. Saxe. ESC/Java user’s manual. Technical Report SRC 2000-002, Compaq System Research Center, 2000.
B.H. Liskov and J.M. Wing. A behavioral notion of subtyping. ACM Trans. on Progr. Lang. and Systems, 16(1):1811–1841, 1994.
The LOOP project. http://www.cs.kun.nl/~bart/LOOP/.
J. McCarthy and P. Hayes. Some philosophical problems from the standpoint of artificial intelligence. In B. Meltzer and D. Michie, editors, Machine Intelligence 4, pages 463–502. Edinburgh Univ. Press, 1969.
B. Meyer. Object-Oriented Software Construction. Prentice Hall, 2nd rev. edition, 1997.
P. Müller. Modular Specification and Veri.cation of Object Oriented Programs. PhD thesis, FernUniversität Hagen, 2001.
E. Poll and F. Spoto. Static analysis for JML’s assignable clauses, 2002. Manuscript.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cataño, N., Huisman, M. (2003). CHASE:A Static Checker for JML’s Assignable Clause. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2003. Lecture Notes in Computer Science, vol 2575. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36384-X_6
Download citation
DOI: https://doi.org/10.1007/3-540-36384-X_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00348-9
Online ISBN: 978-3-540-36384-2
eBook Packages: Springer Book Archive