Invariants

s = 0
i = 0
while i < n:
    i = i + 1
    s = s + i

This loop adds up $1 + 2 + \ldots + n$. An invariant is a statement that is true before the loop and after every iteration.

Here the invariant is $s = 1 + 2 + \ldots + i$. A correctness proof has three parts: initialization, maintenance and termination.