Abstract
To have impact, a grand challenge should provide a way for diverse research to be integrated in a synergistic fashion. Synergy in the JML project comes from a shared specification language, and thus holds several lessons for the verifying compiler grand challenge. An important lesson is that the project should focus considerable resources on specification language design, which still contains many open research problems. Another important lesson is that, to support such a specification language, the project needs to involve groups doing research on extensible compilers and integrated development environments.
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
Hoare, T.: The verifying compiler: A grand challenge for computing research. Journal of the ACM 50(1), 63–69 (2003)
Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Journal on Software Tools for Technology Transfer 7(3), 212–232 (2005)
Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. Science of Computer Programming 55(1-3), 185–208 (2005)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI 2002), June 2002. SIGPLAN, vol. 37(5), pp. 234–245. ACM Press, New York (2002)
Meyer, B.: Object-oriented Software Construction, 2nd edn. Prentice Hall, New York (1997)
Dhara, K.K., Leavens, G.T.: Forcing behavioral subtyping through specification inheritance. In: Proceedings of the 18th International Conference on Software Engineering, March 1996. A corrected version is ISU CS TR #95-20c, pp. 258–267. IEEE Computer Society Press, Berlin (1996), http://tinyurl.com/s2krg
Leavens, G.T.: JML’s rich, inherited specifications for behavioral subtypes. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 2–34. Springer, Heidelberg (2006)
Leavens, G.T., Naumann, D.A.: Behavioral subtyping, specification inheritance, and modular reasoning. Technical Report 06-20b, Department of Computer Science, Iowa State University, Ames, Iowa, 50011 (September 2006)
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., Müller, P., Kiniry, J., Chalin, P.: JML reference manual. In: Department of Computer Science, Iowa State University (February 2007), http://www.jmlspecs.org
Barnett, M., Naumann, D.A., Schulte, W., Sun, Q.: Allowing state changes in specifications. In: Müller, G. (ed.) ETRICS 2006. LNCS, vol. 3995, pp. 321–336. Springer, Heidelberg (2006)
Naumann, D.A.: Observational Purity and Encapsulation. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 190–204. Springer, Heidelberg (2005)
Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6), 27–56 (2004)
Leino, K.R.M., Müller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 491–516. Springer, Heidelberg (2004)
Leino, K.R.M., Nelson, G.: Data abstraction and information hiding. ACM Transactions on Programming Languages and Systems 24(5), 491–553 (2002)
Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular specification of frame properties in JML. Concurrency and Computation: Practice and Experience 15(2), 117–154 (2003)
Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Science of Computer Programming 62(3), 253–286 (2006)
Boyland, J., Noble, J., Retert, W.: Capabilities for sharing. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 1–27. Springer, Heidelberg (2001)
Noble, J., Vitek, J., Potter, J.: Flexible alias protection. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol. 1445, pp. 158–185. Springer, Heidelberg (1998)
Dietl, W., Müller, P.: Universes: Lightweight ownership for JML. Journal of Object Technology 4(8), 5–32 (2005)
Szyperski, C., Gruntz, D., Murer, S.: Component Software: Beyond Object-Oriented Programming, 2nd edn. ACM Press and Addison-Wesley, New York (2002)
Ernst, G.W., Navlakha, J.K., Ogden, W.F.: Verification of programs with procedure-type parameters. Acta Informatica 18(2), 149–169 (1982)
Goguen, J.A.: Parameterized programming. IEEE Transactions on Software Engineering SE-10(5), 528–543 (1984)
Büchi, M., Weck, W.: A plea for grey-box components. Technical Report 122, Turku Center for Computer Science, Presented at the Workshop on Foundations of Component-Based Systems, Zürich (1997) (September 1997), http://tinyurl.com/2833tr
Büchi, M., Weck, W.: The greybox approach: When blackbox specifications hide too much. Technical Report 297, Turku Center for Computer Science (August (1999), http://tinyurl.com/ywmuzy
Büchi, M.: Safe language mechanisms for modularization and concurrency. Technical Report TUCS Dissertations No. 28, Turku Center for Computer Science (May 2000)
Ball, T., Rajamani, S.K.: The SLAM project: Debugging system software via static analysis. In: Conference Record of POPL 2002: The 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, January 16–18, 2002, pp. 1–3 (2002)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York (1992)
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Z.H.: Bandera: Extracting finite-state models from Java source code. In: Proceedings of the 22nd International Conference on Software Engineering, June 2000, pp. 439–448. ACM Press, New York (2000)
Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming 8(3), 231–274 (1987)
Cheon, Y., Perumendla, A.: Specifying and checking method call sequences in JML. In: Arabnia, H.R., Reza, H. (eds.) Proceedings of the 2005 International Conference on Software Engineering Research and Practice (SERP 2005), June 27-29, 2005, vol. II, pp. 511–516. CSREA Press, Las Vegas, Nevada (2005)
RodrÃguez, E., Dwyer, M.B., Flanagan, C., Hatcliff, J., Leavens, G.T.: Robby: Extending JML for modular specification and verification of multi-threaded programs. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol. 3586, pp. 551–576. Springer, Heidelberg (2005)
Guttag, J.V., Horning, J.J., Garland, S., Jones, K., Modet, A., Wing, J.: Larch: Languages and Tools for Formal Specification. Springer, New York (1993)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Leavens, G.T., Clifton, C. (2008). Lessons from the JML Project. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)