JML: Expressive Modular Reasoning for Java
Dr. Gary T. Leavens
Thursday, April 12, 2007
2:00PM ~ 3:00PM, Harris Center 125
Abstract
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. I explain our recent results proving that behavioral subtyping, together with a set of methodological restrictions, makes supertype abstraction valid.
This work was supported in part by NSF grant CCF-0429567. 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.
Short Bio
Gary T. Leavens is a professor of computer science at Iowa State University in Ames, Iowa. He has taught there since receiving his Ph.D. from MIT in 1989. 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.cs.iastate.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 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). He is married to Janet Leavens, who is a Ph.D. candidate in French Literature at the University of Iowa.
