Non modification de variable en JML

Non modification de variable en JML - Java - Programmation

Marsh Posté le 26-11-2008 à 15:06:46    

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.

Reply

Marsh Posté le 26-11-2008 à 15:06:46   

Reply

Sujets relatifs:

Leave a Replay

Make sure you enter the(*)required information where indicate.HTML code is not allowed