Consider the following program fragment:

var x, y: integer;
x := 1;
y := 0;

while y < x do
    x := 2*x;
    y := y+1

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





(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?

  • 1
    $\begingroup$ Do you intend some of the $2$'s to be exponents? As it stands, none of the answers, including (E), are appropriate. $\endgroup$ Commented Feb 28, 2021 at 12:39
  • $\begingroup$ 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. $\endgroup$ Commented Feb 28, 2021 at 12:54

1 Answer 1


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.

The Wikipedia article on correctness additionally describes the difference between partial and total correctness. For partial correctness, we don't require a program terminates, only that the result is correct if it is returned.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.