Attention à la lecture ...

Un étudiant du groupe 3 a écrit, explicitant son calcul de la plus faible précondition

[x := x + 1] (x : 1..10)

Je rappelle que cela se lit :
la substitution de x + 1 à x établit l'invariant (x appartient à l'ensemble 0..10).
(Et non que x = l'ensemble des entiers de 0 à 10 !!!!)

Voici ce qu'a écrit l'étudiant :

[x := x + 1] (x : 1..9)

alors que la plus faible précondition est x : 1..9
Quand on fait en effet la substitution dans x : 1..10, ça donne :
x+1 : 1..10
ce qui donne (petites classes)
x : 1..9

Tant que x appartient à l'ensemble de 1 à 9 on peut ajouter + 1 à x.
C'est écrit plusieurs fois sur mes pages web et j'ai fait cette manip plusieurs fois en cours
et TD. Et même en couleur !

Ce qu'il a écrit est la plus faible précondition ...
x + 1 : 1..9
ce qui donne :
x : 1..8

Mais on lui a mis la note maxi. C'est qu'on veut être bien noté !
Et on justifie par "il n'a pas fait attention. Mais comme nous sommes télépathe, nous savons que c'est une coquille".

Je vous rappelle le premier vol d'Ariane V et le "dépassement de capacité".
Je vous rappelle aussi tous ces services de distribution d'eau qui, plus le client consommait, plus ils versaient de l'argent au client. ...
car ils ne prenaient pas en compte les changements de compteur. Et comme la consommation est calculé ainsi
Conso = nouvel index du compteur - ancien index du compteur
quand on mettait un nouveau compteur à un index inférieur à l'ancien index de l'ancien compteur, vous qui faites de la compta, vous savez que ...

Et je vous rappelle la dernière question du DS... vous voyez le rapport ?

J'ai eu comme réponse à la question :

voici le résultat du calcul de la précondition :
x : 1..9 & x < 9
ce qui se lit :
x doit appartenir à l'ensemble des entiers de 1 à 9
et x doit être inférieur à 9

Là je n'ai pas mis 1/1 à la réponse !