Transcript JML Tools: Review and Evaluation

Chris Grosshans
Mark Lewis-Prazen
JML TOOLS REVIEW &
EVALUATION
What is Java Modeling Language
(JML)?
public class Counter {
public final static int MAX = 100;
//@ invariant 0 <= count && count <= MAX;
private int count;
/*@ requires count < MAX;
@ ensures count == \old(count) + 1;
@ also
@ requires count == MAX;
@ ensures count == 0;
@*/
public void inc() {
count = count < MAX ? count + 1 : 0;
}
}
Project Motivation

Find JML tool(s) that we can use at work
◦ Easy to use
◦ Robust and fully developed

Project plan
◦ Survey all tools
◦ In depth analysis of most promising tools
◦ Introduce best of breed to work
Types of JML Tools
Run time checking – Tests for
violations of the JML assertions as Java
code is executed
 Static checking - checking annotations
prior to execution

◦ Automatic – little developer interaction
◦ Manual – Programmer provides proof for
more sound and complete evaluation
Overview of JML tools
Runtime Tools
Static Tools
JML2
JML3
ESC/java
LOOP
ESC/java2
FSPV
ESC4
FSPV
JML5
JML4
jml4c
Legend
Inactive
Active
Future
JMLEclipse
jml4c
JACK
JML4
JML4
Evaluation of the JML4
Tool Conclusions

Tools not commercially viable; currently
they are research tools
◦ Tools have difficulty keeping up with changing
language features
◦ Usability issues - difficult to install and use

Bottom line the tools are not actively
marketed commercially – Academically
driven w/o corporate sponsorship
Is JML useful?

Assuming a production ready JML tool:
Would you use JML?
◦ Hard to identify invariant pre/post conditions
◦ Adding specifications as complex as coding
◦ No published work showing results of testing
on industrial scale code

But, probably only cost- effective for
“mission critical” development
Questions
Significant References

CHALIN, P., JAMES, P. R., AND KARABOTSOS, G. JML4: Towards an industrial grade IVE for Java and
next generation research platform for JML. In VSTTE ’08: Proceedings of the 2008 Conference on
Verified Systems: Theories, Tools, and Experiments (2008).

COK, D. R., AND KINIRY, J. R. ESC/Java2: Uniting ESC/Java and JML. In Construction and Analysis of Safe,
Secure, and Interoperable Devices (2005), vol. 3362/2005 of LNCS, pp. 108-28.

LEAVENS, G. T., POLL, E., CLIFTON, C., CHEON, Y., RUBY, C., COK, D., MÜLLER, P., KINIRY, J., AND
CHALIN, P. JML reference manual, 2008. Available at http://www.jmlspecs.org.

LEINO, K. R. M., AND MONAHAN, R. Automatic verification of textbook programs that use
comprehensions. In FTfJP ’07: Formal Techniques for Java-like Programs (2007).

PAULSON, L. C., AND SUSANTO, K. W. Source-level proof reconstruction for interactive theorem
proving. In Theorem Proving in Higher Order Logics: TPHOLs 2007 (2007), K. Schneider and J. Brandt,
Eds., LNCS 4732, Springer, pp. 232–245.

TAYLOR, K.B.: A specification language design for the Java Modeling Language (JML) using Java 5
annotations. Masters thesis, Iowa State University (2008)