Loop invariant
= Loop invariant
{wiki}
A statement true whenever execution reaches a chosen point in a loop, usually immediately before its condition is tested. Establish it initially, preserve it through each iteration, and combine it with the exit condition to establish <algorithm correctness>. Termination needs a separate argument.https://www.cs.cornell.edu/courses/cs2112/2019fa/lectures/loopinv/[Cornell CS 2112: loop invariants]{ref}