# Does loop invariant has nothing to do with termination?

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)^2

(C)x=(y+1)2^y

(D)x=2^y

(E)None of the above, since the loop does not terminate

As per my solution, the loop never seems to terminate. I came with the answer E but the D is the answer to the above questions. Isn't the loop invariant affected by the nontermination of the loop?

• Do you intend some of the $2$'s to be exponents? As it stands, none of the answers, including (E), are appropriate. Commented Feb 28, 2021 at 12:39
• Yeah, it was my mistake, I type the question wrong. You were right @RickDecker I intended the 2's to be exponents. I apologize for that. Commented Feb 28, 2021 at 12:54

The loop invariant is just a proposition which holds on each iteration of the loop (in your question, the relationship between $$x$$ and $$y$$ holds regardless, so no, it is not affected by loop nontermination). It doesn't inherently say anything about termination. It is potentially something that you can use to argue about termination.