Abstract
Formal specifications are more useful and easier to develop if they are executable. In this work, we describe a system for executing specifications written in the Java Modeling Language (JML) by translating them to constraint programs, which are then executed via the Java Constraint Kit (JCK). Our system can execute specifications written at a high level of abstraction, and the generated constraint programs are Java implementations of the translated specifications. Hence, they can be called directly from ordinary Java code.
This is a preview of subscription content, log in via an institution to check access.
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
Grieskamp, W.: A computation model for Z based on concurrent constraint resolution. In: Bowen, J.P., Dunne, S., Galloway, A., King, S. (eds.) B 2000, ZUM 2000, and ZB 2000. LNCS, vol. 1878, pp. 414–432. Springer, Heidelberg (2000)
Wahls, T., Leavens, G.T., Baker, A.L.: Executing formal specifications with concurrent constraint programming. Automated Software Engineering 7(4), 315–343 (2000)
Bouquet, F., Dadeau, F., Legeard, B., Utting, M.: Symbolic animation of JML specifications. In: Fitzgerald, J.A., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 75–90. Springer, Heidelberg (2005)
Wahls, T.: Compiling formal specifications to Oz programs. In: Van Roy, P. (ed.) MOZ 2004. LNCS, vol. 3389, pp. 66–77. Springer, Heidelberg (2005)
Leuschel, M., Butler, M.: ProB: A model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)
Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer (STTT) 7(3), 212–232 (2005)
Abdennadher, S., Krämer, E., Saft, M., Schmauss, M.: JACK: A Java constraint kit. In: Hanus, M. (ed.) Electronic Notes in Theoretical Computer Science, vol. 64, Elsevier, Amsterdam (2002)
Cheon, Y., Leavens, G.T.: A runtime assertion checker for the Java Modeling Language (JML). In: Arabnia, H.R., Mun, Y. (eds.) Proceedings of the International Conference on Software Engineering Research and Practice (SERP ’02), Las Vegas, Nevada, USA, June 24-27, 2002, pp. 322–328. CSREA Press (2002), ftp://ftp.cs.iastate.edu/pub/techreports/TR02-05/TR.pdf
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Krause, B., Wahls, T. (2007). jmle: A Tool for Executing JML Specifications Via Constraint Programming. In: Brim, L., Haverkort, B., Leucker, M., van de Pol, J. (eds) Formal Methods: Applications and Technology. PDMC 2006. Lecture Notes in Computer Science, vol 4346. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70952-7_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-70952-7_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70951-0
Online ISBN: 978-3-540-70952-7
eBook Packages: Computer ScienceComputer Science (R0)