Une autre solution (la plus fréquente) consiste à calculer l'état suivant par une expression arithmétique
plutôt que d'explorer toutes les possibilités.
void incrementer3() {
if (this.etat < 29) {
this.etat += 3;
} else {
// sinon etat >= 29, on dépasse de 31
this.etat += (3 - 32) ; // équivaut à this.etat -= 29;
}
}
Il faut faire attention à trouver le bon compromis entre la lisibilité et le nombre de lignes. Cette dernière
solution a en effet moins de lignes, mais nécessite une réflexion plus longue pour se convaincre qu'elle est juste.
Dans ce cas, on peut travailler par invariants.
Ici, on veut s'assurer que quoi qu'il arrive, l'état sera toujours dans l'intervalle [0,32[.
0 ≤ etat < 32 est donc notre invariant. On remarque que cet invariant est vrai
pour l'état initial (0).
/** invariant : 0 ≤ etat < 32 */
void incrementer3() { /* On suppose que l'invariant est vrai avant l'appel */
if (this.etat < 29) {
/* invariant : 0 ≤ etat < 29
* donc : 3 ≤ etat+3 < 32 */
this.etat += 3;
/* invariant : 3 ≤ etat < 32 */
} else {
/* invariant : 29 ≤ etat < 32
* donc : 0 ≤ etat-29 < 3 */
this.etat += (3 - 32) ; // équivaut à this.etat -= 29;
/* invariant : 0 ≤ etat < 3 */
}
} /* on constate qu'il est alors maintenu après l'appel dans tous les cas ! */
Il faudrait faire ce calcul pour chacune des méthodes de la classe.
Source : Compteur5Bits.java
