I am currently new and learning about loop invariants. I have come across this pseudocode where the goal is to shift the elements inside an array with N size in a clockwise direction by K steps.



Is at every iteration, new_index is in [0,N) a good loop invariant? I am really confused about how to pick a good one. Any help would be appreciated.


1 Answer 1


This would not be a good loop invariant, since its trivial (by the definition of modolu).

A good loop invariant here would be to assert that at step $m$, $A_{rot}$ will contain the first $m$ elements after rotation.

This loop invariant is not trivial anymore (you will need to work a bit to prove it) - and using it when $m=N$ will immediately prove that the algorithm is correct.

  • $\begingroup$ This makes much more sense. Thank you! $\endgroup$
    – fynn
    Dec 10, 2021 at 19:29
  • $\begingroup$ @fynn Glad I can help! In general, you would want to find loop invariants in such a way that on the last iteration the loop invariant will conclude that the entire property holds. That is, you want to use the loop invariant to prove correctness - so choose your loop invariant to reflect this. $\endgroup$
    – nir shahar
    Dec 10, 2021 at 20:14

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.