Loop-invariante per un frammento di programma

Question

D) Considera il seguente frammento del programma:

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

Per il frammento di cui sopra, quale dei seguenti è invariante in loop?

A) x = y+1
B) x = (y+1)²
C) x = (y+1) 2^y
D) x = 2^y
E) nessuno dei precedenti, poiché il ciclo non termina

Dal momento che loop-invariante è qualcosa che è vero prima e dopo ogni iterazione di un ciclo. Quindi, secondo la definizione, sto ricevendo una risposta come (d) ma ho un dubbio se la risoluzione di quel ciclo è necessaria o meno per il codice dato. Una delle proprietà dell'algoritmo dice:- L'algoritmo dovrebbe sempre terminare dopo il n. di passaggi. Quindi, se la domanda riguarda lo pseudocodice, segnerò sicuramente la risposta come (d) ma poiché è un frammento di programma, quindi sono confuso tra le opzioni (d) ed (e).
Quindi, il mio dubbio è che la definizione di invariante loop è vera anche per il ciclo nel codice che è scritto in qualsiasi lingua come C, C ++ ecc.
Per favore aiuto.