Attendees will come out of this tutorial with a firm understanding of the use of specifications in software design and engineering, a basic knowledge of the JML specification languages, and will be knowledgeable about the various tools available for the JML language, particularly the JML tool suite, ESC/Java2, and Kiasan.
OCTOBER 25 TO 29, 2009
T33. Introduction to Java Modeling Language (JML)
Hridesh Rajan, Iowa State University
Curtis Clifton, Rose-Hulman Institute of Technology
Curt is an assistant professor in the Dept. of Computer Science and Software Engineering at Rose-Hulman Inst. of Technology. He is a co-designer and the main implementor of the MultiJava programming language. He has also worked on the Java Modeling Language for behavior and interface specification and on foundations of aspect-oriented programming.
Gary T. Leavens, University of Central Florida
Gary is a Professor in the School of Electrical Engineering and Computer Science, University of Central Florida. Gary is the creator of the Java Modeling Language and leads the development of the JML Tool Suite.
Joseph R. Kiniry, University College Dublin
Joe is a lecturer in the Deparment of Computer Science at University College Dublin. He was previously in the SoS Group at Radboud University Nijmegen. He earned his Ph.D. in Computer Science from the California Institute of Technology. Joe is the coauthor of ESC/Java2.
Robby, Kansas State University
Robby is an associate professor in the Department of Computing and Information Sciences at Kansas State University. Robby and his students are collaborating on the development of JML4 — an Eclipse-based JML software infrastructure, and the Kiasan static analyzer.
This tutorial introduces the Java Modeling Language (JML) and associated tool suite. JML can be used to specify and check the behavior of Java modules. This helps developers eliminate bugs and improve the reliability of their software.
JML is a behavioral interface specification language. It combines the design by contract approach of Eiffel and the model-based specification approach of the Larch family of interface specification languages, with some elements of the refinement calculus. JML has a Java-based syntax and semantics, thus is easy to learn for Java programmers.
Among other tools, the JML suite includes ESC/Java2, a tool that checks that a program is consistent with its annotation. It also detects, at compile time, common programming errors that ordinarily are not detected until run time, and sometimes not even then; for example, null dereference errors, array bounds errors, type cast errors, and race conditions. While ESC/Java uses a theorem prover, it feels to a programmer more like a powerful type checker.
Because JML is familiar to Java programmers, and static checkers such as ESC/Java2 just feel like a typechecker, we believe that they are an excellent way to gently introduce developers to formal methods while providing practical tools to improve the reliability of their software.
Objectives:
Format:
This tutorial will be a combination of slide-based lecture and hands-on exercises. Participants are encouraged to bring their own laptop so that they can complete the exercises that will be an integral part of this tutorial.
Audience:
Researchers, Practitioners, Managers, Educators
-
Conference Chair
Adayana, Inc.
-
Program Chair
University of Central Florida
Please email any questions to
.
This e-mail address is being protected from spambots. You need JavaScript enabled to view it