[ main | cases | smart cards | formal methods | schedule | groups ]
Below some information and pointers about the languages, methods, and tools that you will use in this OOTI course. This should help you get started analyzing your applications.
JML, which stands for Java Modeling Language, is a specification language tailored to Java. JML can be used to specify the detailed design of Java (Card) programs, and to record design decisions that have been taken, by annotating programs with for instance class invariants, preconditions, and postconditions, in the Design-By-Contract style.
We will be using two tools that support JML:
JML assertions in a Java program can be compiled into runtime tests that are performed when the program is executing. This will signal any violations of of invariants, preconditions, and postconditions that occur at runtime.
The runtime assertion checker can be downloaded from the JML sourceforge page. Runtime assertion checking actually involves two separate tools, a special compiler jmlc that produces special bytecode which include runtime checks (which replaces javac), and a program jmlrac to execute this bytecode (which replaces java).
ESC/Java is a
tool that automatically checks JML-annotated Java(Card) code,
and warns about potential NullPointerExceptions and
ArrayIndexOutOfBoundsExceptions ESC/Java will be used for the
verification of the Java Card smart card applets.
To use ESC/Java to check your Java Card source code, you will need JML specifications of the Java Card API.
Documentation about ESC/Java (old?):
Some pointers to literature about JML and JML-related tools:
Design by Contract with JML. Gary T. Leavens and Yoonsik Cheon.
An overview of JML tools and applications. Lilian Burdy, Yoonsik Cheon, David Cok, Michael Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll.
A Runtime Assertion Checker for the Java Modeling Language (JML).
Yoonsik Cheon and Gary T. Leavens. In Hamid R. Arabnia and Youngsong Mun (eds.), International Conference on Software Engineering Research and Practice (SERP '02), Las Vegas, Nevada, pages 322-328. CSREA Press, June 2002.
C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, J.B. Saxe, R. Stata. Extended static checking for Java.
In the proceedings of Conference on Programming Language Design and Implementation (PLDI'2002), pages 234- 245, ACM, 2002. © ACM
Formal specification of Gemplus' electronic purse case study
Nestor Cataño and Marieke Huisman. In the proceedings of Formal Methods Europe (FME 2002), Number 2391 of LNCS, pages 272-289. Springer-Verlag, 2002. © Springer-Verlag
A Simple and Practical Approach to Unit Testing: The JML and JUnit Way.
Yoonsik Cheon and Gary T. Leavens. In Boris Magnusson (ed.), ECOOP 2002 -- Object-Oriented Programming, 16th European Conference, Malaga, Spain, June 2002, Proceedings. Volume 2374 of Lecture Notes in Computer Science, Springer-Verlag, 2002, pages 231-255. © Springer-Verlag
Lots more can be found via the JML webpage.
Source code analysers, also called program checkers, are tools that
automatically enforce coding standards and warn about potential bugs
using a technique called static analysis.
The checks done by these tools can be for rules in coding guidelines,
e.g. that method names should not start with a capital letter,
but they also can be much more advanced, e.g. to detect dead code, or
suspicious and possibly erroneous uses of == rather than
.equals() to compare objects.
To get an idea of what program checkers do, see
article about the program checker Findbugs at IBM developersWorks.
Examples of source code analysers to try out are Findbugs and PMD.