4
$\begingroup$

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

Thanks!

$\endgroup$
  • 4
    $\begingroup$ Seems like homework to me. Could you explain how you came by this problem? You may want to read en.wikipedia.org/wiki/Invariant_(computer_science) and en.wikipedia.org/wiki/Loop_invariant $\endgroup$ – Marcus Ritt Nov 25 '10 at 12:39
  • $\begingroup$ 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. $\endgroup$ – Chan Li Nov 25 '10 at 14:06
  • $\begingroup$ I think you got the right definition. For an example have look at portal.acm.org/citation.cfm?id=646485.694471 $\endgroup$ – Marcus Ritt Nov 25 '10 at 14:56
  • $\begingroup$ 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? $\endgroup$ – Chan Li Nov 25 '10 at 15:25
11
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks for the example. I understand the difference now. $\endgroup$ – Chan Li Nov 26 '10 at 9:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.