<p>Just to expand on Jukka's excellent answer, the question of finding invariants usually arises when trying to establish safety properties. A <em>safety property</em> <span class="math-container">$S$</span> is a property that we wish for the system or program to never violate. A safety property that holds at all reachable states is (an) <em>invariant</em>. A way to show that <span class="math-container">$S$</span> is indeed invariant is to find an <em>inductive invariant</em> (i.i.) <span class="math-container">$I$</span> that satisfies three conditions:</p>
<ol>
<li><span class="math-container">$Init \Rightarrow I$</span> (I holds initially)</li>
<li><span class="math-container">$I \wedge Step \Rightarrow I'$</span> (if <span class="math-container">$I$</span> holds before a step, then it holds after the step)</li>
<li><span class="math-container">$I \Rightarrow S$</span> (<span class="math-container">$I$</span> is strong enough to establish the required property)</li>
</ol>
<p>If <span class="math-container">$S$</span> is already an i.i. then we are done. Typically however it isn't. Thats where the fun begins. In the example given above, we may want to ensure that <span class="math-container">$x$</span> is always positive, and make <span class="math-container">$x&gt;0$</span> a safety property. This safety property is also invariant. It is however not an i.i. An i.i. for this problem is <span class="math-container">$x&gt;1$</span>.</p>
<p>The <em>strongest</em> inductive invariant corresponds to (characterizes) exactly the reachable set. (The reason <em>False</em> which is the strongest possible property can't be an i.i. is due to the first condition above). For the example above, the property <span class="math-container">$J(x) \equiv \exists i \geq 0 \cdot x = 1 + r^i$</span> characterizes all the reachable states and its easy to verify that it is also an i.i. for the safety property <span class="math-container">$x&gt;0$</span>. It is therefore the strongest i.i. But finding the strongest i.i. in general is not easy. Hence we settle for a larger set (weaker property, also called an over-approximation) that still holds in all the reachable states but may include additional states that we don't care about. However all its states including unreachable ones are still contained in the safety property. If <span class="math-container">$II1$</span> is a stronger i.i. than <span class="math-container">$II2$</span> and <span class="math-container">$R$</span> is the reachable set then the following relationship always holds: <span class="math-container">$R \subseteq II1 \subseteq II2 \subseteq S$</span>.</p>

CC BY-SA 4.0
2023-04-14T18:23:06.093Z
2023-04-17T18:09:58.867Z
2023-04-17T18:09:58.867Z
Motorhead
<p>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.</p>

<p>Program:</p>

<ul>
<li>Initialise: $x \gets 2$.</li>
<li>Iterate: $x \gets 2x - 1$.</li>
</ul>

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

<p>However, it is not an <em>inductive</em> 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 <em>all</em> that we know, then we might have $x = 0.1$ before an iteration and thus $x &lt; 0$ after the iteration.</p>

<p>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.</p>

CC BY-SA 2.5
2010-11-26T09:41:54.763Z
Thanks for the example. I understand the difference now.
Chan Li
CC BY-SA 2.5
2010-11-25T17:18:36.960Z
2010-11-25T17:18:36.960Z
Jukka Suomela
<p>I would like to understand this with an example. Also, are there other kinds of invariants related to these?</p>

<p>Thanks!</p>

CC BY-SA 2.5
2010-11-25T12:39:29.443Z
Seems like homework to me. Could you explain how you came by this problem? You may want to read http://en.wikipedia.org/wiki/Invariant_(computer_science) and http://en.wikipedia.org/wiki/Loop_invariant
Marcus Ritt
CC BY-SA 2.5
2010-11-25T14:06:32.270Z
No, this isn't a homework question. I vaguely remember reading that an inductive invariant/assertion is stronger (if a predicate holds in the initial state of the system, it holds in all the reachable states) than just an invariant. But I'm not able to find any definitions in the papers. Hence the question. Any help would be appreciated.
Chan Li
CC BY-SA 2.5
2010-11-25T14:56:05.727Z
I think you got the right definition. For an example have look at http://portal.acm.org/citation.cfm?id=646485.694471
Marcus Ritt
CC BY-SA 2.5
2010-11-25T15:25:48.443Z
I have seen the reference you mention. The problem is this: If Inv is an invariant for a program Prog then Inv holds in all reachable states of Prog. If IInv is an inductive invariant for Prog, it holds in every initial state of Prog AND it is preserved under all the transitions, therefore it holds in all reachable states of Prog. Now, it is often mentioned that IInv -> Inv holds. But what I don't get is that why doesn't Inv -> IInv hold? Since, Inv holds in 'all' reachable states of Prog, which includes initial states, the latter should hold as well. What am I missing?
Chan Li
<pl.programming-languages><program-verification>
What's the difference between an invariant and an "inductive" invariant?
Chan Li
# What's the difference between an invariant and an "inductive" invariant?

(Asked by: username_0 on 2010-11-25)

I would like to understand this with an example. Also, are there other kinds of invariants related to these?

Thanks!

**Tags:** pl.programming-languages, program-verification

> **Comments:**
> **username_1**: Seems like homework to me. Could you explain how you came by this problem? You may want to read http://en.wikipedia.org/wiki/Invariant_(computer_science) and http://en.wikipedia.org/wiki/Loop_invariant  
> **username_0**: No, this isn't a homework question. I vaguely remember reading that an inductive invariant/assertion is stronger (if a predicate holds in the initial state of the system, it holds in all the reachable states) than just an invariant. But I'm not able to find any definitions in the papers. Hence the question. Any help would be appreciated.  
> **username_1**: I think you got the right definition. For an example have look at http://portal.acm.org/citation.cfm?id=646485.694471  
> **username_0**: I have seen the reference you mention. The problem is this: If Inv is an invariant for a program Prog then Inv holds in all reachable states of Prog. If IInv is an inductive invariant for Prog, it holds in every initial state of Prog AND it is preserved under all the transitions, therefore it holds in all reachable states of Prog. Now, it is often mentioned that IInv -> Inv holds. But what I don't get is that why doesn't Inv -> IInv hold? Since, Inv holds in 'all' reachable states of Prog, which includes initial states, the latter should hold as well. What am I missing?  

---

## 2 answers

### Answer by username_3 on 2010-11-25. Score: 22 | Accepted answer

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 > 0$ before an iteration is not sufficient to guarantee that $x > 0$ after the iteration. After all, if $x > 0$ is *all* that we know, then we might have $x = 0.1$ before an iteration and thus $x < 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 > 1$ before an iteration, then also $x > 1$ after the iteration.

> **Comments:**
> **username_0**: Thanks for the example. I understand the difference now.  

---

### Answer by username_2 on 2023-04-14. Score: 5

Just to expand on Jukka's excellent answer, the question of finding invariants usually arises when trying to establish safety properties. A *safety property* $S$ is a property that we wish for the system or program to never violate. A safety property that holds at all reachable states is (an) *invariant*. A way to show that $S$ is indeed invariant is to find an *inductive invariant* (i.i.) $I$ that satisfies three conditions:

1. $Init \Rightarrow I$ (I holds initially)
2. $I \wedge Step \Rightarrow I'$ (if $I$ holds before a step, then it holds after the step)
3. $I \Rightarrow S$ ($I$ is strong enough to establish the required property)

If $S$ is already an i.i. then we are done. Typically however it isn't. Thats where the fun begins. In the example given above, we may want to ensure that $x$ is always positive, and make $x>0$ a safety property. This safety property is also invariant. It is however not an i.i. An i.i. for this problem is $x>1$.

The *strongest* inductive invariant corresponds to (characterizes) exactly the reachable set. (The reason *False* which is the strongest possible property can't be an i.i. is due to the first condition above). For the example above, the property $J(x) \equiv \exists i \geq 0 \cdot x = 1 + r^i$ characterizes all the reachable states and its easy to verify that it is also an i.i. for the safety property $x>0$. It is therefore the strongest i.i. But finding the strongest i.i. in general is not easy. Hence we settle for a larger set (weaker property, also called an over-approximation) that still holds in all the reachable states but may include additional states that we don't care about. However all its states including unreachable ones are still contained in the safety property. If $II1$ is a stronger i.i. than $II2$ and $R$ is the reachable set then the following relationship always holds: $R \subseteq II1 \subseteq II2 \subseteq S$.


---

