Salut,  
 
Je cherche a exprimer en JML le fait qu'il doit être impossible de modifier une variable entre un état x et un état y, j'ai tenter d'utiliser des choses comme maVariable == \old(maVariable) mais cela ne fonctionne pas car la condition est vérifiée uniquement au moment ou l'ont sort de la méthode donc au milieu on peut faire ce qu'on veut et ce n'est pas bon. J'ai tenter aussi avec un invariant de la sorte :
 
\\@invariant state != x ==> \not_modified(maVariable)  
 
Donc selon moi cela voudrait dire que si l'état est différent de x on ne peut pas modifier la variable, mais apparemment ça ne marche pas ...
 
Si quelqu'un peut me donner 2 - 3 pistes, je suis preneur, merci.