Invariants

[Google Scholar]

Notes: loop invariant

A property that is always true.

When applied to loops, it is a property that is true at both the start of a loop iteration and the end of a loop iteration.

When applied to global state, it is a property that is true at all times or when the state is not being modified (e.g., between command executions).


Loop invariant