loop invariant

RU: инвариант цикла

A property that holds true before every iteration of a loop and is preserved by each iteration. Used in correctness proofs: if an invariant holds at initialization, is maintained by each step, and implies the desired result at termination, the algorithm is correct. Example: in insertion sort, the invariant is that the prefix up to the current index is always sorted.