Loop-Invariant for a program fragment

Question

Q) Consider the following program fragment:

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

For the above fragment , which of the following is a loop-invariant ?

A) x=y+1
B) x=(y+1)²
C) x=(y+1)2^y
D) x=2^y
E) None of the above, since the loop does not terminate

Since, Loop-Invariant is something which is true before and after each iteration of a loop. So, according to the definition, I am getting answer as (D) but I have a doubt whether termination of that loop is necessary or not for the given code. One of the properties of algorithm says :- algorithm should always terminate after finite no. of steps. So, if the question is about Pseudocode then I will definitely mark answer as (D) but since it is program fragment, So I am confused between options (D) and (E).
So, My Doubt is definition of loop-invariant is also true for the loop in the code which is written in any language like C,C++ etc.
Please help.

Answer 1

The question asks for a loop invariant. This has nothing to do with termination. (D) does look reasonable but you may want to check with the usual tools such as Hoare logic, that (D) holds before the loop and is re-established by the loop body if the guard holds.

PS Your idea of an algorithm may need some work.