  This report presents Jartege, a tool which allows random generation of unit
tests for Java classes specified in JML. JML (Java Modeling Language) is a
specification language for Java which allows one to write invariants for
classes, and pre- and postconditions for operations. As in the JML-JUnit tool,
we use JML specifications on the one hand to eliminate irrelevant test cases,
and on the other hand as a test oracle. Jartege randomly generates test cases,
which consist of a sequence of constructor and method calls for the classes
under test. The random aspect of the tool can be parameterized by associating
weights to classes and operations, and by controlling the number of instances
which are created for each class under test. The practical use of Jartege is
illustrated by a small case study.
