Marc Champesme & Guillaume Vauvert
Département d'informatique - Institut Galilée
Université Paris 13
On peut inclure trois types d'assertions: les invariants, associés à la classe, les preconditions et les postconditions, toutes deux associées à des méthodes. Avec JML, les assertions s'écrivent sous forme de commentaires situés dans le code de la classe ou avant l'entête des méthodes, à des emplacements précis et selon une syntaxe précise. Le but de ce document est de décrire cette syntaxe.