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

France
Yves.Ledru@imag.fr

Sep. 2013
(c) Yves Ledru

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

Slides

Exercices

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

Tools

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

These exercises use JML 5.6. It can be retrieved at
http://sourceforge.net/projects/jmlspecs/files/jmlspecs/5.6_rc4/
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

http://jmlspecs.org or at the following url:
http://www.eecs.ucf.edu/~leavens/JML/jmlrefman/

Tests will be executed with JUnit4, which can be retrieved at the following address:
http://junit.org/
(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

http://gnuwin32.sourceforge.net/packages/make.htm

Make sure that make and javac are on your path.