Abstract
We show how to write a concise and elegant specification of a linearly linked data structure that is applicable for both verification and runtime checking. A specification of linked lists is given as an example. The concept of a list is captured by an observer method which is a functional version of a reachability predicate. The specification is written in the Java Modeling Language (JML) and does not require extensions of that language. This paper addresses a mixed audience of users and developers in the fields of formal verification, runtime checking, and specification language design. We provide an in-depth description of the proposed specification and analyze its implications both for verification and for runtime checking. Based on this analysis we have developed verification techniques that fully automate the verification process, using the KeY tool, and that are also described here.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Albert, E., Bubel, R., Genaim, S., Hähnle, R., Román-Díez, G.: Verified resource guarantees for heap manipulating programs. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 130–145. Springer, Heidelberg (2012)
Becker, K., Leavens, G.T.: Class LinkedList, http://www.eecs.ucf.edu/~leavens/JML-release/javadocs/java/util/LinkedList.html#removeint
Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)
Beckert, B., Trentelman, K.: Second-order principles in specification languages for object-oriented programs. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 154–168. Springer, Heidelberg (2005)
Cheon, Y.: A quick tutorial on JET. Technical Report UTEP-CS-07-40, Department Technical Reports (CS), University of Texas at El Paso (June 2007)
Darvas, A., Müller, P.: Reasoning about method calls in interface specifications. Journal of Object Technology 5(5), 59–85 (2006)
du Bousquet, L., Ledru, Y., Maury, O., Oriat, C., Lanet, J.-L.: Reusing a JML specification dedicated to verification for testing, and vice-versa: Case studies. Journal of Automated Reasoning 45, 415–435 (2010), 10.1007/s10817-009-9132-y
Jacobs, B., Piessens, F.: Inspector methods for state abstraction. Journal of Object Technology 6(5), 55–75 (2007)
Jensen, J.B., Birkedal, L., Sestoft, P.: Modular verification of linked lists with views via separation logic. Journal of Object Technology 10(2), 1–20 (2011)
Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: Proceedings of POPL, pp. 115–126. ACM (2006)
Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. SEN 31(3), 1–38 (2006)
Leavens, G.T., Leino, R., Müller, P.: Specification and verification challenges for sequential object-oriented programs. Formal Asp. Comput. 19(2), 159–189 (2007)
Leino, K.R.M.: Specification and verification of object-oriented software. In: Engineering Methods and Tools for Software Safety and Security. NATO Science for Peace and Security, vol. 22, pp. 231–266. IOS Press (2009)
Lev-Ami, T., Immerman, N., Reps, T.W., Sagiv, M., Srivastava, S., Yorsh, G.: Simulating reachability using first-order logic with applications to verification of linked data structures. Logical Methods in Computer Science 5(2) (2009)
Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 181–198. Springer, Heidelberg (2005)
Nelson, G.: Verifying reachability invariants of linked structures. In: Proceedings of POPL, pp. 38–47. ACM (1983)
Nguyen, H.H., Kuncak, V., Chin, W.-N.: Runtime checking for separation logic. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 203–217. Springer, Heidelberg (2008)
Rajamani, S.K.: Verification, testing and statistics. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol. 5779, p. 25. Springer, Heidelberg (2009)
Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames: Combining dynamic frames and separation logic. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol. 5653, pp. 148–172. Springer, Heidelberg (2009)
Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: Proceedings of PLDI, pp. 349–361 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gladisch, C., Tyszberowicz, S. (2013). Specifying a Linked Data Structure in JML for Formal Verification and Runtime Checking. In: Iyoda, J., de Moura, L. (eds) Formal Methods: Foundations and Applications. SBMF 2013. Lecture Notes in Computer Science, vol 8195. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41071-0_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-41071-0_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-41070-3
Online ISBN: 978-3-642-41071-0
eBook Packages: Computer ScienceComputer Science (R0)