An introduction to formal specifications and JML (Java Modelling Language)

Yves Ledru

Université Joseph Fourier,
Laboratoire d'Informatique de Grenoble,
681 Rue de la Passerelle, BP 72
38402 St Martin d'Hères cedex
Sep. 2013
(c) Yves Ledru

You will find under this page the slides and exercices used  for a course given at Master's level.



1. Invariants - getting started subject source files
2. Operation specification subject source files
3. A class of prime numbers subject source files
4. Invariant testing and pre-condition calculation subject source files
5. Combinatorial generation subject source files


Here are the tools used for the exercises with urls to retrieve them.

These exercises use JML 5.6. It can be retrieved  at
It is rather easy to install under Windows.
First get file JML.5.6_rc4.tar.gz, then unfold it under C:\JML and  add C:\JML\bin to your path.

A more complete documentation on JML is available on the site  or at the following url:

Tests will be executed with JUnit4, which can be retrieved at the following address:
(JUnit4 is also included in the distribution of IDEs like eclipse)

We also use GNU make to automatically compile and run programs.
GNU Make for windows  is available at the following address

Make sure that make and javac are on your path.