Bonjour,

Cela fait deux jours que je bloque sur un exercice dans lequel je dois trouver deux invariants de boucles.
Je pense avoir bien compris ce qu'est un invariant, mais alors pour le trouver, j'ai vraiment du mal

Je vous poste ici l'énoncé de la partie sur laquelle je bloque, ainsi que mon état d'avancement sur le sujet.
Un petit coup de pouce pour avancer serait le bienvenu

Énoncé
  1. Pour le programme ci-dessous, trouver l'invariant I de la boucle externe et montrer qu'il implique la post-condition Q = { z= a * b * c } à la sortie de la boucle externe.
  2. Trouver l'invariant J de la boucle interne et montrer qu'il implique la post-condition I, à la sortie de la boucle interne.

Code du programme :

Code:
    tantQue x > 0

        x = x - 1
        y = 0

        tantQue y < b

            z = z + a
            y = y + 1

        finTantQue

    finTantQue
Ma réflexion

Pour trouver l'invariant I ( de la boucle externe) j'ai utilisé la règle logique de Hoare, qui nous dit :

Code:
I, !Ce => Q
(avec Ce la condition de la boucle externe)

j'ai donc trouvé :

Code:
I = { z = a*b*c - (x * a * b)
(en partant du principe que c est la valeur initiale de x)
je ne suis pas sûr de mon résultat, mais il me semble être correct étant donné que lorsque x arrive à 0, on retombe sur z = a*b*c.


Le deuxième invariant me pose plus de problèmes, je me base sur la même règle (logique de Hoare) qui nous donnerai :

Code:
J, !Ci => I
où Ci est la condition de la boucle interne ( C = { y < b } donc !C = {y >= b } ),
J l'invariant de la boucle interne, et I l'invariant de la boucle externe calculé plus haut.

c'est ici que je bloque, je n'arrive pas à trouver l'invariant J.

Si quelqu'un peut me donner une piste à suivre pour le trouver, s'il vous plaît, ça serait vraiment super .

Merci par avance,

PinoTM