JML: Expressive Modular Reasoning for Java

Gary T. Leavens, University of Central Florida

Time and Location

12:30-13:30 Tuesday, 26 May 2009 - Carwein Auditorium, University of Washington Tacoma

Abstract

The Java Modeling Language (JML) is used to specify, check, and verify detailed designs for Java classes and interfaces. JML is an open, international, collaborative effort among 23 research groups and projects. This talk motivates work on formal methods and the JML effort. It gives an overview of the JML effort, including its tool support for runtime assertion checking, extended static checking, static verification, unit testing, etc. It describes ways that JML can help designers, particularly in dealing with subtyping and dynamic dispatch.

Subtyping and dynamic dispatch in object-oriented languages pose a challenge for modular reasoning, which is the key to practical tools. Modular reasoning is done by using supertype abstraction -- reasoning based on static type information. I describe how JML's specification inheritance forces behavioral subtyping, through a discussion of semantics and examples. Behavioral subtyping, together with a set of methodological restrictions, makes JML's supertype abstraction a valid reasoning technique.

This work was supported in part by NSF grants CCF 0429567 and CNS 08-08913. The work on behavioral subtyping in particular is based on joint work with Prof. David A. Naumann of Stevens University. See http://jmlspecs.org/ for more information about JML.

Biographical Information

Gary T. Leavens is a professor and associate director of the School of Electrical Engineering and Computer Science at the University of Central Florida, where he has been since August 2007. Previously he was a professor of computer science at Iowa State University in Ames, Iowa, where he started in January 1989. He also received his Ph.D. from MIT in 1989. Before his graduate studies at MIT, he worked at Bell Telephone Laboratories in Denver Colorado as a member of technical staff.

Professor Leavens's research interests include programming and specification language design and semantics, program verification, and formal methods, with an emphasis on the object-oriented and aspect-oriented paradigms. For more information on his research see http://www.eecs.ucf.edu/~leavens/. Professor Leavens is a Senior member of the ACM and IEEE, and a member of the IFIP working group on programming methodology (WG 2.3). He is an assistant editor for the journal Software and Systems Modeling (SoSyM). He is program committee chair of OOPSLA 2009 and has served on the program committees of numerous conferences, including OOPSLA, Formal Methods, POPL, ECOOP, AOSD, ICSE, ESEC/FSE, and MFPS. He co-organizes three workshop series: Specification and Verification of Component-Based Systems (SAVCBS), Formal Techniques for Java-Like Languages (FTfJP), and Foundations of Aspect-Oriented Languages (FOAL).