[Pl-seminar] 12/7: Gary T. Leavens, "JML's Rich, Inherited Specifications for Behavioral Subtypes"

[Stevie Strickland]

NEU Programming Languages Seminar presents

Gary T. Leavens
University of Central Florida

Wednesday, 12/7

11:45am - 1:30pm
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Title: JML's Rich, Inherited Specifications for Behavioral Subtypes

Abstract:

The Java Modeling Language (JML) is used to specify detailed designs for Java classes and interfaces. It has a particularly rich set of features for specifying methods. This talk describes those features, with particular emphasis on the features related to specification inheritance. It shows how specification inheritance in JML forces behavioral subtyping, through a discussion of semantics and examples. It also describes a notion of modular reasoning based on static type information, supertype abstraction, which is made valid in JML by methodological restrictions on invariants, history constraints, and initially clauses and by behavioral subtyping.

Bio:

Gary T. Leavens is a professor and interim chair of the department of EECS, Computer Science Division at the University of Central Florida (UCF). He joined UCF in August 2007, was associate chair from August 2008 to August 2010, and was appointed interim chair in September 2010. Previously he was a professor of computer science at Iowa State University in Ames, Iowa, where he started in January 1989. He 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 languages.  His best known work in the area of formal methods is related to the JML project, an international effort with many associated tools (see http://jmlspecs.org).  His work on specification languages embodies insights from his work on the theory of behavioral subtyping (with David Naumann, Don Pigozzi, and others). His best known work on language design and semantics is on aspect-oriented programming (joint with Curtis Clifton, James Noble, Hridesh Rajan, and Medhi Bagherzadeh) and multiple dispatch languages such as MultiJava. See http://www.eecs.ucf.edu/~leavens for more information on his research.

Note:

A limited number of slots are still available for one-on-one discussions with the invited speaker.  Please contact me with your availability on Wednesday if you are interested.

Thanks,
Stevie