What's the difference between an invariant and an "inductive" invariant? I would like to understand this with an example. Also, are there other kinds of invariants related to these?

Thanks!
I don't know anything about the topic, so let me try to give a very simple example and let's see what others say.

Program:


Initialise: $x \gets 2$.
Iterate: $x \gets 2x - 1$.


Now "$x > 0$" is an invariant. It certainly holds initially and after each iteration.

However, it is not an inductive invariant: merely knowing that $x &gt; 0$ before an iteration is not sufficient to guarantee that $x &gt; 0$ after the iteration. After all, if $x &gt; 0$ is all that we know, then we might have $x = 0.1$ before an iteration and thus $x &lt; 0$ after the iteration.

On the other hand, something like "$x > 1$" is an invariant and also an inductive invariant. It is easy to check that if $x &gt; 1$ before an iteration, then also $x &gt; 1$ after the iteration.