Invariant en boucle pour un fragment de programme

Question

Q) Considérez le fragment de programme suivant:

var x,y:integer;  
x:=1; y:=0;  
while y < x do  
begin  
  x:=2∗x;  
  y:=y+1;  
end;

Pour le fragment ci-dessus, lequel des éléments suivants est un invariant de boucle?

A) x = y + 1
B) x = (y + 1)²
C) x = (y + 1) 2^y
D) x = 2^y
E) Aucune de ces éléments, car la boucle ne se termine pas

Depuis, la boucle invariante est quelque chose qui est vrai avant et après chaque itération d'une boucle. Ainsi, selon la définition, je reçois une réponse comme (d) mais je doute que la résiliation de cette boucle soit nécessaire ou non pour le code donné. L'une des propriétés de l'algorithme dit: - L'algorithme doit toujours se terminer après le NO fini. des étapes. Donc, si la question concerne le pseudocode, je marquerai certainement la réponse comme (d), mais comme c'est le fragment de programme, je suis donc confus entre les options (d) et (e).
Donc, mon doute est que la définition de la boucle-invariante est également vraie pour la boucle dans le code qui est écrit dans n'importe quelle langue comme C, C ++ etc.
Veuillez aider.